Commit 2026-05-14 06:13 e9da88d7

View on Github →

feat(MeasureTheory): generalize some lemmas about essSup to conditionally complete lattices (#39104) The motivation for this PR is to show that if a random variable is in $L^\infty$, then so is it conditional expectation (proved in #36888). Created with the help of Codex.

Estimated changes

Modified Mathlib/MeasureTheory/Function/EssSup.lean

modified theorem MeasurableEmbedding.essSup_map_measure

modified theorem OrderIso.essInf_apply

modified theorem OrderIso.essSup_apply

modified theorem essInf_antitone_measure

modified theorem essInf_mono_ae

modified theorem essSup_comp_le_essSup_map_measure

modified theorem essSup_le_of_ae_le

modified theorem essSup_map_measure

modified theorem essSup_map_measure_of_measurable

modified theorem essSup_mono_ae

modified theorem essSup_mono_measure'

modified theorem essSup_mono_measure

modified theorem le_essInf_of_ae_le