real_inner_mul_inner_self_le — Mathlib

English

For real inner products, ⟪x,y⟫_ℝ^2 ≤ ⟪x,x⟫_ℝ ⟪y,y⟫_ℝ, i.e. the standard Cauchy–Schwarz inequality in the real case.

Русский

Для вещественных скалярных произведений справедливо стандартное неравенство Коши–Лайска: ⟪x,y⟫_ℝ^2 ≤ ⟪x,x⟫_ℝ ⟪y,y⟫_ℝ.

LaTeX

$$$\langle x, y \rangle_\mathbb{R}^2 \le \langle x, x \rangle_\mathbb{R} \langle y, y \rangle_\mathbb{R}$$$

Lean4

/-- Cauchy–Schwarz inequality for real inner products. -/
theorem real_inner_mul_inner_self_le (x y : F) : ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ :=
  calc
    ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ‖⟪x, y⟫_ℝ‖ * ‖⟪y, x⟫_ℝ‖ :=
      by
      rw [real_inner_comm y, ← norm_mul]
      exact le_abs_self _
    _ ≤ ⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ := @inner_mul_inner_self_le ℝ _ _ _ _ x y

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