essSup_map_measure_of_measurable — Mathlib

English

If g is an order isomorphism, then g applied to the essential infimum equals the essential infimum of the composed map: g (essInf f μ) = essInf (g ∘ f) μ.

Русский

Если g — изоморфизм порядка, то g(essInf f μ) = essInf (g ∘ f) μ.

LaTeX

$$$$ g(\\operatorname{essInf} f \\mu) = \\operatorname{essInf} (g \\circ f) \\mu $$$$

Lean4

theorem essSup_map_measure_of_measurable (hg : Measurable g) (hf : AEMeasurable f μ) :
    essSup g (Measure.map f μ) = essSup (g ∘ f) μ :=
  by
  refine le_antisymm ?_ (essSup_comp_le_essSup_map_measure hf)
  refine limsSup_le_limsSup (by isBoundedDefault) (by isBoundedDefault) (fun c h_le => ?_)
  rw [eventually_map] at h_le ⊢
  rw [ae_map_iff hf (measurableSet_le hg measurable_const)]
  exact h_le

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