English
The Cauchy–Schwarz inequality for positive semidefinite symmetric forms holds: (B x y)(B y x) ≤ (B x x)(B y y).
Русский
Неравенство Коши–Шварца для положительно полуопределённых симметричных форм: (B x y)(B y x) ≤ (B x x)(B y y).
LaTeX
$$$(B x y)(B y x) \\le (B x x)(B y y)$$$
Lean4
/-- The **Cauchy-Schwarz inequality** for positive semidefinite forms. -/
theorem apply_mul_apply_le_of_forall_zero_le (hs : ∀ x, 0 ≤ B x x) (x y : M) : (B x y) * (B y x) ≤ (B x x) * (B y y) :=
by
have aux (x y : M) : 0 ≤ (B x x) * ((B x x) * (B y y) - (B x y) * (B y x)) :=
by
rw [← apply_smul_sub_smul_sub_eq B x y]
exact hs (B x y • x - B x x • y)
rcases lt_or_ge 0 (B x x) with hx | hx
· exact sub_nonneg.mp <| nonneg_of_mul_nonneg_right (aux x y) hx
· replace hx : B x x = 0 := le_antisymm hx (hs x)
rcases lt_or_ge 0 (B y y) with hy | hy
· rw [mul_comm (B x y), mul_comm (B x x)]
exact sub_nonneg.mp <| nonneg_of_mul_nonneg_right (aux y x) hy
· replace hy : B y y = 0 := le_antisymm hy (hs y)
suffices B x y = -B y x by simpa [this, hx, hy] using mul_self_nonneg (B y x)
rw [eq_neg_iff_add_eq_zero]
apply le_antisymm
· simpa [hx, hy, le_neg_iff_add_nonpos_left] using hs (x - y)
· simpa [hx, hy] using hs (x + y)
