Commit 2024-03-09 08:55 95abf566

View on Github →

feat: tendsto_of_integral_tendsto_of_monotone (#11167) Add tendsto_of_integral_tendsto_of_monotone, as well as ...of_antitone and the corresponding results for lintegral. Also:

move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue.
add lintegral_iInf', a version of lintegral_iInf for a.e.-measurable functions. We already have the corresponding lintegral_iSup'.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

added theorem ENNReal.aemeasurable_of_tendsto'

added theorem ENNReal.aemeasurable_of_tendsto

added theorem ENNReal.measurable_of_tendsto'

added theorem ENNReal.measurable_of_tendsto

added theorem NNReal.measurable_of_tendsto'

added theorem NNReal.measurable_of_tendsto

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

deleted theorem measurable_of_tendsto_ennreal'

deleted theorem measurable_of_tendsto_ennreal

deleted theorem measurable_of_tendsto_nnreal'

deleted theorem measurable_of_tendsto_nnreal

Modified Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean

added theorem aeSeq.iInf

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

added theorem MeasureTheory.tendsto_of_integral_tendsto_of_antitone

added theorem MeasureTheory.tendsto_of_integral_tendsto_of_monotone

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem MeasureTheory.lintegral_iInf'

added theorem MeasureTheory.lintegral_tendsto_of_tendsto_of_antitone

added theorem MeasureTheory.tendsto_of_lintegral_tendsto_of_antitone

added theorem MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone

added theorem MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone_aux

Modified scripts/style-exceptions.txt