English
If for unit vectors x,y with x ≠ y there exist a,b ≥ 0 with a+b=1 such that ∥a x + b y∥ < 1, then the space is strictly convex.
Русский
Если для любых единичных векторов x и y с x ≠ y существует выпуклая комбинация с положительными коэффициентами, дающая норму меньше единицы, то пространство строго выпукло.
LaTeX
$$$\forall x,y:\ E, \|x\|=\|y\|=1, x\neq y \Rightarrow \exists a,b≥0, a+b=1: \|a x + b y\| < 1 \Rightarrow \ StrictConvexSpace_{\mathbb{R}} E$$$
Lean4
theorem of_norm_add_ne_two (h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2) : StrictConvexSpace ℝ E :=
by
refine
StrictConvexSpace.of_norm_combo_ne_one fun x y hx hy hne =>
⟨1 / 2, 1 / 2, one_half_pos.le, one_half_pos.le, add_halves _, ?_⟩
rw [← smul_add, norm_smul, Real.norm_of_nonneg one_half_pos.le, one_div, ← div_eq_inv_mul, Ne,
div_eq_one_iff_eq (two_ne_zero' ℝ)]
exact h hx hy hne
