eLpNorm_aeeqFun — Mathlib

English

For MemLp f p μ, the eLpNorm of its AEEqFun.mk representation is finite: eLpNorm (AEEqFun.mk f hfp.1) p μ < ∞.

Русский

Для MemLp f p μ нормa eLpNorm(AEEqFun.mk f) конечна: eLpNorm(AEEqFun.mk f) p μ < ∞.

LaTeX

$$eLpNorm (AEEqFun.mk f hfp.1) p μ < ∞$$

Lean4

@[simp]
theorem eLpNorm_aeeqFun {α E : Type*} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] {p : ℝ≥0∞} {f : α → E}
    (hf : AEStronglyMeasurable f μ) : eLpNorm (AEEqFun.mk f hf) p μ = eLpNorm f p μ :=
  eLpNorm_congr_ae (AEEqFun.coeFn_mk _ _)

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