inner_eq_wInner_one — Mathlib

English

The norm of the weighted inner product is bounded above by the weighted inner product of coordinatewise norms: ‖⟪f,g⟫⟖ ≤ ⟪|f|, |g|⟫.

Русский

Норма взвешенного скалярного произведения не превосходит взвешенное произведение норм по координатам.

LaTeX

$$‖⟪f,g⟫⟖ ≤ ⟪|f|, |g|⟫$$

Lean4

theorem inner_eq_wInner_one (f g : PiLp 2 fun _i : ι ↦ 𝕜) : ⟪f, g⟫_𝕜 = ⟪WithLp.ofLp f, WithLp.ofLp g⟫_[𝕜, 1] := by
  simp [PiLp.inner_apply, wInner]

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