abs_wInner_le — Mathlib

English

The absolute value of the weighted inner product is bounded by the inner product of the absolute values coordinatewise: |⟪f,g⟫_{𝕜,w}| ≤ ⟪|f|, |g|⟫_{ℝ,w}.

Русский

Модуль взвешенного скалярного произведения ≤ взвешенное произведение модулей по координатам.

LaTeX

$$|⟪f,g⟫_{ℝ?} ≤ ⟪|f|, |g|⟫_{ℝ,w}$$

Lean4

theorem abs_wInner_le (hw : 0 ≤ w) : |⟪f, g⟫_[ℝ, w]| ≤ ⟪|f|, |g|⟫_[ℝ, w] := by simpa using norm_wInner_le (𝕜 := ℝ) hw

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