eLpNorm_eq_zero_iff — Mathlib

English

For AEStronglyMeasurable g and AEMeasurable f, the eLpNorm of g on Measure.map f μ equals that of g ∘ f on μ, when g is viewed as an AEEqFun.

Русский

Для AEStronglyMeasurable g и AEMeasurable f справедливо eLpNorm(g, p, Measure.map f μ) = eLpNorm(g ∘ f, p, μ).

LaTeX

$$eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ$$

Lean4

theorem eLpNorm_eq_zero_iff {f : α → ε} (hf : AEStronglyMeasurable f μ) (h0 : p ≠ 0) : eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0 :=
  by
  by_cases h_top : p = ∞
  · rw [h_top, eLpNorm_exponent_top, eLpNormEssSup_eq_zero_iff]
  rw [eLpNorm_eq_eLpNorm' h0 h_top]
  exact eLpNorm'_eq_zero_iff (ENNReal.toReal_pos h0 h_top) hf

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