essSup_map_measure — Mathlib

English

If ν is absolutely continuous with respect to μ, then essSup f ν ≤ essSup f μ.

Русский

Если ν абсолютно непрерывна по отношению к μ, то essSup f ν ≤ essSup f μ.

LaTeX

$$$$ \\operatorname{essSup} f \\nu \\le \\operatorname{essSup} f \\mu \\quad \\text{if } \\nu \\ll \\mu $$$$

Lean4

theorem essSup_map_measure (hg : AEMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
    essSup g (Measure.map f μ) = essSup (g ∘ f) μ :=
  by
  rw [essSup_congr_ae hg.ae_eq_mk, essSup_map_measure_of_measurable hg.measurable_mk hf]
  refine essSup_congr_ae ?_
  have h_eq := ae_of_ae_map hf hg.ae_eq_mk
  rw [← EventuallyEq] at h_eq
  exact h_eq.symm

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