Commit 2023-05-09 19:44 9042f7bc

View on Github →

feat: port MeasureTheory.Measure.AEMeasurable (#3819)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/AEMeasurable.lean

added theorem AEMeasurable.add_measure

added theorem AEMeasurable.ae_inf_principal_eq_mk

added theorem AEMeasurable.ae_mem_imp_eq_mk

added theorem AEMeasurable.comp_aemeasurable

added theorem AEMeasurable.comp_measurable

added theorem AEMeasurable.comp_quasiMeasurePreserving

added theorem AEMeasurable.exists_ae_eq_range_subset

added theorem AEMeasurable.exists_measurable_nonneg

added theorem AEMeasurable.indicator

added theorem AEMeasurable.map_map_of_aemeasurable

added theorem AEMeasurable.mono_measure

added theorem AEMeasurable.mono_set

added theorem AEMeasurable.prod_mk

added theorem AEMeasurable.restrict

added theorem AEMeasurable.smul_measure

added theorem AEMeasurable.subtype_mk

added theorem AEMeasurable.sum_measure

added theorem MeasurableEmbedding.aemeasurable_comp_iff

added theorem MeasurableEmbedding.aemeasurable_map_iff

added theorem MeasureTheory.Measure.map_mono_of_aemeasurable

added theorem MeasureTheory.Measure.restrict_map_of_aemeasurable

added theorem Subsingleton.aemeasurable

added theorem aemeasurable_Ioi_of_forall_Ioc

added theorem aemeasurable_add_measure_iff

added theorem aemeasurable_const'

added theorem aemeasurable_iff_measurable

added theorem aemeasurable_indicator_iff

added theorem aemeasurable_map_equiv_iff

added theorem aemeasurable_of_aemeasurable_trim

added theorem aemeasurable_of_subsingleton_codomain

added theorem aemeasurable_one

added theorem aemeasurable_restrict_iff_comap_subtype

added theorem aemeasurable_restrict_of_measurable_subtype

added theorem aemeasurable_smul_measure_iff

added theorem aemeasurable_sum_measure_iff

added theorem aemeasurable_uIoc_iff

added theorem aemeasurable_union_iff

added theorem aemeasurable_unionᵢ_iff

added theorem aemeasurable_zero_measure