Commit 2023-05-25 11:48 81dd6c69

View on Github →

feat: port MeasureTheory.Function.Egorov (#4333)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/Egorov.lean

added theorem MeasureTheory.Egorov.exists_notConvergentSeq_lt

added def MeasureTheory.Egorov.iUnionNotConvergentSeq

added theorem MeasureTheory.Egorov.iUnionNotConvergentSeq_measurableSet

added theorem MeasureTheory.Egorov.iUnionNotConvergentSeq_subset

added theorem MeasureTheory.Egorov.measure_iUnionNotConvergentSeq

added theorem MeasureTheory.Egorov.measure_inter_notConvergentSeq_eq_zero

added theorem MeasureTheory.Egorov.measure_notConvergentSeq_tendsto_zero

added theorem MeasureTheory.Egorov.mem_notConvergentSeq_iff

added def MeasureTheory.Egorov.notConvergentSeq

added def MeasureTheory.Egorov.notConvergentSeqLtIndex

added theorem MeasureTheory.Egorov.notConvergentSeqLtIndex_spec

added theorem MeasureTheory.Egorov.notConvergentSeq_antitone

added theorem MeasureTheory.Egorov.notConvergentSeq_measurableSet

added theorem MeasureTheory.Egorov.tendstoUniformlyOn_diff_iUnionNotConvergentSeq

added theorem MeasureTheory.tendstoUniformlyOn_of_ae_tendsto'

added theorem MeasureTheory.tendstoUniformlyOn_of_ae_tendsto