abs_real_inner_div_norm_mul_norm_le_one

English

Let x and y be vectors in a real inner product space. Then the absolute value of their real inner product divided by the product of their norms is at most 1, i.e. |⟨x,y⟩ℝ / (∥x∥ ∥y∥)| ≤ 1; equivalently |⟨x,y⟩ℝ| ≤ ∥x∥ ∥y∥.

Русский

Пусть x и y — векторы в вещественном скалярном произведении. Тогда |⟨x,y⟩ℝ| ≤ ∥x∥ ∥y∥, то есть |⟨x,y⟩ℝ / (∥x∥ ∥y∥)| ≤ 1.

LaTeX

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

Lean4

/-- The real inner product of two vectors, divided by the product of their
norms, has absolute value at most 1. -/
theorem abs_real_inner_div_norm_mul_norm_le_one (x y : F) : |⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)| ≤ 1 :=
  by
  rw [abs_div, abs_mul, abs_norm, abs_norm]
  exact div_le_one_of_le₀ (abs_real_inner_le_norm x y) (by positivity)

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