Commit 2023-05-21 14:20 3c3ab91d

View on Github →

feat: port MeasureTheory.Function.EssSup (#4098)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/EssSup.lean

added theorem ENNReal.ae_le_essSup

added theorem ENNReal.coe_essSup

added theorem ENNReal.essSup_add_le

added theorem ENNReal.essSup_const_mul

added theorem ENNReal.essSup_eq_zero_iff

added theorem ENNReal.essSup_liminf_le

added theorem ENNReal.essSup_mul_le

added theorem MeasurableEmbedding.essSup_map_measure

added theorem OrderIso.essInf_apply

added theorem OrderIso.essSup_apply

added theorem ae_essInf_le

added theorem ae_le_essSup

added theorem ae_lt_of_essSup_lt

added theorem ae_lt_of_lt_essInf

added def essInf

added theorem essInf_antitone_measure

added theorem essInf_congr_ae

added theorem essInf_const'

added theorem essInf_const

added theorem essInf_const_top

added theorem essInf_eq_sSup

added theorem essInf_measure_zero

added theorem essInf_mono_ae

added def essSup

added theorem essSup_comp_le_essSup_map_measure

added theorem essSup_congr_ae

added theorem essSup_const'

added theorem essSup_const

added theorem essSup_const_bot

added theorem essSup_eq_sInf

added theorem essSup_indicator_eq_essSup_restrict

added theorem essSup_le_of_ae_le

added theorem essSup_map_measure

added theorem essSup_map_measure_of_measurable

added theorem essSup_measure_zero

added theorem essSup_mono_ae

added theorem essSup_mono_measure'

added theorem essSup_mono_measure

added theorem essSup_smul_measure

added theorem le_essInf_of_ae_le

added theorem meas_essSup_lt

added theorem meas_lt_essInf