norm_inner_le_norm — Mathlib

English

Let E be an inner product space. For all vectors x, y in E, the modulus of their inner product is bounded by the product of their norms: |⟪x, y⟫| ≤ ∥x∥ ∥y∥.

Русский

Пусть E является пространством с скалярным произведением. Для любых векторов x, y ∈ E выполняется неравенство модуля скалярного произведения: |⟪x, y⟫| ≤ ∥x∥ ∥y∥.

LaTeX

$$$|\langle x,y\rangle| \le \|x\| \|y\|$$$

Lean4

/-- Cauchy–Schwarz inequality with norm -/
theorem norm_inner_le_norm (x y : E) : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ :=
  by
  rw [norm_eq_sqrt_re_inner (𝕜 := 𝕜) x, norm_eq_sqrt_re_inner (𝕜 := 𝕜) y]
  letI : PreInnerProductSpace.Core 𝕜 E := PreInnerProductSpace.toCore
  exact InnerProductSpace.Core.norm_inner_le_norm x y

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