Commit 2023-05-23 17:53 dcfe6388

View on Github →

feat: port MeasureTheory.Function.StronglyMeasurable.Basic (#4226)

Estimated changes

Modified Mathlib.lean

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

added theorem AEMeasurable.aestronglyMeasurable

added theorem Continuous.aestronglyMeasurable

added theorem Continuous.comp_aestronglyMeasurable

added theorem Continuous.comp_stronglyMeasurable

added theorem Continuous.stronglyMeasurable

added theorem ContinuousLinearMap.aestronglyMeasurable_comp₂

added theorem Embedding.aestronglyMeasurable_comp_iff

added theorem Embedding.comp_stronglyMeasurable_iff

added theorem Finset.aestronglyMeasurable_prod'

added theorem Finset.aestronglyMeasurable_prod

added theorem Finset.stronglyMeasurable_prod'

added theorem Finset.stronglyMeasurable_prod

added theorem List.aestronglyMeasurable_prod'

added theorem List.aestronglyMeasurable_prod

added theorem List.stronglyMeasurable_prod'

added theorem List.stronglyMeasurable_prod

added theorem Measurable.aestronglyMeasurable

added theorem Measurable.stronglyMeasurable

added theorem MeasurableEmbedding.aestronglyMeasurable_map_iff

added theorem MeasurableEmbedding.exists_stronglyMeasurable_extend

added theorem MeasurableEmbedding.stronglyMeasurable_extend

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.apply_continuousLinearMap

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_measure

added theorem MeasureTheory.AEStronglyMeasurable.mono_set

added theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_eq_fun

added theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_le

added theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_lt

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.FinStronglyMeasurable.exists_set_sigmaFinite

added def MeasureTheory.FinStronglyMeasurable

added theorem MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff

added theorem MeasureTheory.SimpleFunc.aestronglyMeasurable

added theorem MeasureTheory.SimpleFunc.stronglyMeasurable

added theorem MeasureTheory.StronglyMeasurable.comp_measurable

added theorem MeasureTheory.StronglyMeasurable.const_mul

added theorem MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le

added theorem MeasureTheory.StronglyMeasurable.finStronglyMeasurable_of_set_sigmaFinite

added theorem MeasureTheory.StronglyMeasurable.isSeparable_range

added theorem MeasureTheory.StronglyMeasurable.measurableSet_eq_fun

added theorem MeasureTheory.StronglyMeasurable.measurableSet_le

added theorem MeasureTheory.StronglyMeasurable.measurableSet_lt

added theorem MeasureTheory.StronglyMeasurable.mul_const

added theorem MeasureTheory.StronglyMeasurable.norm_approxBounded_le

added theorem MeasureTheory.StronglyMeasurable.of_uncurry_left

added theorem MeasureTheory.StronglyMeasurable.of_uncurry_right

added theorem MeasureTheory.StronglyMeasurable.separableSpace_range_union_singleton

added theorem MeasureTheory.StronglyMeasurable.stronglyMeasurable_in_set

added theorem MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on

added theorem MeasureTheory.StronglyMeasurable.tendsto_approxBounded_ae

added theorem MeasureTheory.StronglyMeasurable.tendsto_approxBounded_of_norm_le

added def MeasureTheory.StronglyMeasurable

added theorem MeasureTheory.Subsingleton.aestronglyMeasurable'

added theorem MeasureTheory.Subsingleton.aestronglyMeasurable

added theorem MeasureTheory.Subsingleton.stronglyMeasurable'

added theorem MeasureTheory.Subsingleton.stronglyMeasurable

added theorem MeasureTheory.aefinStronglyMeasurable_iff_aemeasurable

added theorem MeasureTheory.aefinStronglyMeasurable_zero

added theorem MeasureTheory.aestronglyMeasurable_const

added theorem MeasureTheory.aestronglyMeasurable_one

added theorem MeasureTheory.aestronglyMeasurable_zero_measure

added theorem MeasureTheory.finStronglyMeasurable_iff_measurable

added theorem MeasureTheory.finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFinite

added theorem MeasureTheory.finStronglyMeasurable_zero

added theorem MeasureTheory.measurable_uncurry_of_continuous_of_measurable

added theorem MeasureTheory.stronglyMeasurable_const'

added theorem MeasureTheory.stronglyMeasurable_const

added theorem MeasureTheory.stronglyMeasurable_of_isEmpty

added theorem MeasureTheory.stronglyMeasurable_one

added theorem MeasureTheory.stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable

added theorem Multiset.aestronglyMeasurable_prod'

added theorem Multiset.aestronglyMeasurable_prod

added theorem Multiset.stronglyMeasurable_prod'

added theorem Multiset.stronglyMeasurable_prod

added theorem StronglyMeasurable.apply_continuousLinearMap

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_indicator_iff

added theorem aestronglyMeasurable_of_aestronglyMeasurable_trim

added theorem aestronglyMeasurable_of_tendsto_ae

added theorem aestronglyMeasurable_smul_const_iff

added theorem aestronglyMeasurable_sum_measure_iff

added theorem aestronglyMeasurable_union_iff

added theorem aestronglyMeasurable_withDensity_iff

added theorem exists_stronglyMeasurable_limit_of_tendsto_ae

added theorem stronglyMeasurable_bot_iff

added theorem stronglyMeasurable_const_smul_iff

added theorem stronglyMeasurable_const_smul_iff₀

added theorem stronglyMeasurable_id

added theorem stronglyMeasurable_iff_measurable

added theorem stronglyMeasurable_iff_measurable_separable

added theorem stronglyMeasurable_of_restrict_of_restrict_compl

added theorem stronglyMeasurable_of_stronglyMeasurable_union_cover

added theorem stronglyMeasurable_of_tendsto

Modified Mathlib/Tactic/Measurability.lean