Commit 2024-07-19 10:46 1674b343

View on Github →

feat(MeasureTheory/Function): Uniform tightness of functions in Lp (#14646) Uniform tightness is a hypothesis necessary for the general version of the Vitali Convergence Theorem proven in #9163.

Estimated changes

Modified Mathlib.lean

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

added theorem MeasureTheory.Memℒp.exists_snorm_indicator_compl_lt

added theorem MeasureTheory.snorm_indicator_eq_restrict

Created Mathlib/MeasureTheory/Function/UnifTight.lean

added theorem MeasureTheory.UnifTight.eventually_cofinite_indicator

added def MeasureTheory.UnifTight

added theorem MeasureTheory.unifTight_congr_ae

added theorem MeasureTheory.unifTight_const

added theorem MeasureTheory.unifTight_finite

added theorem MeasureTheory.unifTight_iff_ennreal

added theorem MeasureTheory.unifTight_iff_real

added theorem MeasureTheory.unifTight_of_subsingleton

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem MeasureTheory.exists_measurable_le_setLintegral_eq_of_integrable

added theorem MeasureTheory.exists_setLintegral_compl_lt

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified scripts/style-exceptions.txt