English
For any x,y ∈ E with x ≠ 0, the equality ‖⟪x,y⟫‖ / (‖x‖ ∥y∥) = 1 holds iff there exists r ∈ 𝕜 with y = r x and r ≠ 0.
Русский
Для любых x ≠ 0, y ∈ E равенство ∥⟪x,y⟫∥ / (∥x∥ ∥y∥) = 1 имеет место тогда, когда ∃ r ∈ 𝕜: y = r x и r ≠ 0.
LaTeX
$$$‖⟪x,y⟫‖/(‖x‖ \cdot ‖y‖) = 1 \iff x ≠ 0 ∧ ∃ r \; (r ≠ 0 ∧ y = r x)$$$
Lean4
/-- The inner product of two vectors, divided by the product of their
norms, has absolute value 1 if and only if they are nonzero and one is
a multiple of the other. One form of equality case for Cauchy-Schwarz. -/
theorem norm_inner_div_norm_mul_norm_eq_one_iff (x y : E) :
‖⟪x, y⟫ / (‖x‖ * ‖y‖)‖ = 1 ↔ x ≠ 0 ∧ ∃ r : 𝕜, r ≠ 0 ∧ y = r • x :=
by
constructor
· intro h
have hx₀ : x ≠ 0 := fun h₀ => by simp [h₀] at h
have hy₀ : y ≠ 0 := fun h₀ => by simp [h₀] at h
refine ⟨hx₀, (norm_inner_eq_norm_iff hx₀ hy₀).1 <| eq_of_div_eq_one ?_⟩
simpa using h
· rintro ⟨hx, ⟨r, ⟨hr, rfl⟩⟩⟩
simp only [norm_div, norm_mul, norm_ofReal, abs_norm]
exact norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr
