English
Let x and y be vectors in an inner product space; then the modulus of their inner product is bounded by the product of their norms: |⟪x, y⟫| ≤ ‖x‖‖y‖.
Русский
Пусть x и y — векторы внутри скалярного произведения; тогда модуль скалярного произведения ограничен произведением норм: |⟪x, y⟫| ≤ ‖x‖‖y‖.
LaTeX
$$$|\langle x,y\rangle| \le \|x\| \|y\|$$$
Lean4
/-- **Cauchy–Schwarz inequality**.
We need this for the `PreInnerProductSpace.Core` structure to prove the triangle inequality below
when showing the core is a normed group and to take the quotient.
(This is not intended for general use; see `Analysis.InnerProductSpace.Basic` for a variety of
versions of Cauchy-Schwartz for an inner product space, rather than a `PreInnerProductSpace.Core`).
-/
theorem inner_mul_inner_self_le (x y : F) : ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖ ≤ re ⟪x, x⟫ * re ⟪y, y⟫ :=
by
suffices discrim (normSqF x) (2 * ‖⟪x, y⟫_𝕜‖) (normSqF y) ≤ 0
by
rw [norm_inner_symm y x]
rw [discrim, normSq, normSq, sq] at this
linarith
refine discrim_le_zero fun t ↦ ?_
by_cases hzero : ⟪x, y⟫ = 0
· simp only [← sq, hzero, norm_zero, mul_zero, zero_mul, add_zero]
obtain ⟨hx, hy⟩ : (0 ≤ normSqF x ∧ 0 ≤ normSqF y) := ⟨inner_self_nonneg, inner_self_nonneg⟩
positivity
· have hzero' : ‖⟪x, y⟫‖ ≠ 0 := norm_ne_zero_iff.2 hzero
convert cauchy_schwarz_aux' (𝕜 := 𝕜) (⟪x, y⟫ • x) y (t / ‖⟪x, y⟫‖) using 3
· field_simp
rw [normSq, normSq, inner_smul_right, inner_smul_left, ← mul_assoc _ _ ⟪x, x⟫, mul_conj]
rw [← ofReal_pow, re_ofReal_mul]
ring
· field_simp
rw [inner_smul_left, mul_comm _ ⟪x, y⟫_𝕜, mul_conj, ← ofReal_pow, ofReal_re]
ring
