abs_real_inner_le_norm — Mathlib

English

For all x, y in E, the absolute value of their inner product (over the real part) is bounded by the product of their norms: |⟪x,y⟫_ℝ| ≤ ∥x∥ ∥y∥.

Русский

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

LaTeX

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

Lean4

/-- Cauchy–Schwarz inequality with norm -/
theorem abs_real_inner_le_norm (x y : F) : |⟪x, y⟫_ℝ| ≤ ‖x‖ * ‖y‖ :=
  (Real.norm_eq_abs _).ge.trans (norm_inner_le_norm x y)

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