Commit 2024-02-22 16:20 eaba1225

View on Github →

feat: add versions of the monotone convergence theorem for the Bochner integral (#10793)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

added theorem MeasureTheory.integral_tendsto_of_tendsto_of_antitone

added theorem MeasureTheory.integral_tendsto_of_tendsto_of_monotone

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem Filter.tendsto_const_div_iff

added theorem Filter.tendsto_div_const_iff

added theorem Filter.tendsto_sub_const_iff

Modified Mathlib/Topology/Instances/ENNReal.lean

added theorem ENNReal.continuousAt_toReal