Commit 2024-05-28 14:16 5e475e24

View on Github →

feat(MeasureTheory): generalize ae to OuterMeasureClass (#13022)

Move definition and some lemmas from MeasureSpaceDef to OuterMeasure.AE.
Rename MeasureTheory.Measure.ae to MeasureTheory.ae.
Generalize the definition and theorems to [OuterMeasureClass _ _]. See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.22Almost.20every.22.20on.20outer.20measures and https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Order.20on.20measures/near/425729507

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Dynamics/Ergodic/Conservative.lean

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

modified theorem MeasureTheory.Measure.ae_pi_le_pi

modified theorem MeasureTheory.Measure.tendsto_eval_ae_ae

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

modified def MeasureTheory.AEEqFun.toGerm

modified def MeasureTheory.AEEqFun.toGermMonoidHom

modified theorem MeasureTheory.AEEqFun.toGerm_injective

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

Modified Mathlib/MeasureTheory/Function/EssSup.lean

modified theorem ENNReal.coe_essSup

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

modified theorem AEMeasurable.ae_inf_principal_eq_mk

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

modified theorem MeasureTheory.ae_dirac_eq

modified theorem MeasureTheory.mem_ae_dirac_iff

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem MeasurableEquiv.map_ae

modified theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae_map_le

modified theorem MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae

modified theorem MeasureTheory.Measure.ae_le_iff_absolutelyContinuous

modified theorem MeasureTheory.Measure.ae_sum_eq

modified theorem MeasureTheory.Measure.tendsto_ae_map

modified theorem MeasureTheory.ae_eq_bot

modified theorem MeasureTheory.ae_mono

modified theorem MeasureTheory.ae_neBot

modified theorem MeasureTheory.ae_zero

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

deleted def MeasureTheory.Measure.ae

deleted theorem MeasureTheory.ae_all_iff

deleted theorem MeasureTheory.ae_ball_iff

deleted theorem MeasureTheory.ae_eq_empty

deleted theorem MeasureTheory.ae_eq_refl

deleted theorem MeasureTheory.ae_eq_set

deleted theorem MeasureTheory.ae_eq_set_compl

deleted theorem MeasureTheory.ae_eq_set_compl_compl

deleted theorem MeasureTheory.ae_eq_set_inter

deleted theorem MeasureTheory.ae_eq_set_union

deleted theorem MeasureTheory.ae_eq_symm

deleted theorem MeasureTheory.ae_eq_trans

deleted theorem MeasureTheory.ae_eq_univ

deleted theorem MeasureTheory.ae_iff

deleted theorem MeasureTheory.ae_iff_of_countable

deleted theorem MeasureTheory.ae_le_of_ae_lt

deleted theorem MeasureTheory.ae_le_set

deleted theorem MeasureTheory.ae_le_set_inter

deleted theorem MeasureTheory.ae_le_set_union

deleted theorem MeasureTheory.ae_of_all

deleted theorem MeasureTheory.all_ae_of

deleted theorem MeasureTheory.compl_mem_ae_iff

deleted theorem MeasureTheory.diff_ae_eq_self

deleted theorem MeasureTheory.diff_null_ae_eq_self

deleted theorem MeasureTheory.frequently_ae_iff

deleted theorem MeasureTheory.frequently_ae_mem_iff

deleted theorem MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_left

deleted theorem MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_right

deleted theorem MeasureTheory.inter_ae_eq_left_of_ae_eq_univ

deleted theorem MeasureTheory.inter_ae_eq_right_of_ae_eq_univ

deleted theorem MeasureTheory.measure_congr

deleted theorem MeasureTheory.measure_mono_ae

deleted theorem MeasureTheory.measure_mono_null_ae

deleted theorem MeasureTheory.measure_null_iff_singleton

deleted theorem MeasureTheory.measure_symmDiff_eq_zero_iff

deleted theorem MeasureTheory.measure_zero_iff_ae_nmem

deleted theorem MeasureTheory.mem_ae_iff

deleted theorem MeasureTheory.union_ae_eq_left_of_ae_eq_empty

deleted theorem MeasureTheory.union_ae_eq_right

deleted theorem MeasureTheory.union_ae_eq_right_of_ae_eq_empty

deleted theorem MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_left

deleted theorem MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_right

deleted theorem Set.mulIndicator_ae_eq_one

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

modified theorem MeasureTheory.Measure.ae_completion

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

modified theorem MeasureTheory.ae_restrict_eq

modified theorem MeasureTheory.ae_restrict_eq_bot

modified theorem MeasureTheory.ae_restrict_neBot

modified theorem MeasureTheory.le_ae_restrict

modified theorem MeasureTheory.self_mem_ae_restrict

Modified Mathlib/MeasureTheory/Measure/Trim.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

modified theorem MeasureTheory.IsProbabilityMeasure.ae_neBot

modified theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono_ae

modified theorem MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff

modified theorem MeasureTheory.mem_ae_iff_prob_eq_one

modified theorem MeasureTheory.mem_ae_iff_prob_eq_one₀

Created Mathlib/MeasureTheory/OuterMeasure/AE.lean

added def MeasureTheory.ae

added theorem MeasureTheory.ae_all_iff

added theorem MeasureTheory.ae_ball_iff

added theorem MeasureTheory.ae_eq_empty

added theorem MeasureTheory.ae_eq_refl

added theorem MeasureTheory.ae_eq_set

added theorem MeasureTheory.ae_eq_set_compl

added theorem MeasureTheory.ae_eq_set_compl_compl

added theorem MeasureTheory.ae_eq_set_inter

added theorem MeasureTheory.ae_eq_set_union

added theorem MeasureTheory.ae_eq_symm

added theorem MeasureTheory.ae_eq_trans

added theorem MeasureTheory.ae_eq_univ

added theorem MeasureTheory.ae_iff

added theorem MeasureTheory.ae_iff_of_countable

added theorem MeasureTheory.ae_le_of_ae_lt

added theorem MeasureTheory.ae_le_set

added theorem MeasureTheory.ae_le_set_inter

added theorem MeasureTheory.ae_le_set_union

added theorem MeasureTheory.ae_of_all

added theorem MeasureTheory.all_ae_of

added theorem MeasureTheory.compl_mem_ae_iff

added theorem MeasureTheory.diff_ae_eq_self

added theorem MeasureTheory.diff_null_ae_eq_self

added theorem MeasureTheory.frequently_ae_iff

added theorem MeasureTheory.frequently_ae_mem_iff

added theorem MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_left

added theorem MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_right

added theorem MeasureTheory.inter_ae_eq_left_of_ae_eq_univ

added theorem MeasureTheory.inter_ae_eq_right_of_ae_eq_univ

added theorem MeasureTheory.measure_congr

added theorem MeasureTheory.measure_mono_ae

added theorem MeasureTheory.measure_mono_null_ae

added theorem MeasureTheory.measure_symmDiff_eq_zero_iff

added theorem MeasureTheory.measure_zero_iff_ae_nmem

added theorem MeasureTheory.mem_ae_iff

added theorem MeasureTheory.union_ae_eq_left_of_ae_eq_empty

added theorem MeasureTheory.union_ae_eq_right

added theorem MeasureTheory.union_ae_eq_right_of_ae_eq_empty

added theorem MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_left

added theorem MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_right

added theorem Set.mulIndicator_ae_eq_one

Modified Mathlib/MeasureTheory/OuterMeasure/Basic.lean

added theorem MeasureTheory.measure_null_iff_singleton

Modified Mathlib/NumberTheory/Liouville/Measure.lean

modified theorem Real.disjoint_residual_ae

Modified Mathlib/NumberTheory/WellApproximable.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/Filter/CountableInter.lean

Modified Mathlib/Order/Filter/CountableSeparatingOn.lean

Modified Mathlib/Probability/Variance.lean

Modified docs/overview.yaml

Modified docs/undergrad.yaml