Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-15 21:23 b577bb2c

View on Github →

feat(measure_theory/conditional_expectation): define condexp_L2, conditional expectation of L2 functions (#8324)

Estimated changes

Modified src/measure_theory/conditional_expectation.lean

added def measure_theory.condexp_L2

added theorem measure_theory.condexp_L2_indicator_of_measurable

added theorem measure_theory.inner_condexp_L2_eq_inner_fun

added theorem measure_theory.inner_condexp_L2_left_eq_right

added theorem measure_theory.integrable_condexp_L2_of_finite_measure

added theorem measure_theory.integrable_on_condexp_L2_of_measure_ne_top

added theorem measure_theory.mem_Lp_meas_indicator_const_Lp

added theorem measure_theory.norm_condexp_L2_coe_le

added theorem measure_theory.norm_condexp_L2_le

added theorem measure_theory.norm_condexp_L2_le_one

added theorem measure_theory.snorm_condexp_L2_le