Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-13 16:52 0f79668f

View on Github →

feat(measure_theory/function/uniform_integrable): Egorov's theorem (#11328) This PR proves Egorov's theorem which is necessary for the Vitali convergence theorem which is vital for the martingale convergence theorems.

Estimated changes

Created src/measure_theory/function/uniform_integrable.lean

added def measure_theory.egorov.Union_not_convergent_seq

added theorem measure_theory.egorov.Union_not_convergent_seq_measurable_set

added theorem measure_theory.egorov.Union_not_convergent_seq_subset

added theorem measure_theory.egorov.exists_not_convergent_seq_lt

added theorem measure_theory.egorov.measure_Union_not_convergent_seq

added theorem measure_theory.egorov.measure_inter_not_convergent_seq_eq_zero

added theorem measure_theory.egorov.measure_not_convergent_seq_tendsto_zero

added theorem measure_theory.egorov.mem_not_convergent_seq_iff

added def measure_theory.egorov.not_convergent_seq

added theorem measure_theory.egorov.not_convergent_seq_antitone

added def measure_theory.egorov.not_convergent_seq_lt_index

added theorem measure_theory.egorov.not_convergent_seq_lt_index_spec

added theorem measure_theory.egorov.not_convergent_seq_measurable_set

added theorem measure_theory.egorov.tendsto_uniformly_on_diff_Union_not_convergent_seq

added theorem measure_theory.tendsto_uniformly_on_of_ae_tendsto'

added theorem measure_theory.tendsto_uniformly_on_of_ae_tendsto