norm_rpow_eq_tsum — Mathlib

English

For hp > 0, the equality holds: ‖f‖^{p.toReal} = ∑' i, ‖f i‖^{p.toReal}.

Русский

Пусть hp > 0. Тогда выполняется равенство: ‖f‖^{p.toReal} = ∑' i ‖f_i‖^{p.toReal}.

LaTeX

$$$$ \|f\|^{p^{\mathrm{toReal}}} = \sum_i \|f_i\|^{p^{\mathrm{toReal}}}. $$$$

Lean4

theorem norm_rpow_eq_tsum (hp : 0 < p.toReal) (f : lp E p) : ‖f‖ ^ p.toReal = ∑' i, ‖f i‖ ^ p.toReal :=
  by
  rw [norm_eq_tsum_rpow hp, ← Real.rpow_mul]
  · field_simp
    simp
  apply tsum_nonneg
  intro i
  calc
    (0 : ℝ) = (0 : ℝ) ^ p.toReal := by rw [Real.zero_rpow hp.ne']
    _ ≤ _ := by gcongr; apply norm_nonneg

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