Commit 2025-01-31 17:41 ea8f1b04

View on Github →

chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273) Separate MeasureTheory/Function/StronglyMeasurable/Basic into a file Basic which contains everything about StronglyMeasurable and FinStronglyMeasurable and a file AEStronglyMeasurable which is about AEStronglyMeasurable and FinAEStronglyMeasurable. I am not sure about the split of the doc.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

Modified Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean

Created Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

added theorem AEMeasurable.aestronglyMeasurable

added theorem Continuous.aestronglyMeasurable

added theorem Continuous.comp_aestronglyMeasurable

added theorem Continuous.comp_aestronglyMeasurable₂

added theorem Finset.aestronglyMeasurable_prod'

added theorem Finset.aestronglyMeasurable_prod

added theorem List.aestronglyMeasurable_prod'

added theorem List.aestronglyMeasurable_prod

added theorem Measurable.aestronglyMeasurable

added theorem MeasurableEmbedding.aestronglyMeasurable_map_iff

added theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk

added theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_compl

added theorem MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite

added theorem MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk

added def MeasureTheory.AEFinStronglyMeasurable.sigmaFiniteSet

added def MeasureTheory.AEFinStronglyMeasurable

added theorem MeasureTheory.AEStronglyMeasurable.add_measure

added theorem MeasureTheory.AEStronglyMeasurable.ae_eq_mk

added theorem MeasureTheory.AEStronglyMeasurable.ae_mem_imp_eq_mk

added theorem MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff

added theorem MeasureTheory.AEStronglyMeasurable.comp_aemeasurable

added theorem MeasureTheory.AEStronglyMeasurable.comp_measurable

added theorem MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving

added theorem MeasureTheory.AEStronglyMeasurable.congr

added theorem MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range

added theorem MeasureTheory.AEStronglyMeasurable.measurable_mk

added theorem MeasureTheory.AEStronglyMeasurable.mono

added theorem MeasureTheory.AEStronglyMeasurable.mono_measure

added theorem MeasureTheory.AEStronglyMeasurable.mono_set

added theorem MeasureTheory.AEStronglyMeasurable.mul_iff_left

added theorem MeasureTheory.AEStronglyMeasurable.mul_iff_right

added theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_eq_fun

added theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_le

added theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_lt

added theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_mulSupport

added theorem MeasureTheory.AEStronglyMeasurable.of_finite

added theorem MeasureTheory.AEStronglyMeasurable.of_measurableSpace_le_on

added theorem MeasureTheory.AEStronglyMeasurable.of_subsingleton_cod

added theorem MeasureTheory.AEStronglyMeasurable.of_subsingleton_dom

added theorem MeasureTheory.AEStronglyMeasurable.of_trim

added theorem MeasureTheory.AEStronglyMeasurable.piecewise

added theorem MeasureTheory.AEStronglyMeasurable.smul_measure

added theorem MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk

added theorem MeasureTheory.AEStronglyMeasurable.sum_measure

added def MeasureTheory.AEStronglyMeasurable

added theorem MeasureTheory.FinStronglyMeasurable.aefinStronglyMeasurable

added theorem MeasureTheory.SimpleFunc.aestronglyMeasurable

added theorem MeasureTheory.Subsingleton.aestronglyMeasurable'

added theorem MeasureTheory.Subsingleton.aestronglyMeasurable

added theorem MeasureTheory.aefinStronglyMeasurable_iff_aemeasurable

added theorem MeasureTheory.aefinStronglyMeasurable_of_aemeasurable

added theorem MeasureTheory.aefinStronglyMeasurable_zero

added theorem MeasureTheory.aestronglyMeasurable_const

added theorem MeasureTheory.aestronglyMeasurable_one

added theorem MeasureTheory.aestronglyMeasurable_zero_measure

added theorem Multiset.aestronglyMeasurable_prod'

added theorem Multiset.aestronglyMeasurable_prod

added theorem Topology.IsEmbedding.aestronglyMeasurable_comp_iff

added theorem aestronglyMeasurable_add_measure_iff

added theorem aestronglyMeasurable_congr

added theorem aestronglyMeasurable_const_smul_iff

added theorem aestronglyMeasurable_const_smul_iff₀

added theorem aestronglyMeasurable_iUnion_iff

added theorem aestronglyMeasurable_id

added theorem aestronglyMeasurable_iff_aemeasurable

added theorem aestronglyMeasurable_iff_aemeasurable_separable

added theorem aestronglyMeasurable_iff_nullMeasurable_separable

added theorem aestronglyMeasurable_indicator_iff

added theorem aestronglyMeasurable_of_aestronglyMeasurable_trim

added theorem aestronglyMeasurable_of_tendsto_ae

added theorem aestronglyMeasurable_sum_measure_iff

added theorem aestronglyMeasurable_union_iff

added theorem exists_stronglyMeasurable_limit_of_tendsto_ae

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

