Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-18 23:07 fbc9e5e3

View on Github →

feat(measure_theory/function/conditional_expectation): condexp_ind is ae_measurable' (#9263)

Estimated changes

Modified src/measure_theory/function/conditional_expectation.lean

added def measure_theory.Lp_meas_subgroup

added theorem measure_theory.Lp_meas_subgroup_coe

added def measure_theory.Lp_meas_subgroup_to_Lp_meas_iso

added def measure_theory.Lp_meas_subgroup_to_Lp_trim

added theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_add

added theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_ae_eq

added def measure_theory.Lp_meas_subgroup_to_Lp_trim_iso

added theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_left_inv

added theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_neg

added theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_norm_map

added theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_right_inv

added theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_sub

deleted def measure_theory.Lp_meas_to_Lp_trim

deleted theorem measure_theory.Lp_meas_to_Lp_trim_add

deleted theorem measure_theory.Lp_meas_to_Lp_trim_ae_eq

deleted theorem measure_theory.Lp_meas_to_Lp_trim_left_inv

deleted def measure_theory.Lp_meas_to_Lp_trim_lie

deleted theorem measure_theory.Lp_meas_to_Lp_trim_norm_map

deleted theorem measure_theory.Lp_meas_to_Lp_trim_right_inv

deleted theorem measure_theory.Lp_meas_to_Lp_trim_smul

deleted def measure_theory.Lp_trim_to_Lp_meas

deleted theorem measure_theory.Lp_trim_to_Lp_meas_ae_eq

added def measure_theory.Lp_trim_to_Lp_meas_subgroup

added theorem measure_theory.Lp_trim_to_Lp_meas_subgroup_ae_eq

added theorem measure_theory.ae_measurable'_condexp_L2

added theorem measure_theory.ae_measurable'_condexp_ind

added theorem measure_theory.ae_measurable'_condexp_ind_smul

added theorem measure_theory.is_closed_ae_measurable'

added theorem measure_theory.is_complete_ae_measurable'

added theorem measure_theory.isometry_Lp_meas_subgroup_to_Lp_trim

added theorem measure_theory.mem_Lp_meas_subgroup_iff_ae_measurable'

added theorem measure_theory.mem_Lp_meas_subgroup_to_Lp_of_trim

deleted theorem measure_theory.mem_Lp_meas_to_Lp_of_trim

deleted theorem measure_theory.mem_ℒp_trim_of_mem_Lp_meas

added theorem measure_theory.mem_ℒp_trim_of_mem_Lp_meas_subgroup