norm_eq_tsum_rpow — Mathlib

English

If hp : 0 < p.toReal, then the lp-norm satisfies ‖f‖ = (∑' i, ‖f i‖^{p.toReal})^{1/p.toReal}.

Русский

Пусть hp : 0 < p.toReal. Тогда норма lp удовлетворяет ‖f‖ = (∑' i ‖f_i‖^{p.toReal})^{1/p.toReal}.

LaTeX

$$$$ \|f\| = \left( \sum_i \|f_i\|^{p^{\mathrm{toReal}}} \right)^{1/p^{\mathrm{toReal}}}, \quad \text{если } 0 < p^{\mathrm{toReal}}. $$$$

Lean4

theorem norm_eq_tsum_rpow (hp : 0 < p.toReal) (f : lp E p) : ‖f‖ = (∑' i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal) :=
  by
  dsimp [norm]
  rw [ENNReal.toReal_pos_iff] at hp
  rw [dif_neg hp.1.ne', if_neg hp.2.ne]

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