Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-12 09:33 d8bbb04e

View on Github →

chore(measure_theory/function/conditional_expectation): split measure_theory.function.conditional_expectation.basic (#19177)

Estimated changes

Created src/measure_theory/function/conditional_expectation/ae_measurable.lean

added theorem measure_theory.Lp.induction_strongly_measurable

added theorem measure_theory.Lp.induction_strongly_measurable_aux

added theorem measure_theory.Lp_meas.ae_fin_strongly_measurable'

added theorem measure_theory.Lp_meas.ae_strongly_measurable'

added def measure_theory.Lp_meas

added theorem measure_theory.Lp_meas_coe

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

added def measure_theory.Lp_meas_to_Lp_trim

added theorem measure_theory.Lp_meas_to_Lp_trim_ae_eq

added def measure_theory.Lp_meas_to_Lp_trim_lie

added theorem measure_theory.Lp_meas_to_Lp_trim_lie_symm_indicator

added theorem measure_theory.Lp_meas_to_Lp_trim_lie_symm_to_Lp

added theorem measure_theory.Lp_meas_to_Lp_trim_smul

added def measure_theory.Lp_trim_to_Lp_meas

added 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_eq_trim_iff_of_ae_strongly_measurable'

added theorem measure_theory.ae_strongly_measurable'.add

added theorem measure_theory.ae_strongly_measurable'.ae_eq_mk

added theorem measure_theory.ae_strongly_measurable'.ae_strongly_measurable'_of_measurable_space_le_on

added theorem measure_theory.ae_strongly_measurable'.congr

added theorem measure_theory.ae_strongly_measurable'.const_inner

added theorem measure_theory.ae_strongly_measurable'.const_smul

added theorem measure_theory.ae_strongly_measurable'.continuous_comp

added def measure_theory.ae_strongly_measurable'.mk

added theorem measure_theory.ae_strongly_measurable'.neg

added theorem measure_theory.ae_strongly_measurable'.strongly_measurable_mk

added theorem measure_theory.ae_strongly_measurable'.sub

added def measure_theory.ae_strongly_measurable'

added theorem measure_theory.ae_strongly_measurable'_of_ae_strongly_measurable'_trim

added theorem measure_theory.ae_strongly_measurable.comp_ae_measurable'

added theorem measure_theory.is_closed_ae_strongly_measurable'

added theorem measure_theory.is_complete_ae_strongly_measurable'

added theorem measure_theory.isometry_Lp_meas_subgroup_to_Lp_trim

added theorem measure_theory.mem_Lp_meas_iff_ae_strongly_measurable'

added theorem measure_theory.mem_Lp_meas_indicator_const_Lp

added theorem measure_theory.mem_Lp_meas_self

added theorem measure_theory.mem_Lp_meas_subgroup_iff_ae_strongly_measurable'

added theorem measure_theory.mem_Lp_meas_subgroup_to_Lp_of_trim

added theorem measure_theory.mem_ℒp.induction_strongly_measurable

added theorem measure_theory.mem_ℒp_trim_of_mem_Lp_meas_subgroup

added theorem measure_theory.strongly_measurable.ae_strongly_measurable'

Modified src/measure_theory/function/conditional_expectation/basic.lean

deleted theorem measure_theory.Lp.ae_eq_of_forall_set_integral_eq'

deleted theorem measure_theory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero'

deleted theorem measure_theory.Lp.induction_strongly_measurable

deleted theorem measure_theory.Lp.induction_strongly_measurable_aux

deleted theorem measure_theory.Lp_meas.ae_eq_zero_of_forall_set_integral_eq_zero

deleted theorem measure_theory.Lp_meas.ae_fin_strongly_measurable'

deleted theorem measure_theory.Lp_meas.ae_strongly_measurable'

deleted def measure_theory.Lp_meas

deleted theorem measure_theory.Lp_meas_coe

deleted def measure_theory.Lp_meas_subgroup

deleted theorem measure_theory.Lp_meas_subgroup_coe

deleted def measure_theory.Lp_meas_subgroup_to_Lp_meas_iso

deleted def measure_theory.Lp_meas_subgroup_to_Lp_trim

deleted theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_add

deleted theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_ae_eq

deleted def measure_theory.Lp_meas_subgroup_to_Lp_trim_iso

deleted theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_left_inv

deleted theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_neg

deleted theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_norm_map

deleted theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_right_inv

deleted 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_ae_eq

deleted def measure_theory.Lp_meas_to_Lp_trim_lie

deleted theorem measure_theory.Lp_meas_to_Lp_trim_lie_symm_indicator

deleted theorem measure_theory.Lp_meas_to_Lp_trim_lie_symm_to_Lp

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

deleted def measure_theory.Lp_trim_to_Lp_meas_subgroup

deleted theorem measure_theory.Lp_trim_to_Lp_meas_subgroup_ae_eq

deleted theorem measure_theory.ae_eq_of_forall_set_integral_eq_of_sigma_finite'

deleted theorem measure_theory.ae_eq_trim_iff_of_ae_strongly_measurable'

deleted theorem measure_theory.ae_strongly_measurable'.add

deleted theorem measure_theory.ae_strongly_measurable'.ae_eq_mk

deleted theorem measure_theory.ae_strongly_measurable'.ae_strongly_measurable'_of_measurable_space_le_on

deleted theorem measure_theory.ae_strongly_measurable'.congr

deleted theorem measure_theory.ae_strongly_measurable'.const_inner

deleted theorem measure_theory.ae_strongly_measurable'.const_smul

deleted theorem measure_theory.ae_strongly_measurable'.continuous_comp

deleted def measure_theory.ae_strongly_measurable'.mk

deleted theorem measure_theory.ae_strongly_measurable'.neg

deleted theorem measure_theory.ae_strongly_measurable'.strongly_measurable_mk

deleted theorem measure_theory.ae_strongly_measurable'.sub

deleted def measure_theory.ae_strongly_measurable'

deleted theorem measure_theory.ae_strongly_measurable'_condexp_L1

deleted theorem measure_theory.ae_strongly_measurable'_condexp_L1_clm

deleted theorem measure_theory.ae_strongly_measurable'_condexp_L2

deleted theorem measure_theory.ae_strongly_measurable'_condexp_ind

deleted theorem measure_theory.ae_strongly_measurable'_condexp_ind_smul

deleted theorem measure_theory.ae_strongly_measurable'_of_ae_strongly_measurable'_trim

deleted theorem measure_theory.ae_strongly_measurable.comp_ae_measurable'

deleted def measure_theory.condexp_L1

deleted theorem measure_theory.condexp_L1_add

deleted def measure_theory.condexp_L1_clm

deleted theorem measure_theory.condexp_L1_clm_Lp_meas

deleted theorem measure_theory.condexp_L1_clm_indicator_const

deleted theorem measure_theory.condexp_L1_clm_indicator_const_Lp

deleted theorem measure_theory.condexp_L1_clm_of_ae_strongly_measurable'

deleted theorem measure_theory.condexp_L1_clm_smul

deleted theorem measure_theory.condexp_L1_congr_ae

deleted theorem measure_theory.condexp_L1_eq

deleted theorem measure_theory.condexp_L1_measure_zero

deleted theorem measure_theory.condexp_L1_mono

deleted theorem measure_theory.condexp_L1_neg

deleted theorem measure_theory.condexp_L1_of_ae_strongly_measurable'

deleted theorem measure_theory.condexp_L1_smul

deleted theorem measure_theory.condexp_L1_sub

deleted theorem measure_theory.condexp_L1_undef

deleted theorem measure_theory.condexp_L1_zero

deleted def measure_theory.condexp_L2

deleted theorem measure_theory.condexp_L2_ae_eq_zero_of_ae_eq_zero

deleted theorem measure_theory.condexp_L2_comp_continuous_linear_map

deleted theorem measure_theory.condexp_L2_const_inner

deleted theorem measure_theory.condexp_L2_indicator_ae_eq_smul

deleted theorem measure_theory.condexp_L2_indicator_eq_to_span_singleton_comp

deleted theorem measure_theory.condexp_L2_indicator_nonneg

deleted theorem measure_theory.condexp_L2_indicator_of_measurable

deleted def measure_theory.condexp_ind

deleted def measure_theory.condexp_ind_L1

deleted theorem measure_theory.condexp_ind_L1_add

deleted theorem measure_theory.condexp_ind_L1_disjoint_union

deleted def measure_theory.condexp_ind_L1_fin

deleted theorem measure_theory.condexp_ind_L1_fin_add

deleted theorem measure_theory.condexp_ind_L1_fin_ae_eq_condexp_ind_smul

deleted theorem measure_theory.condexp_ind_L1_fin_disjoint_union

deleted theorem measure_theory.condexp_ind_L1_fin_smul'

deleted theorem measure_theory.condexp_ind_L1_fin_smul

deleted theorem measure_theory.condexp_ind_L1_of_measurable_set_of_measure_ne_top

deleted theorem measure_theory.condexp_ind_L1_of_measure_eq_top

deleted theorem measure_theory.condexp_ind_L1_of_not_measurable_set

deleted theorem measure_theory.condexp_ind_L1_smul'

deleted theorem measure_theory.condexp_ind_L1_smul

deleted theorem measure_theory.condexp_ind_ae_eq_condexp_ind_smul

deleted theorem measure_theory.condexp_ind_disjoint_union

deleted theorem measure_theory.condexp_ind_disjoint_union_apply

deleted theorem measure_theory.condexp_ind_empty

deleted theorem measure_theory.condexp_ind_nonneg

deleted theorem measure_theory.condexp_ind_of_measurable

deleted theorem measure_theory.condexp_ind_smul'

deleted def measure_theory.condexp_ind_smul

deleted theorem measure_theory.condexp_ind_smul_add

deleted theorem measure_theory.condexp_ind_smul_ae_eq_smul

deleted theorem measure_theory.condexp_ind_smul_empty

deleted theorem measure_theory.condexp_ind_smul_nonneg

deleted theorem measure_theory.condexp_ind_smul_smul'

deleted theorem measure_theory.condexp_ind_smul_smul

deleted theorem measure_theory.continuous_condexp_ind_L1

deleted theorem measure_theory.dominated_fin_meas_additive_condexp_ind

deleted theorem measure_theory.inner_condexp_L2_eq_inner_fun

deleted theorem measure_theory.inner_condexp_L2_left_eq_right

deleted theorem measure_theory.integrable_condexp_L1

deleted theorem measure_theory.integrable_condexp_L2_indicator

deleted theorem measure_theory.integrable_condexp_L2_of_is_finite_measure

deleted theorem measure_theory.integrable_condexp_ind_smul

deleted theorem measure_theory.integrable_on_condexp_L2_of_measure_ne_top

deleted theorem measure_theory.integral_condexp_L2_eq

deleted theorem measure_theory.integral_condexp_L2_eq_of_fin_meas_real

deleted theorem measure_theory.integral_norm_le_of_forall_fin_meas_integral_eq

deleted theorem measure_theory.is_closed_ae_strongly_measurable'

deleted theorem measure_theory.is_complete_ae_strongly_measurable'

deleted theorem measure_theory.isometry_Lp_meas_subgroup_to_Lp_trim

deleted theorem measure_theory.lintegral_nnnorm_condexp_L2_indicator_le

deleted theorem measure_theory.lintegral_nnnorm_condexp_L2_indicator_le_real

deleted theorem measure_theory.lintegral_nnnorm_condexp_L2_le

deleted theorem measure_theory.lintegral_nnnorm_condexp_ind_smul_le

deleted theorem measure_theory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq

deleted theorem measure_theory.mem_Lp_meas_iff_ae_strongly_measurable'

deleted theorem measure_theory.mem_Lp_meas_indicator_const_Lp

deleted theorem measure_theory.mem_Lp_meas_self

deleted theorem measure_theory.mem_Lp_meas_subgroup_iff_ae_strongly_measurable'

deleted theorem measure_theory.mem_Lp_meas_subgroup_to_Lp_of_trim

deleted theorem measure_theory.mem_ℒp.induction_strongly_measurable

deleted theorem measure_theory.mem_ℒp_trim_of_mem_Lp_meas_subgroup

deleted theorem measure_theory.norm_condexp_L2_coe_le

deleted theorem measure_theory.norm_condexp_L2_le

deleted theorem measure_theory.norm_condexp_L2_le_one

deleted theorem measure_theory.norm_condexp_ind_L1_fin_le

deleted theorem measure_theory.norm_condexp_ind_L1_le

deleted theorem measure_theory.norm_condexp_ind_apply_le

deleted theorem measure_theory.norm_condexp_ind_le

deleted theorem measure_theory.set_integral_condexp_L1

deleted theorem measure_theory.set_integral_condexp_L1_clm

deleted theorem measure_theory.set_integral_condexp_L1_clm_of_measure_ne_top

deleted theorem measure_theory.set_integral_condexp_L2_indicator

deleted theorem measure_theory.set_integral_condexp_ind

deleted theorem measure_theory.set_integral_condexp_ind_smul

deleted theorem measure_theory.set_lintegral_nnnorm_condexp_L2_indicator_le

deleted theorem measure_theory.set_lintegral_nnnorm_condexp_ind_smul_le

deleted theorem measure_theory.snorm_condexp_L2_le

deleted theorem measure_theory.strongly_measurable.ae_strongly_measurable'

Created src/measure_theory/function/conditional_expectation/condexp_L1.lean

added theorem measure_theory.ae_strongly_measurable'_condexp_L1

added theorem measure_theory.ae_strongly_measurable'_condexp_L1_clm

added theorem measure_theory.ae_strongly_measurable'_condexp_ind

added def measure_theory.condexp_L1

added theorem measure_theory.condexp_L1_add

added def measure_theory.condexp_L1_clm

added theorem measure_theory.condexp_L1_clm_Lp_meas

added theorem measure_theory.condexp_L1_clm_indicator_const

added theorem measure_theory.condexp_L1_clm_indicator_const_Lp

added theorem measure_theory.condexp_L1_clm_of_ae_strongly_measurable'

added theorem measure_theory.condexp_L1_clm_smul

added theorem measure_theory.condexp_L1_congr_ae

added theorem measure_theory.condexp_L1_eq

added theorem measure_theory.condexp_L1_measure_zero

added theorem measure_theory.condexp_L1_mono

added theorem measure_theory.condexp_L1_neg

added theorem measure_theory.condexp_L1_of_ae_strongly_measurable'

added theorem measure_theory.condexp_L1_smul

added theorem measure_theory.condexp_L1_sub

added theorem measure_theory.condexp_L1_undef

added theorem measure_theory.condexp_L1_zero

added def measure_theory.condexp_ind

added def measure_theory.condexp_ind_L1

added theorem measure_theory.condexp_ind_L1_add

added theorem measure_theory.condexp_ind_L1_disjoint_union

added def measure_theory.condexp_ind_L1_fin

added theorem measure_theory.condexp_ind_L1_fin_add

added theorem measure_theory.condexp_ind_L1_fin_ae_eq_condexp_ind_smul

added theorem measure_theory.condexp_ind_L1_fin_disjoint_union

added theorem measure_theory.condexp_ind_L1_fin_smul'

added theorem measure_theory.condexp_ind_L1_fin_smul

added theorem measure_theory.condexp_ind_L1_of_measurable_set_of_measure_ne_top

added theorem measure_theory.condexp_ind_L1_of_measure_eq_top

added theorem measure_theory.condexp_ind_L1_of_not_measurable_set

added theorem measure_theory.condexp_ind_L1_smul'

added theorem measure_theory.condexp_ind_L1_smul

added theorem measure_theory.condexp_ind_ae_eq_condexp_ind_smul

added theorem measure_theory.condexp_ind_disjoint_union

added theorem measure_theory.condexp_ind_disjoint_union_apply

added theorem measure_theory.condexp_ind_empty

added theorem measure_theory.condexp_ind_nonneg

added theorem measure_theory.condexp_ind_of_measurable

added theorem measure_theory.condexp_ind_smul'

added theorem measure_theory.continuous_condexp_ind_L1

added theorem measure_theory.dominated_fin_meas_additive_condexp_ind

added theorem measure_theory.integrable_condexp_L1

added theorem measure_theory.norm_condexp_ind_L1_fin_le

added theorem measure_theory.norm_condexp_ind_L1_le

added theorem measure_theory.norm_condexp_ind_apply_le

added theorem measure_theory.norm_condexp_ind_le

added theorem measure_theory.set_integral_condexp_L1

added theorem measure_theory.set_integral_condexp_L1_clm

added theorem measure_theory.set_integral_condexp_L1_clm_of_measure_ne_top

added theorem measure_theory.set_integral_condexp_ind

Created src/measure_theory/function/conditional_expectation/condexp_L2.lean

added theorem measure_theory.ae_strongly_measurable'_condexp_L2

added theorem measure_theory.ae_strongly_measurable'_condexp_ind_smul

added def measure_theory.condexp_L2

added theorem measure_theory.condexp_L2_ae_eq_zero_of_ae_eq_zero

added theorem measure_theory.condexp_L2_comp_continuous_linear_map

added theorem measure_theory.condexp_L2_const_inner

added theorem measure_theory.condexp_L2_indicator_ae_eq_smul

added theorem measure_theory.condexp_L2_indicator_eq_to_span_singleton_comp

added theorem measure_theory.condexp_L2_indicator_nonneg

added theorem measure_theory.condexp_L2_indicator_of_measurable

added def measure_theory.condexp_ind_smul

added theorem measure_theory.condexp_ind_smul_add

added theorem measure_theory.condexp_ind_smul_ae_eq_smul

added theorem measure_theory.condexp_ind_smul_empty

added theorem measure_theory.condexp_ind_smul_nonneg

added theorem measure_theory.condexp_ind_smul_smul'

added theorem measure_theory.condexp_ind_smul_smul

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_indicator

added theorem measure_theory.integrable_condexp_L2_of_is_finite_measure

added theorem measure_theory.integrable_condexp_ind_smul

added theorem measure_theory.integrable_on_condexp_L2_of_measure_ne_top

added theorem measure_theory.integral_condexp_L2_eq

added theorem measure_theory.integral_condexp_L2_eq_of_fin_meas_real

added theorem measure_theory.lintegral_nnnorm_condexp_L2_indicator_le

added theorem measure_theory.lintegral_nnnorm_condexp_L2_indicator_le_real

added theorem measure_theory.lintegral_nnnorm_condexp_L2_le

added theorem measure_theory.lintegral_nnnorm_condexp_ind_smul_le

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.set_integral_condexp_L2_indicator

added theorem measure_theory.set_integral_condexp_ind_smul

added theorem measure_theory.set_lintegral_nnnorm_condexp_L2_indicator_le

added theorem measure_theory.set_lintegral_nnnorm_condexp_ind_smul_le

added theorem measure_theory.snorm_condexp_L2_le

Created src/measure_theory/function/conditional_expectation/unique.lean

added theorem measure_theory.Lp.ae_eq_of_forall_set_integral_eq'

added theorem measure_theory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero'

added theorem measure_theory.Lp_meas.ae_eq_zero_of_forall_set_integral_eq_zero

added theorem measure_theory.ae_eq_of_forall_set_integral_eq_of_sigma_finite'

added theorem measure_theory.integral_norm_le_of_forall_fin_meas_integral_eq

added theorem measure_theory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq