English
A formulation that strict convexity of the space is equivalent to the unit-norm convex combinations of unit vectors; more precisely, for any unit vectors x,y with x≠y there exist a,b >0 with a+b=1 such that ∥a x + b y∥ < 1, which characterizes strict convexity.
Русский
Строгое выпуклость пространства эквивалентна свойству, что любые два различных векторы единичной нормы дают расходящийся по норме выпуклый комбинирование с нормой меньше 1; это характеристика строгой выпуклости.
LaTeX
$$$\bigl(\forall x,y:\ E,\ \|x\|=\|y\|=1,\ x\neq y\Rightarrow \exists a,b\in\mathbb{R}, a\ge 0,b\ge 0, a+b=1,\ \|a x + b y\| < 1\bigr) \Rightarrow \ StrictConvexSpace_{\mathbb{R}} E$$$
Lean4
/-- Strict convexity is equivalent to `‖a • x + b • y‖ < 1` for all `x` and `y` of norm at most `1`
and all strictly positive `a` and `b` such that `a + b = 1`. This lemma shows that it suffices to
check this for points of norm one and some `a`, `b` such that `a + b = 1`. -/
theorem of_norm_combo_lt_one (h : ∀ x y : E, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b : ℝ, a + b = 1 ∧ ‖a • x + b • y‖ < 1) :
StrictConvexSpace ℝ E :=
by
refine
StrictConvexSpace.of_strictConvex_unitClosedBall ℝ ((convex_closedBall _ _).strictConvex' fun x hx y hy hne => ?_)
rw [interior_closedBall (0 : E) one_ne_zero, closedBall_diff_ball, mem_sphere_zero_iff_norm] at hx hy
rcases h x y hx hy hne with ⟨a, b, hab, hlt⟩
use b
rwa [AffineMap.lineMap_apply_module, interior_closedBall (0 : E) one_ne_zero, mem_ball_zero_iff,
sub_eq_iff_eq_add.2 hab.symm]
