English
In a strictly convex space, if x and y are not in the same ray, then ∥x+y∥ < ∥x∥ + ∥y∥.
Русский
В строго выпуклом пространстве, если векторы x и y не лежат на одном луче, то ∥x+y∥ < ∥x∥ + ∥y∥.
LaTeX
$$$\lnot \mathrm{SameRay}(x,y) \Rightarrow \|x+y\| < \|x\| + \|y\|.$$$
Lean4
/-- In a strictly convex space, if `x` and `y` are not in the same ray, then `‖x + y‖ < ‖x‖ + ‖y‖`.
-/
theorem norm_add_lt_of_not_sameRay (h : ¬SameRay ℝ x y) : ‖x + y‖ < ‖x‖ + ‖y‖ :=
by
simp only [sameRay_iff_inv_norm_smul_eq, not_or, ← Ne.eq_def] at h
rcases h with ⟨hx, hy, hne⟩
rw [← norm_pos_iff] at hx hy
have hxy : 0 < ‖x‖ + ‖y‖ := add_pos hx hy
have :=
combo_mem_ball_of_ne (inv_norm_smul_mem_unitClosedBall x) (inv_norm_smul_mem_unitClosedBall y) hne (div_pos hx hxy)
(div_pos hy hxy) (by rw [← add_div, div_self hxy.ne'])
rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ← div_eq_inv_mul,
div_lt_one hxy] at this
