Commit 2023-06-02 11:07 204f135f

View on Github →

feat: port MeasureTheory.Function.UniformIntegrable (#4577)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/UniformIntegrable.lean

added theorem MeasureTheory.Memℒp.integral_indicator_norm_ge_le

added theorem MeasureTheory.Memℒp.integral_indicator_norm_ge_nonneg_le

added theorem MeasureTheory.Memℒp.integral_indicator_norm_ge_nonneg_le_of_meas

added theorem MeasureTheory.Memℒp.snormEssSup_indicator_norm_ge_eq_zero

added theorem MeasureTheory.Memℒp.snorm_indicator_le'

added theorem MeasureTheory.Memℒp.snorm_indicator_le

added theorem MeasureTheory.Memℒp.snorm_indicator_le_of_meas

added theorem MeasureTheory.Memℒp.snorm_indicator_norm_ge_le

added theorem MeasureTheory.Memℒp.snorm_indicator_norm_ge_pos_le

added def MeasureTheory.UnifIntegrable

added theorem MeasureTheory.UniformIntegrable.ae_eq

added theorem MeasureTheory.UniformIntegrable.spec'

added theorem MeasureTheory.UniformIntegrable.spec

added def MeasureTheory.UniformIntegrable

added theorem MeasureTheory.snorm_indicator_le_of_bound

added theorem MeasureTheory.snorm_sub_le_of_dist_bdd

added theorem MeasureTheory.tendstoInMeasure_iff_tendsto_Lp

added theorem MeasureTheory.tendsto_Lp_of_tendstoInMeasure

added theorem MeasureTheory.tendsto_Lp_of_tendsto_ae

added theorem MeasureTheory.tendsto_Lp_of_tendsto_ae_of_meas

added theorem MeasureTheory.tendsto_indicator_ge

added theorem MeasureTheory.unifIntegrable_congr_ae

added theorem MeasureTheory.unifIntegrable_const

added theorem MeasureTheory.unifIntegrable_fin

added theorem MeasureTheory.unifIntegrable_finite

added theorem MeasureTheory.unifIntegrable_of'

added theorem MeasureTheory.unifIntegrable_of

added theorem MeasureTheory.unifIntegrable_of_tendsto_Lp

added theorem MeasureTheory.unifIntegrable_of_tendsto_Lp_zero

added theorem MeasureTheory.unifIntegrable_subsingleton

added theorem MeasureTheory.unifIntegrable_zero_meas

added theorem MeasureTheory.uniformIntegrable_average

added theorem MeasureTheory.uniformIntegrable_congr_ae

added theorem MeasureTheory.uniformIntegrable_const

added theorem MeasureTheory.uniformIntegrable_finite

added theorem MeasureTheory.uniformIntegrable_iff

added theorem MeasureTheory.uniformIntegrable_of'

added theorem MeasureTheory.uniformIntegrable_of

added theorem MeasureTheory.uniformIntegrable_subsingleton

added theorem MeasureTheory.uniformIntegrable_zero_meas