inner_mul_inner_self_le — Mathlib

English

The Cauchy–Schwarz inequality holds: ‖⟪x,y⟫‖ · ‖⟪y,x⟫‖ ≤ Re ⟪x,x⟫ · Re ⟪y,y⟫.

Русский

Неравенство Коши–Лайс: ‖⟪x,y⟫‖ · ‖⟪y,x⟫‖ ≤ Re ⟪x,x⟫ · Re ⟪y,y⟫.

LaTeX

$$$\|\langle x, y \rangle\| \cdot \|\langle y, x \rangle\| \le \operatorname{Re}\langle x, x \rangle \cdot \operatorname{Re}\langle y, y \rangle$$$

Lean4

/-- **Cauchy–Schwarz inequality**. -/
theorem inner_mul_inner_self_le (x y : E) : ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖ ≤ re ⟪x, x⟫ * re ⟪y, y⟫ :=
  letI : PreInnerProductSpace.Core 𝕜 E := PreInnerProductSpace.toCore
  InnerProductSpace.Core.inner_mul_inner_self_le x y

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