eLpNormEssSup_map_measure — Mathlib

English

If f is a measurable embedding, then eLpNorm g on Measure.map f μ equals eLpNorm (g ∘ f) μ.

Русский

Если f — измеримое вложение, то eLpNorm g на Measure.map f μ равно eLpNorm (g ∘ f) μ.

LaTeX

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

Lean4

theorem eLpNormEssSup_map_measure (hg : AEStronglyMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
    eLpNormEssSup g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ :=
  essSup_map_measure hg.enorm hf

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