StrictConvexSpace.of_strictConvex_closed_unit_ball
theorem StrictConvexSpace.of_strictConvex_closed_unit_ball :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedLinearOrderedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedSpace ℝ E] [inst_4 : LinearMap.CompatibleSMul E E 𝕜 ℝ],
StrictConvex 𝕜 (Metric.closedBall 0 1) → StrictConvexSpace 𝕜 E
The theorem states that a real normed vector space is strictly convex if the unit ball in that space is strictly convex. In more detail, given a type `𝕜` representing a normed linear ordered field, and `E` representing a normed additive commutative group (that is also a normed space over `𝕜` and `ℝ`), if the unit ball centered at 0 with radius 1 (represented by `Metric.closedBall 0 1`) is a strictly convex set (meaning the open line segment between any two distinct points in the set lies entirely within the set's interior), then the entire space `E` is a strictly convex space. The compatibility of the scalar multiplication (`LinearMap.CompatibleSMul E E 𝕜 ℝ`) is also a necessary condition.
More concisely: If a real normed vector space `E` with strictly convex unit ball has compatible scalar multiplication, then `E` is a strictly convex space.
|
StrictConvexSpace.of_norm_add
theorem StrictConvexSpace.of_norm_add :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
(∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y) → StrictConvexSpace ℝ E
The theorem `StrictConvexSpace.of_norm_add` states that for any normed additive commutative group `E` which is also a normed space over real numbers, if for all pairs of vectors `x` and `y` in `E` with norm 1, the condition that the norm of their sum equals 2 implies that `x` and `y` are in the same ray, then it can be concluded that `E` is a strictly convex space. This theorem establishes a connection between the geometric property of being in the same ray and the algebraic property of strict convexity in a vector space.
More concisely: If a real normed additive commutative group `E` satisfies the property that any two vectors `x` and `y` with norm 1 for which `||x + y|| = 2` imply `x = t*y` for some `t > 0`, then `E` is a strictly convex space.
|
StrictConvexSpace.of_norm_combo_lt_one
theorem StrictConvexSpace.of_norm_combo_lt_one :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
(∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1) → StrictConvexSpace ℝ E
This theorem states that for any normed additively commutative group `E` that is also a normed space over the real numbers, if for every pair of distinct elements `x` and `y` of `E` with norm 1, there exist strictly positive real numbers `a` and `b` such that `a + b = 1` and the norm of the linear combination `a • x + b • y` is less than 1, then `E` is a strictly convex space over the real numbers. In other words, it's enough to check this condition for points of norm 1 and some `a`, `b` that add up to 1 to conclude that the space is strictly convex.
More concisely: If a normed additively commutative group equipped with a real norm satisfies the condition that for any distinct elements of norm 1 there exist strict positive real coefficients adding up to 1 such that their linear combination has norm strictly less than 1, then the space is strictly convex.
|
not_sameRay_iff_norm_add_lt
theorem not_sameRay_iff_norm_add_lt :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : StrictConvexSpace ℝ E]
{x y : E}, ¬SameRay ℝ x y ↔ ‖x + y‖ < ‖x‖ + ‖y‖
In a strictly convex space, the theorem states that two vectors `x` and `y` are not on the same ray if and only if the triangle inequality for `x` and `y` is strictly satisfied. That is, the norm of the sum of the vectors `x` and `y` is strictly less than the sum of their individual norms. This is written mathematically as: ‖x + y‖ < ‖x‖ + ‖y‖. Here, a strictly convex space is a vector space equipped with a norm that fulfills certain properties related to convexity. The concept of vectors being on the "same ray" is defined as either one of the vectors being zero or that there exist positive multiples of the vectors that are equal.
More concisely: In a strictly convex space, two vectors are not on the same ray if and only if their sum has a strictly smaller norm than the sum of their individual norms.
|
combo_mem_ball_of_ne
theorem combo_mem_ball_of_ne :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : StrictConvexSpace ℝ E]
{x y z : E} {a b r : ℝ},
x ∈ Metric.closedBall z r →
y ∈ Metric.closedBall z r → x ≠ y → 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ Metric.ball z r
This theorem states that in a real normed space with a strict convex structure, if two distinct points `x` and `y` belong to the same closed ball centered at `z` with radius `r`, then any convex combination of `x` and `y` with positive coefficients that sum up to 1 lies in the open ball centered at `z` with the same radius `r`. A convex combination of `x` and `y` is any point that can be obtained by `a * x + b * y` where `a` and `b` are positive real numbers such that `a + b = 1`.
More concisely: In a strict convex real normed space, if two distinct points belong to the same closed ball, then any convex combination of them with positive coefficients summing to 1 lies in the smaller open ball with the same radius.
|
strictConvex_closedBall
theorem strictConvex_closedBall :
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedLinearOrderedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : StrictConvexSpace 𝕜 E] (x : E) (r : ℝ),
StrictConvex 𝕜 (Metric.closedBall x r)
The theorem `strictConvex_closedBall` states that for every normed linear ordered field `𝕜`, and for any type `E` that forms a normed add commutative group and a normed space over `𝕜`, and which is additionally a strictly convex space, any closed ball in `E` centered at a point `x` with radius `r` is strictly convex. Here, a set in `E` is strictly convex if for any two distinct points in the set, the open line segment connecting them lies entirely within the set's interior. A closed ball in `E` is the set of all points whose distance to `x` is less than or equal to `r`.
More concisely: In a strictly convex normed linear ordered field `𝕜`, a closed ball in a strictly convex normed add commutative group and normed space `E` over `𝕜` is strictly convex.
|
openSegment_subset_ball_of_ne
theorem openSegment_subset_ball_of_ne :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : StrictConvexSpace ℝ E]
{x y z : E} {r : ℝ},
x ∈ Metric.closedBall z r → y ∈ Metric.closedBall z r → x ≠ y → openSegment ℝ x y ⊆ Metric.ball z r
The theorem `openSegment_subset_ball_of_ne` states that for any three points `x`, `y`, and `z` in a strictly convex space over the reals, where the space is also a normed additively commutative group and a normed space over reals, and for any real number `r`, if `x` and `y` are different and both belong to the same closed ball centered at `z` with radius `r`, then the open segment with `x` and `y` as endpoints is contained within the open ball centered at `z` with radius `r`.
In other words, if two different points are within a certain "closed" distance (inclusive) from a center point, then all points on the line segment between these two points (excluding the endpoints) are within a certain "open" distance (exclusive) from the same center point.
More concisely: If two distinct points in a strictly convex, normed additive commutative group over the reals lie in the closed ball of radius r around a center point, then the open segment connecting them is contained in the open ball of radius r around the center point.
|
norm_combo_lt_of_ne
theorem norm_combo_lt_of_ne :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : StrictConvexSpace ℝ E] {x y : E}
{a b r : ℝ}, ‖x‖ ≤ r → ‖y‖ ≤ r → x ≠ y → 0 < a → 0 < b → a + b = 1 → ‖a • x + b • y‖ < r
This theorem states that for any two distinct vectors `x` and `y` in a strict convex space over the real numbers, if both vectors have a norm no greater than `r`, and if `a` and `b` are positive real numbers that sum to 1, then the norm of the convex combination `a • x + b • y` (where `•` represents scalar multiplication) is strictly less than `r`. In other words, a convex combination of two distinct vectors with norms no greater than a given value, using positive coefficients that sum to 1, will result in a vector with a norm strictly less than that given value.
More concisely: Given two distinct vectors in a strict convex real inner product space with norms no greater than r, and positive coefficients a and b summing to 1, the norm of their convex combination a * x + b * y is strictly less than r.
|
sameRay_iff_norm_add
theorem sameRay_iff_norm_add :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : StrictConvexSpace ℝ E]
{x y : E}, SameRay ℝ x y ↔ ‖x + y‖ = ‖x‖ + ‖y‖
In a strictly convex space, two vectors `x` and `y` are considered to be in the same ray if and only if the triangle inequality for `x` and `y` turns into an equality. That is, the length (or norm) of the sum of `x` and `y` is equal to the sum of the lengths (or norms) of `x` and `y`. This forms the basis of the theorem `sameRay_iff_norm_add`.
In a more formal mathematical language, for vectors `x` and `y` in a strictly convex space `E`, the vectors are in the same ray (as defined by the `SameRay` function) if and only if the norm of `x + y` (`‖x + y‖`) is equal to the sum of the norms of `x` and `y` (`‖x‖ + ‖y‖`).
More concisely: In a strictly convex space, two vectors are in the same ray if and only if their sum has the same norm as the sum of their individual norms.
|
norm_add_lt_of_not_sameRay
theorem norm_add_lt_of_not_sameRay :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : StrictConvexSpace ℝ E]
{x y : E}, ¬SameRay ℝ x y → ‖x + y‖ < ‖x‖ + ‖y‖
In a strictly convex space, the theorem `norm_add_lt_of_not_sameRay` states that if two vectors `x` and `y` are not in the same ray, meaning they are not multiples of each other or one of them is not a zero vector, then the norm (or length) of the vector resulting from their addition is less than the sum of their individual norms. In mathematical terms, it means if `x` and `y` are not in the same ray, then $‖x + y‖ < ‖x‖ + ‖y‖$.
More concisely: In a strictly convex space, if two vectors are not in the same ray, then their sum has a strictly smaller norm than the sum of their individual norms.
|
eq_of_norm_eq_of_norm_add_eq
theorem eq_of_norm_eq_of_norm_add_eq :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : StrictConvexSpace ℝ E]
{x y : E}, ‖x‖ = ‖y‖ → ‖x + y‖ = ‖x‖ + ‖y‖ → x = y
This theorem states that if `x` and `y` are two vectors in a strictly convex space and they have the same norm (length), and if the norm of their sum is equal to the sum of their norms, then the vectors `x` and `y` are equal. This is a property specific to strictly convex spaces and is an application of the triangle inequality. Note that the proof of this theorem is not provided here.
More concisely: In a strictly convex space, if two vectors of equal norm have a sum with the same norm as their individual norms, then they are equal.
|