essSup_map_measure — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem essSup_map_measure (hf : MeasurableEmbedding f) : essSup g (Measure.map f μ) = essSup (g ∘ f) μ :=
  by
  refine le_antisymm ?_ (essSup_comp_le_essSup_map_measure hf.measurable.aemeasurable)
  refine limsSup_le_limsSup (by isBoundedDefault) (by isBoundedDefault) (fun c h_le => ?_)
  rw [eventually_map] at h_le ⊢
  exact hf.ae_map_iff.mpr h_le

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