apply_sq_le_of_symm — Mathlib

English

For a symmetric bilinear form B, the CS inequality can be expressed as (B x y)^2 ≤ (B x x)(B y y).

Русский

Для симметричной билинейной формы выполняется неравенство Коши–Шварца: (B x y)^2 ≤ (B x x)(B y y).

LaTeX

$$$(B x y)^2 \\le (B x x)(B y y)$$$

Lean4

/-- The **Cauchy-Schwarz inequality** for positive semidefinite symmetric forms. -/
theorem apply_sq_le_of_symm (hs : ∀ x, 0 ≤ B x x) (hB : B.IsSymm) (x y : M) : (B x y) ^ 2 ≤ (B x x) * (B y y) :=
  by
  rw [show (B x y) ^ 2 = (B x y) * (B y x) by rw [sq, ← hB.eq, RingHom.id_apply]]
  exact apply_mul_apply_le_of_forall_zero_le B hs x y

Похожие утверждения