Commit 2023-06-13 09:59 dd235858

View on Github →

feat: port MeasureTheory.Function.ConditionalExpectation.AEMeasurable (#5005)

Estimated changes

Modified Mathlib.lean

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

added theorem MeasureTheory.AEStronglyMeasurable'.add

added theorem MeasureTheory.AEStronglyMeasurable'.aeStronglyMeasurable'_of_measurableSpace_le_on

added theorem MeasureTheory.AEStronglyMeasurable'.ae_eq_mk

added theorem MeasureTheory.AEStronglyMeasurable'.congr

added theorem MeasureTheory.AEStronglyMeasurable'.const_inner

added theorem MeasureTheory.AEStronglyMeasurable'.const_smul

added theorem MeasureTheory.AEStronglyMeasurable'.continuous_comp

added theorem MeasureTheory.AEStronglyMeasurable'.neg

added theorem MeasureTheory.AEStronglyMeasurable'.stronglyMeasurable_mk

added theorem MeasureTheory.AEStronglyMeasurable'.sub

added def MeasureTheory.AEStronglyMeasurable'

added theorem MeasureTheory.AEStronglyMeasurable.comp_ae_measurable'

added theorem MeasureTheory.Lp.induction_stronglyMeasurable

added theorem MeasureTheory.Lp.induction_stronglyMeasurable_aux

added theorem MeasureTheory.Memℒp.induction_stronglyMeasurable

added theorem MeasureTheory.StronglyMeasurable.aeStronglyMeasurable'

added theorem MeasureTheory.aeStronglyMeasurable'_of_aeStronglyMeasurable'_trim

added theorem MeasureTheory.ae_eq_trim_iff_of_aeStronglyMeasurable'

added theorem MeasureTheory.isClosed_aeStronglyMeasurable'

added theorem MeasureTheory.isComplete_aeStronglyMeasurable'

added theorem MeasureTheory.isometry_lpMeasSubgroupToLpTrim

added theorem MeasureTheory.lpMeas.aeStronglyMeasurable'

added theorem MeasureTheory.lpMeas.ae_fin_strongly_measurable'

added def MeasureTheory.lpMeas

added def MeasureTheory.lpMeasSubgroup

added theorem MeasureTheory.lpMeasSubgroupToLpTrim_add

added theorem MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq

added theorem MeasureTheory.lpMeasSubgroupToLpTrim_left_inv

added theorem MeasureTheory.lpMeasSubgroupToLpTrim_neg

added theorem MeasureTheory.lpMeasSubgroupToLpTrim_norm_map

added theorem MeasureTheory.lpMeasSubgroupToLpTrim_right_inv

added theorem MeasureTheory.lpMeasSubgroupToLpTrim_sub

added theorem MeasureTheory.lpMeasSubgroup_coe

added theorem MeasureTheory.lpMeasToLpTrimLie_symm_indicator

added theorem MeasureTheory.lpMeasToLpTrimLie_symm_toLp

added theorem MeasureTheory.lpMeasToLpTrim_ae_eq

added theorem MeasureTheory.lpMeasToLpTrim_smul

added theorem MeasureTheory.lpMeas_coe

added theorem MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq

added theorem MeasureTheory.lpTrimToLpMeas_ae_eq

added theorem MeasureTheory.mem_lpMeasSubgroup_iff_aeStronglyMeasurable'

added theorem MeasureTheory.mem_lpMeasSubgroup_toLp_of_trim

added theorem MeasureTheory.mem_lpMeas_iff_aeStronglyMeasurable'

added theorem MeasureTheory.mem_lpMeas_indicatorConstLp

added theorem MeasureTheory.mem_lpMeas_self

added theorem MeasureTheory.memℒp_trim_of_mem_lpMeasSubgroup