deleted theorem AEMeasurable.aestronglyMeasurable

deleted theorem Continuous.aestronglyMeasurable

deleted theorem Continuous.comp_aestronglyMeasurable

deleted theorem Continuous.comp_aestronglyMeasurable₂

deleted theorem Finset.aestronglyMeasurable_prod'

deleted theorem Finset.aestronglyMeasurable_prod

deleted theorem List.aestronglyMeasurable_prod'

deleted theorem List.aestronglyMeasurable_prod

deleted theorem Measurable.aestronglyMeasurable

deleted theorem MeasurableEmbedding.aestronglyMeasurable_map_iff

deleted theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk

deleted theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_compl

deleted theorem MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite

deleted theorem MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk

deleted def MeasureTheory.AEFinStronglyMeasurable.sigmaFiniteSet

deleted def MeasureTheory.AEFinStronglyMeasurable

deleted theorem MeasureTheory.AEStronglyMeasurable.add_measure

deleted theorem MeasureTheory.AEStronglyMeasurable.ae_eq_mk

deleted theorem MeasureTheory.AEStronglyMeasurable.ae_mem_imp_eq_mk

deleted theorem MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff

deleted theorem MeasureTheory.AEStronglyMeasurable.comp_aemeasurable

deleted theorem MeasureTheory.AEStronglyMeasurable.comp_measurable

deleted theorem MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving

deleted theorem MeasureTheory.AEStronglyMeasurable.congr

deleted theorem MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range

deleted theorem MeasureTheory.AEStronglyMeasurable.measurable_mk

deleted theorem MeasureTheory.AEStronglyMeasurable.mono

deleted theorem MeasureTheory.AEStronglyMeasurable.mono_measure

deleted theorem MeasureTheory.AEStronglyMeasurable.mono_set

deleted theorem MeasureTheory.AEStronglyMeasurable.mul_iff_left

deleted theorem MeasureTheory.AEStronglyMeasurable.mul_iff_right

deleted theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_eq_fun

deleted theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_le

deleted theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_lt

deleted theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_mulSupport

deleted theorem MeasureTheory.AEStronglyMeasurable.of_finite

deleted theorem MeasureTheory.AEStronglyMeasurable.of_measurableSpace_le_on

deleted theorem MeasureTheory.AEStronglyMeasurable.of_subsingleton_cod

deleted theorem MeasureTheory.AEStronglyMeasurable.of_subsingleton_dom

deleted theorem MeasureTheory.AEStronglyMeasurable.of_trim

deleted theorem MeasureTheory.AEStronglyMeasurable.piecewise

deleted theorem MeasureTheory.AEStronglyMeasurable.smul_measure

deleted theorem MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk

deleted theorem MeasureTheory.AEStronglyMeasurable.sum_measure

deleted def MeasureTheory.AEStronglyMeasurable

deleted theorem MeasureTheory.FinStronglyMeasurable.aefinStronglyMeasurable

deleted theorem MeasureTheory.SimpleFunc.aestronglyMeasurable

deleted theorem MeasureTheory.Subsingleton.aestronglyMeasurable'

deleted theorem MeasureTheory.Subsingleton.aestronglyMeasurable

deleted theorem MeasureTheory.aefinStronglyMeasurable_iff_aemeasurable

deleted theorem MeasureTheory.aefinStronglyMeasurable_of_aemeasurable

deleted theorem MeasureTheory.aefinStronglyMeasurable_zero

deleted theorem MeasureTheory.aestronglyMeasurable_const

deleted theorem MeasureTheory.aestronglyMeasurable_one

deleted theorem MeasureTheory.aestronglyMeasurable_zero_measure

deleted theorem Multiset.aestronglyMeasurable_prod'

deleted theorem Multiset.aestronglyMeasurable_prod

deleted theorem Topology.IsEmbedding.aestronglyMeasurable_comp_iff

deleted theorem aestronglyMeasurable_add_measure_iff

deleted theorem aestronglyMeasurable_congr

deleted theorem aestronglyMeasurable_const_smul_iff

deleted theorem aestronglyMeasurable_const_smul_iff₀

deleted theorem aestronglyMeasurable_iUnion_iff

deleted theorem aestronglyMeasurable_id

deleted theorem aestronglyMeasurable_iff_aemeasurable

deleted theorem aestronglyMeasurable_iff_aemeasurable_separable

deleted theorem aestronglyMeasurable_iff_nullMeasurable_separable

deleted theorem aestronglyMeasurable_indicator_iff

deleted theorem aestronglyMeasurable_of_aestronglyMeasurable_trim

deleted theorem aestronglyMeasurable_of_tendsto_ae

deleted theorem aestronglyMeasurable_sum_measure_iff

deleted theorem aestronglyMeasurable_union_iff

deleted theorem exists_stronglyMeasurable_limit_of_tendsto_ae

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

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

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