Commit 2023-06-17 04:56 17ae9987

View on Github →

feat: port MeasureTheory.Function.ConditionalExpectation.CondexpL2 (#5048)

Estimated changes

Modified Mathlib.lean

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

added theorem MeasureTheory.aeStronglyMeasurable'_condexpIndSMul

added theorem MeasureTheory.aeStronglyMeasurable'_condexpL2

added theorem MeasureTheory.condexpIndSMul_add

added theorem MeasureTheory.condexpIndSMul_ae_eq_smul

added theorem MeasureTheory.condexpIndSMul_empty

added theorem MeasureTheory.condexpIndSMul_nonneg

added theorem MeasureTheory.condexpIndSMul_smul'

added theorem MeasureTheory.condexpIndSMul_smul

added theorem MeasureTheory.condexpL2_ae_eq_zero_of_ae_eq_zero

added theorem MeasureTheory.condexpL2_comp_continuousLinearMap

added theorem MeasureTheory.condexpL2_const_inner

added theorem MeasureTheory.condexpL2_indicator_ae_eq_smul

added theorem MeasureTheory.condexpL2_indicator_eq_toSpanSingleton_comp

added theorem MeasureTheory.condexpL2_indicator_nonneg

added theorem MeasureTheory.condexpL2_indicator_of_measurable

added theorem MeasureTheory.inner_condexpL2_eq_inner_fun

added theorem MeasureTheory.inner_condexpL2_left_eq_right

added theorem MeasureTheory.integrableOn_condexpL2_of_measure_ne_top

added theorem MeasureTheory.integrable_condexpIndSMul

added theorem MeasureTheory.integrable_condexpL2_indicator

added theorem MeasureTheory.integrable_condexpL2_of_isFiniteMeasure

added theorem MeasureTheory.integral_condexpL2_eq

added theorem MeasureTheory.integral_condexpL2_eq_of_fin_meas_real

added theorem MeasureTheory.lintegral_nnnorm_condexpIndSMul_le

added theorem MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le

added theorem MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le_real

added theorem MeasureTheory.lintegral_nnnorm_condexpL2_le

added theorem MeasureTheory.norm_condexpL2_coe_le

added theorem MeasureTheory.norm_condexpL2_le

added theorem MeasureTheory.norm_condexpL2_le_one

added theorem MeasureTheory.set_integral_condexpIndSMul

added theorem MeasureTheory.set_integral_condexpL2_indicator

added theorem MeasureTheory.set_lintegral_nnnorm_condexpIndSMul_le

added theorem MeasureTheory.set_lintegral_nnnorm_condexpL2_indicator_le

added theorem MeasureTheory.snorm_condexpL2_le