Commit 2023-05-31 07:01 19f958e3

View on Github →

feat: port MeasureTheory.Integral.IntegrableOn (#4520)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/IntegrableOn.lean

added theorem AeStronglyMeasurable.stronglyMeasurableAtFilter_of_mem

added theorem Continuous.integrableAt_nhds

added theorem Continuous.stronglyMeasurableAtFilter

added theorem ContinuousAt.stronglyMeasurableAtFilter

added theorem ContinuousOn.aemeasurable

added theorem ContinuousOn.aestronglyMeasurable

added theorem ContinuousOn.aestronglyMeasurable_of_isCompact

added theorem ContinuousOn.aestronglyMeasurable_of_isSeparable

added theorem ContinuousOn.integrableAt_nhdsWithin

added theorem ContinuousOn.integrableAt_nhdsWithin_of_isSeparable

added theorem ContinuousOn.stronglyMeasurableAtFilter

added theorem ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin

added theorem MeasurableEmbedding.integrableOn_map_iff

added theorem MeasureTheory.Integrable.indicator

added theorem MeasureTheory.Integrable.integrableAtFilter

added theorem MeasureTheory.Integrable.integrableOn

added theorem MeasureTheory.Integrable.lintegral_lt_top

added theorem MeasureTheory.IntegrableAtFilter.filter_mono

added theorem MeasureTheory.IntegrableAtFilter.inf_ae_iff

added theorem MeasureTheory.IntegrableAtFilter.inf_of_left

added theorem MeasureTheory.IntegrableAtFilter.inf_of_right

added def MeasureTheory.IntegrableAtFilter

added theorem MeasureTheory.IntegrableOn.add_measure

added theorem MeasureTheory.IntegrableOn.congr_fun

added theorem MeasureTheory.IntegrableOn.congr_fun_ae

added theorem MeasureTheory.IntegrableOn.congr_set_ae

added theorem MeasureTheory.IntegrableOn.indicator

added theorem MeasureTheory.IntegrableOn.integrable

added theorem MeasureTheory.IntegrableOn.integrable_indicator

added theorem MeasureTheory.IntegrableOn.integrable_of_ae_not_mem_eq_zero

added theorem MeasureTheory.IntegrableOn.integrable_of_forall_not_mem_eq_zero

added theorem MeasureTheory.IntegrableOn.left_of_union

added theorem MeasureTheory.IntegrableOn.mono

added theorem MeasureTheory.IntegrableOn.mono_measure

added theorem MeasureTheory.IntegrableOn.mono_set

added theorem MeasureTheory.IntegrableOn.mono_set_ae

added theorem MeasureTheory.IntegrableOn.of_ae_diff_eq_zero

added theorem MeasureTheory.IntegrableOn.of_forall_diff_eq_zero

added theorem MeasureTheory.IntegrableOn.restrict

added theorem MeasureTheory.IntegrableOn.restrict_toMeasurable

added theorem MeasureTheory.IntegrableOn.right_of_union

added theorem MeasureTheory.IntegrableOn.set_lintegral_lt_top

added theorem MeasureTheory.IntegrableOn.union

added def MeasureTheory.IntegrableOn

added theorem MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter

added theorem MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto

added theorem MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto_ae

added theorem MeasureTheory.MeasurePreserving.integrableOn_comp_preimage

added theorem MeasureTheory.MeasurePreserving.integrableOn_image

added theorem MeasureTheory.hasFiniteIntegral_restrict_of_bounded

added theorem MeasureTheory.integrableOn_Lp_of_measure_ne_top

added theorem MeasureTheory.integrableOn_add_measure

added theorem MeasureTheory.integrableOn_congr_fun

added theorem MeasureTheory.integrableOn_congr_fun_ae

added theorem MeasureTheory.integrableOn_const

added theorem MeasureTheory.integrableOn_def

added theorem MeasureTheory.integrableOn_empty

added theorem MeasureTheory.integrableOn_finite_biUnion

added theorem MeasureTheory.integrableOn_finite_iUnion

added theorem MeasureTheory.integrableOn_finset_iUnion

added theorem MeasureTheory.integrableOn_iff_integrable_of_support_subset

added theorem MeasureTheory.integrableOn_map_equiv

added theorem MeasureTheory.integrableOn_singleton_iff

added theorem MeasureTheory.integrableOn_union

added theorem MeasureTheory.integrableOn_univ

added theorem MeasureTheory.integrableOn_zero

added theorem MeasureTheory.integrable_add_of_disjoint

added theorem MeasureTheory.integrable_indicatorConstLp

added theorem MeasureTheory.integrable_indicator_iff

added def StronglyMeasurableAtFilter

added theorem integrableOn_Icc_iff_integrableOn_Ico'

added theorem integrableOn_Icc_iff_integrableOn_Ico

added theorem integrableOn_Icc_iff_integrableOn_Ioc'

added theorem integrableOn_Icc_iff_integrableOn_Ioc

added theorem integrableOn_Icc_iff_integrableOn_Ioo'

added theorem integrableOn_Icc_iff_integrableOn_Ioo

added theorem integrableOn_Ici_iff_integrableOn_Ioi'

added theorem integrableOn_Ici_iff_integrableOn_Ioi

added theorem integrableOn_Ico_iff_integrableOn_Ioo'

added theorem integrableOn_Ico_iff_integrableOn_Ioo

added theorem integrableOn_Iic_iff_integrableOn_Iio'

added theorem integrableOn_Iic_iff_integrableOn_Iio

added theorem integrableOn_Ioc_iff_integrableOn_Ioo'

added theorem integrableOn_Ioc_iff_integrableOn_Ioo

added theorem stronglyMeasurableAt_bot