Commit 2023-06-01 12:52 dc285819

View on Github →

feat: port MeasureTheory.Function.ConvergenceInMeasure (#4484)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

added theorem MeasureTheory.ExistsSeqTendstoAe.exists_nat_measure_lt_two_inv

added theorem MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_spec

added theorem MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono

added theorem MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_succ

added theorem MeasureTheory.TendstoInMeasure.aeMeasurable

added theorem MeasureTheory.TendstoInMeasure.congr_left

added theorem MeasureTheory.TendstoInMeasure.congr_right

added theorem MeasureTheory.TendstoInMeasure.exists_seq_tendstoInMeasure_atTop

added theorem MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae'

added theorem MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae

added def MeasureTheory.TendstoInMeasure

added theorem MeasureTheory.tendstoInMeasure_iff_norm

added theorem MeasureTheory.tendstoInMeasure_of_tendsto_Lp

added theorem MeasureTheory.tendstoInMeasure_of_tendsto_ae

added theorem MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable

added theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm

added theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_ne_top

added theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_stronglyMeasurable

added theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_top