norm_inner_le_norm — Mathlib

English

The inner product is bounded by the product of norms: ‖⟪x,y⟫‖ ≤ ‖x‖‖y‖.

Русский

Скалярное произведение ограничено произведением норм: ‖⟪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 : F) : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ :=
  nonneg_le_nonneg_of_sq_le_sq (mul_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) <|
    calc
      ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ = ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖ := by rw [norm_inner_symm]
      _ ≤ re ⟪x, x⟫ * re ⟪y, y⟫ := (inner_mul_inner_self_le x y)
      _ = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖) := by simp only [inner_self_eq_norm_mul_norm]; ring

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