Commit 2023-06-17 11:16 dd445718

View on Github →

feat: port MeasureTheory.Function.ConditionalExpectation.CondexpL1 (#5174)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

added theorem MeasureTheory.aestronglyMeasurable'_condexpInd

added theorem MeasureTheory.aestronglyMeasurable'_condexpL1

added theorem MeasureTheory.aestronglyMeasurable'_condexpL1Clm

added def MeasureTheory.condexpInd

added def MeasureTheory.condexpIndL1

added def MeasureTheory.condexpIndL1Fin

added theorem MeasureTheory.condexpIndL1Fin_add

added theorem MeasureTheory.condexpIndL1Fin_ae_eq_condexpIndSMul

added theorem MeasureTheory.condexpIndL1Fin_disjoint_union

added theorem MeasureTheory.condexpIndL1Fin_smul'

added theorem MeasureTheory.condexpIndL1Fin_smul

added theorem MeasureTheory.condexpIndL1_add

added theorem MeasureTheory.condexpIndL1_disjoint_union

added theorem MeasureTheory.condexpIndL1_of_measurableSet_of_measure_ne_top

added theorem MeasureTheory.condexpIndL1_of_measure_eq_top

added theorem MeasureTheory.condexpIndL1_of_not_measurableSet

added theorem MeasureTheory.condexpIndL1_smul'

added theorem MeasureTheory.condexpIndL1_smul

added theorem MeasureTheory.condexpInd_ae_eq_condexpIndSMul

added theorem MeasureTheory.condexpInd_disjoint_union

added theorem MeasureTheory.condexpInd_disjoint_union_apply

added theorem MeasureTheory.condexpInd_empty

added theorem MeasureTheory.condexpInd_nonneg

added theorem MeasureTheory.condexpInd_of_measurable

added theorem MeasureTheory.condexpInd_smul'

added def MeasureTheory.condexpL1

added def MeasureTheory.condexpL1Clm

added theorem MeasureTheory.condexpL1Clm_indicatorConst

added theorem MeasureTheory.condexpL1Clm_indicatorConstLp

added theorem MeasureTheory.condexpL1Clm_lpMeas

added theorem MeasureTheory.condexpL1Clm_of_aestronglyMeasurable'

added theorem MeasureTheory.condexpL1Clm_smul

added theorem MeasureTheory.condexpL1_add

added theorem MeasureTheory.condexpL1_congr_ae

added theorem MeasureTheory.condexpL1_eq

added theorem MeasureTheory.condexpL1_measure_zero

added theorem MeasureTheory.condexpL1_mono

added theorem MeasureTheory.condexpL1_neg

added theorem MeasureTheory.condexpL1_of_aestronglyMeasurable'

added theorem MeasureTheory.condexpL1_smul

added theorem MeasureTheory.condexpL1_sub

added theorem MeasureTheory.condexpL1_undef

added theorem MeasureTheory.condexpL1_zero

added theorem MeasureTheory.continuous_condexpIndL1

added theorem MeasureTheory.dominatedFinMeasAdditive_condexpInd

added theorem MeasureTheory.integrable_condexpL1

added theorem MeasureTheory.norm_condexpIndL1Fin_le

added theorem MeasureTheory.norm_condexpIndL1_le

added theorem MeasureTheory.norm_condexpInd_apply_le

added theorem MeasureTheory.norm_condexpInd_le

added theorem MeasureTheory.set_integral_condexpInd

added theorem MeasureTheory.set_integral_condexpL1

added theorem MeasureTheory.set_integral_condexpL1Clm

added theorem MeasureTheory.set_integral_condexpL1Clm_of_measure_ne_top