Commit 2025-01-22 13:49 fc30cf7d

View on Github →

chore: rename condexp to condExp (#20930) The current name is vestigial. From my PhD (LeanCamCombi)

Estimated changes

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

added theorem MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq

deleted theorem MeasureTheory.ae_eq_condexp_of_forall_setIntegral_eq

added theorem MeasureTheory.condExp_add

added theorem MeasureTheory.condExp_ae_eq_condExpL1

added theorem MeasureTheory.condExp_ae_eq_condExpL1CLM

added theorem MeasureTheory.condExp_bot'

added theorem MeasureTheory.condExp_bot

added theorem MeasureTheory.condExp_bot_ae_eq

added theorem MeasureTheory.condExp_condExp_of_le

added theorem MeasureTheory.condExp_congr_ae

added theorem MeasureTheory.condExp_const

added theorem MeasureTheory.condExp_finset_sum

added theorem MeasureTheory.condExp_mono

added theorem MeasureTheory.condExp_neg

added theorem MeasureTheory.condExp_nonneg

added theorem MeasureTheory.condExp_nonpos

added theorem MeasureTheory.condExp_of_aestronglyMeasurable'

added theorem MeasureTheory.condExp_of_not_le

added theorem MeasureTheory.condExp_of_not_sigmaFinite

added theorem MeasureTheory.condExp_of_sigmaFinite

added theorem MeasureTheory.condExp_of_stronglyMeasurable

added theorem MeasureTheory.condExp_smul

added theorem MeasureTheory.condExp_sub

added theorem MeasureTheory.condExp_undef

added theorem MeasureTheory.condExp_zero

deleted theorem MeasureTheory.condexp_add

deleted theorem MeasureTheory.condexp_ae_eq_condexpL1

deleted theorem MeasureTheory.condexp_ae_eq_condexpL1CLM

deleted theorem MeasureTheory.condexp_bot'

deleted theorem MeasureTheory.condexp_bot

deleted theorem MeasureTheory.condexp_bot_ae_eq

deleted theorem MeasureTheory.condexp_condexp_of_le

deleted theorem MeasureTheory.condexp_congr_ae

deleted theorem MeasureTheory.condexp_const

deleted theorem MeasureTheory.condexp_finset_sum

deleted theorem MeasureTheory.condexp_mono

deleted theorem MeasureTheory.condexp_neg

deleted theorem MeasureTheory.condexp_nonneg

deleted theorem MeasureTheory.condexp_nonpos

deleted theorem MeasureTheory.condexp_of_aestronglyMeasurable'

deleted theorem MeasureTheory.condexp_of_not_le

deleted theorem MeasureTheory.condexp_of_not_sigmaFinite

deleted theorem MeasureTheory.condexp_of_sigmaFinite

deleted theorem MeasureTheory.condexp_of_stronglyMeasurable

deleted theorem MeasureTheory.condexp_smul

deleted theorem MeasureTheory.condexp_sub

deleted theorem MeasureTheory.condexp_undef

deleted theorem MeasureTheory.condexp_zero

added theorem MeasureTheory.integrable_condExp

deleted theorem MeasureTheory.integrable_condexp

added theorem MeasureTheory.integral_condExp

added theorem MeasureTheory.integral_condExp_indicator

deleted theorem MeasureTheory.integral_condexp

deleted theorem MeasureTheory.integral_condexp_indicator

added theorem MeasureTheory.setIntegral_condExp

deleted theorem MeasureTheory.setIntegral_condexp

added theorem MeasureTheory.stronglyMeasurable_condExp

deleted theorem MeasureTheory.stronglyMeasurable_condexp

added theorem MeasureTheory.tendsto_condExpL1_of_dominated_convergence

added theorem MeasureTheory.tendsto_condExp_unique

deleted theorem MeasureTheory.tendsto_condexpL1_of_dominated_convergence

deleted theorem MeasureTheory.tendsto_condexp_unique

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

added theorem MeasureTheory.aestronglyMeasurable'_condExpInd

added theorem MeasureTheory.aestronglyMeasurable'_condExpL1

added theorem MeasureTheory.aestronglyMeasurable'_condExpL1CLM

deleted theorem MeasureTheory.aestronglyMeasurable'_condexpInd

deleted theorem MeasureTheory.aestronglyMeasurable'_condexpL1

deleted theorem MeasureTheory.aestronglyMeasurable'_condexpL1CLM

added def MeasureTheory.condExpInd

added def MeasureTheory.condExpIndL1

added def MeasureTheory.condExpIndL1Fin

added theorem MeasureTheory.condExpIndL1Fin_add

added theorem MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul

added theorem MeasureTheory.condExpIndL1Fin_disjoint_union

added theorem MeasureTheory.condExpIndL1Fin_smul'

added theorem MeasureTheory.condExpIndL1Fin_smul

added theorem MeasureTheory.condExpIndL1_add

added theorem MeasureTheory.condExpIndL1_disjoint_union

added theorem MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top

added theorem MeasureTheory.condExpIndL1_of_measure_eq_top

added theorem MeasureTheory.condExpIndL1_of_not_measurableSet

added theorem MeasureTheory.condExpIndL1_smul'

added theorem MeasureTheory.condExpIndL1_smul

added theorem MeasureTheory.condExpInd_ae_eq_condExpIndSMul

added theorem MeasureTheory.condExpInd_disjoint_union

added theorem MeasureTheory.condExpInd_disjoint_union_apply

added theorem MeasureTheory.condExpInd_empty

added theorem MeasureTheory.condExpInd_nonneg

added theorem MeasureTheory.condExpInd_of_measurable

added theorem MeasureTheory.condExpInd_smul'

added def MeasureTheory.condExpL1

added def MeasureTheory.condExpL1CLM

added theorem MeasureTheory.condExpL1CLM_indicatorConst

added theorem MeasureTheory.condExpL1CLM_indicatorConstLp

added theorem MeasureTheory.condExpL1CLM_lpMeas

added theorem MeasureTheory.condExpL1CLM_of_aestronglyMeasurable'

added theorem MeasureTheory.condExpL1CLM_smul

added theorem MeasureTheory.condExpL1_add

added theorem MeasureTheory.condExpL1_congr_ae

added theorem MeasureTheory.condExpL1_eq

added theorem MeasureTheory.condExpL1_measure_zero

added theorem MeasureTheory.condExpL1_mono

added theorem MeasureTheory.condExpL1_neg

added theorem MeasureTheory.condExpL1_of_aestronglyMeasurable'

added theorem MeasureTheory.condExpL1_smul

added theorem MeasureTheory.condExpL1_sub

added theorem MeasureTheory.condExpL1_undef

added theorem MeasureTheory.condExpL1_zero

deleted def MeasureTheory.condexpInd

deleted def MeasureTheory.condexpIndL1

deleted def MeasureTheory.condexpIndL1Fin

deleted theorem MeasureTheory.condexpIndL1Fin_add

deleted theorem MeasureTheory.condexpIndL1Fin_ae_eq_condexpIndSMul

deleted theorem MeasureTheory.condexpIndL1Fin_disjoint_union

deleted theorem MeasureTheory.condexpIndL1Fin_smul'

deleted theorem MeasureTheory.condexpIndL1Fin_smul

deleted theorem MeasureTheory.condexpIndL1_add

deleted theorem MeasureTheory.condexpIndL1_disjoint_union

deleted theorem MeasureTheory.condexpIndL1_of_measurableSet_of_measure_ne_top

deleted theorem MeasureTheory.condexpIndL1_of_measure_eq_top

deleted theorem MeasureTheory.condexpIndL1_of_not_measurableSet

deleted theorem MeasureTheory.condexpIndL1_smul'

deleted theorem MeasureTheory.condexpIndL1_smul

deleted theorem MeasureTheory.condexpInd_ae_eq_condexpIndSMul

deleted theorem MeasureTheory.condexpInd_disjoint_union

deleted theorem MeasureTheory.condexpInd_disjoint_union_apply

deleted theorem MeasureTheory.condexpInd_empty

deleted theorem MeasureTheory.condexpInd_nonneg

deleted theorem MeasureTheory.condexpInd_of_measurable

deleted theorem MeasureTheory.condexpInd_smul'

deleted def MeasureTheory.condexpL1

deleted def MeasureTheory.condexpL1CLM

deleted theorem MeasureTheory.condexpL1CLM_indicatorConst

deleted theorem MeasureTheory.condexpL1CLM_indicatorConstLp

deleted theorem MeasureTheory.condexpL1CLM_lpMeas

deleted theorem MeasureTheory.condexpL1CLM_of_aestronglyMeasurable'

deleted theorem MeasureTheory.condexpL1CLM_smul

deleted theorem MeasureTheory.condexpL1_add

deleted theorem MeasureTheory.condexpL1_congr_ae

deleted theorem MeasureTheory.condexpL1_eq

deleted theorem MeasureTheory.condexpL1_measure_zero

deleted theorem MeasureTheory.condexpL1_mono

deleted theorem MeasureTheory.condexpL1_neg

deleted theorem MeasureTheory.condexpL1_of_aestronglyMeasurable'

deleted theorem MeasureTheory.condexpL1_smul

deleted theorem MeasureTheory.condexpL1_sub

deleted theorem MeasureTheory.condexpL1_undef

deleted theorem MeasureTheory.condexpL1_zero

added theorem MeasureTheory.continuous_condExpIndL1

deleted theorem MeasureTheory.continuous_condexpIndL1

added theorem MeasureTheory.dominatedFinMeasAdditive_condExpInd

deleted theorem MeasureTheory.dominatedFinMeasAdditive_condexpInd

added theorem MeasureTheory.integrable_condExpL1

deleted theorem MeasureTheory.integrable_condexpL1

added theorem MeasureTheory.norm_condExpIndL1Fin_le

added theorem MeasureTheory.norm_condExpIndL1_le

added theorem MeasureTheory.norm_condExpInd_apply_le

added theorem MeasureTheory.norm_condExpInd_le

deleted theorem MeasureTheory.norm_condexpIndL1Fin_le

deleted theorem MeasureTheory.norm_condexpIndL1_le

deleted theorem MeasureTheory.norm_condexpInd_apply_le

deleted theorem MeasureTheory.norm_condexpInd_le

added theorem MeasureTheory.setIntegral_condExpInd

added theorem MeasureTheory.setIntegral_condExpL1

added theorem MeasureTheory.setIntegral_condExpL1CLM

added theorem MeasureTheory.setIntegral_condExpL1CLM_of_measure_ne_top

deleted theorem MeasureTheory.setIntegral_condexpInd

deleted theorem MeasureTheory.setIntegral_condexpL1

deleted theorem MeasureTheory.setIntegral_condexpL1CLM

deleted theorem MeasureTheory.setIntegral_condexpL1CLM_of_measure_ne_top

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

added theorem MeasureTheory.aeStronglyMeasurable'_condExpIndSMul

added theorem MeasureTheory.aeStronglyMeasurable'_condExpL2

deleted theorem MeasureTheory.aeStronglyMeasurable'_condexpIndSMul

deleted 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

deleted theorem MeasureTheory.condexpIndSMul_add

deleted theorem MeasureTheory.condexpIndSMul_ae_eq_smul

deleted theorem MeasureTheory.condexpIndSMul_empty

deleted theorem MeasureTheory.condexpIndSMul_nonneg

deleted theorem MeasureTheory.condexpIndSMul_smul'

deleted theorem MeasureTheory.condexpIndSMul_smul

deleted theorem MeasureTheory.condexpL2_ae_eq_zero_of_ae_eq_zero

deleted theorem MeasureTheory.condexpL2_comp_continuousLinearMap

deleted theorem MeasureTheory.condexpL2_const_inner

deleted theorem MeasureTheory.condexpL2_indicator_ae_eq_smul

deleted theorem MeasureTheory.condexpL2_indicator_eq_toSpanSingleton_comp

deleted theorem MeasureTheory.condexpL2_indicator_nonneg

deleted theorem MeasureTheory.condexpL2_indicator_of_measurable

added theorem MeasureTheory.eLpNorm_condExpL2_le

deleted theorem MeasureTheory.eLpNorm_condexpL2_le

added theorem MeasureTheory.inner_condExpL2_eq_inner_fun

added theorem MeasureTheory.inner_condExpL2_left_eq_right

deleted theorem MeasureTheory.inner_condexpL2_eq_inner_fun

deleted theorem MeasureTheory.inner_condexpL2_left_eq_right

added theorem MeasureTheory.integrableOn_condExpL2_of_measure_ne_top

deleted 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

deleted theorem MeasureTheory.integrable_condexpIndSMul

deleted theorem MeasureTheory.integrable_condexpL2_indicator

deleted theorem MeasureTheory.integrable_condexpL2_of_isFiniteMeasure

added theorem MeasureTheory.integral_condExpL2_eq

added theorem MeasureTheory.integral_condExpL2_eq_of_fin_meas_real

deleted theorem MeasureTheory.integral_condexpL2_eq

deleted 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

deleted theorem MeasureTheory.lintegral_nnnorm_condexpIndSMul_le

deleted theorem MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le

deleted theorem MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le_real

deleted 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

deleted theorem MeasureTheory.norm_condexpL2_coe_le

deleted theorem MeasureTheory.norm_condexpL2_le

deleted theorem MeasureTheory.norm_condexpL2_le_one

added theorem MeasureTheory.setIntegral_condExpIndSMul

added theorem MeasureTheory.setIntegral_condExpL2_indicator

deleted theorem MeasureTheory.setIntegral_condexpIndSMul

deleted theorem MeasureTheory.setIntegral_condexpL2_indicator

added theorem MeasureTheory.setLIntegral_nnnorm_condExpIndSMul_le

added theorem MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le

deleted theorem MeasureTheory.setLIntegral_nnnorm_condexpIndSMul_le

deleted theorem MeasureTheory.setLIntegral_nnnorm_condexpL2_indicator_le

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Indicator.lean

added theorem MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on

added theorem MeasureTheory.condExp_ae_eq_restrict_zero

added theorem MeasureTheory.condExp_indicator

added theorem MeasureTheory.condExp_indicator_aux

added theorem MeasureTheory.condExp_restrict_ae_eq_restrict

deleted theorem MeasureTheory.condexp_ae_eq_restrict_of_measurableSpace_eq_on

deleted theorem MeasureTheory.condexp_ae_eq_restrict_zero

deleted theorem MeasureTheory.condexp_indicator

deleted theorem MeasureTheory.condexp_indicator_aux

deleted theorem MeasureTheory.condexp_restrict_ae_eq_restrict

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

added theorem MeasureTheory.Integrable.uniformIntegrable_condExp

deleted theorem MeasureTheory.Integrable.uniformIntegrable_condexp

added theorem MeasureTheory.ae_bdd_condExp_of_ae_bdd

deleted theorem MeasureTheory.ae_bdd_condexp_of_ae_bdd

added theorem MeasureTheory.condExp_mul_of_aestronglyMeasurable_left

added theorem MeasureTheory.condExp_mul_of_aestronglyMeasurable_right

added theorem MeasureTheory.condExp_mul_of_stronglyMeasurable_left

added theorem MeasureTheory.condExp_mul_of_stronglyMeasurable_right

added theorem MeasureTheory.condExp_stronglyMeasurable_mul_of_bound

added theorem MeasureTheory.condExp_stronglyMeasurable_mul_of_bound₀

added theorem MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul

deleted theorem MeasureTheory.condexp_mul_of_aestronglyMeasurable_left

deleted theorem MeasureTheory.condexp_mul_of_aestronglyMeasurable_right

deleted theorem MeasureTheory.condexp_mul_of_stronglyMeasurable_left

deleted theorem MeasureTheory.condexp_mul_of_stronglyMeasurable_right

deleted theorem MeasureTheory.condexp_stronglyMeasurable_mul_of_bound

deleted theorem MeasureTheory.condexp_stronglyMeasurable_mul_of_bound₀

deleted theorem MeasureTheory.condexp_stronglyMeasurable_simpleFunc_mul

added theorem MeasureTheory.eLpNorm_one_condExp_le_eLpNorm

deleted theorem MeasureTheory.eLpNorm_one_condexp_le_eLpNorm

added theorem MeasureTheory.integral_abs_condExp_le

deleted theorem MeasureTheory.integral_abs_condexp_le

added theorem MeasureTheory.rnDeriv_ae_eq_condExp

deleted theorem MeasureTheory.rnDeriv_ae_eq_condexp

added theorem MeasureTheory.setIntegral_abs_condExp_le

deleted theorem MeasureTheory.setIntegral_abs_condexp_le

Modified Mathlib/Probability/BorelCantelli.lean

added theorem ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt

deleted theorem ProbabilityTheory.iIndepFun.condexp_natural_ae_eq_of_lt

added theorem ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq

deleted theorem ProbabilityTheory.iIndepSet.condexp_indicator_filtrationOfSet_ae_eq

Modified Mathlib/Probability/ConditionalExpectation.lean

added theorem MeasureTheory.condExp_indep_eq

deleted theorem MeasureTheory.condexp_indep_eq

Modified Mathlib/Probability/Independence/Conditional.lean

added theorem ProbabilityTheory.condIndepFun_iff_condExp_inter_preimage_eq_mul

deleted theorem ProbabilityTheory.condIndepFun_iff_condexp_inter_preimage_eq_mul

added theorem ProbabilityTheory.iCondIndepFun_iff_condExp_inter_preimage_eq_mul

deleted theorem ProbabilityTheory.iCondIndepFun_iff_condexp_inter_preimage_eq_mul

Modified Mathlib/Probability/Independence/Kernel.lean

Modified Mathlib/Probability/Independence/ZeroOne.lean

added theorem ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self

added theorem ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup

added theorem ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atBot

added theorem ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atTop

deleted theorem ProbabilityTheory.condexp_eq_zero_or_one_of_condIndepSet_self

deleted theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup

deleted theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atBot

deleted theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atTop

Modified Mathlib/Probability/Kernel/CondDistrib.lean

added theorem ProbabilityTheory.condDistrib_ae_eq_condExp

deleted theorem ProbabilityTheory.condDistrib_ae_eq_condexp

added theorem ProbabilityTheory.condExp_ae_eq_integral_condDistrib'

added theorem ProbabilityTheory.condExp_ae_eq_integral_condDistrib

added theorem ProbabilityTheory.condExp_ae_eq_integral_condDistrib_id

added theorem ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib'

added theorem ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib

added theorem ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib₀

deleted theorem ProbabilityTheory.condexp_ae_eq_integral_condDistrib'

deleted theorem ProbabilityTheory.condexp_ae_eq_integral_condDistrib

deleted theorem ProbabilityTheory.condexp_ae_eq_integral_condDistrib_id

deleted theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib'

deleted theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib

deleted theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib₀

Modified Mathlib/Probability/Kernel/Condexp.lean

added theorem MeasureTheory.AEStronglyMeasurable.integral_condExpKernel

deleted theorem MeasureTheory.AEStronglyMeasurable.integral_condexpKernel

added theorem MeasureTheory.Integrable.condExpKernel_ae

deleted theorem MeasureTheory.Integrable.condexpKernel_ae

added theorem MeasureTheory.Integrable.integral_condExpKernel

deleted theorem MeasureTheory.Integrable.integral_condexpKernel

added theorem MeasureTheory.Integrable.integral_norm_condExpKernel

deleted theorem MeasureTheory.Integrable.integral_norm_condexpKernel

added theorem MeasureTheory.Integrable.norm_integral_condExpKernel

deleted theorem MeasureTheory.Integrable.norm_integral_condexpKernel

added theorem ProbabilityTheory.aestronglyMeasurable'_integral_condExpKernel

deleted theorem ProbabilityTheory.aestronglyMeasurable'_integral_condexpKernel

added theorem ProbabilityTheory.condExpKernel_ae_eq_condExp'

added theorem ProbabilityTheory.condExpKernel_ae_eq_condExp

added theorem ProbabilityTheory.condExpKernel_ae_eq_trim_condExp

added theorem ProbabilityTheory.condExpKernel_apply_eq_condDistrib

added theorem ProbabilityTheory.condExpKernel_eq

added theorem ProbabilityTheory.condExpKernel_singleton_ae_eq_cond

added theorem ProbabilityTheory.condExp_ae_eq_integral_condExpKernel'

added theorem ProbabilityTheory.condExp_ae_eq_integral_condExpKernel

added theorem ProbabilityTheory.condExp_generateFrom_singleton

added theorem ProbabilityTheory.condExp_set_generateFrom_singleton

deleted theorem ProbabilityTheory.condexpKernel_ae_eq_condexp'

deleted theorem ProbabilityTheory.condexpKernel_ae_eq_condexp

deleted theorem ProbabilityTheory.condexpKernel_ae_eq_trim_condexp

deleted theorem ProbabilityTheory.condexpKernel_apply_eq_condDistrib

deleted theorem ProbabilityTheory.condexpKernel_eq

deleted theorem ProbabilityTheory.condexpKernel_singleton_ae_eq_cond

deleted theorem ProbabilityTheory.condexp_ae_eq_integral_condexpKernel'

deleted theorem ProbabilityTheory.condexp_ae_eq_integral_condexpKernel

deleted theorem ProbabilityTheory.condexp_generateFrom_singleton

deleted theorem ProbabilityTheory.condexp_set_generateFrom_singleton

added theorem ProbabilityTheory.integrable_toReal_condExpKernel

deleted theorem ProbabilityTheory.integrable_toReal_condexpKernel

added theorem ProbabilityTheory.measurable_condExpKernel

deleted theorem ProbabilityTheory.measurable_condexpKernel

added theorem ProbabilityTheory.stronglyMeasurable_condExpKernel

deleted theorem ProbabilityTheory.stronglyMeasurable_condexpKernel

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean

added theorem ProbabilityTheory.Kernel.condExp_densityProcess

deleted theorem ProbabilityTheory.Kernel.condexp_densityProcess

Modified Mathlib/Probability/Martingale/Basic.lean

added theorem MeasureTheory.Martingale.condExp_ae_eq

deleted theorem MeasureTheory.Martingale.condexp_ae_eq

added theorem MeasureTheory.Submartingale.ae_le_condExp

deleted theorem MeasureTheory.Submartingale.ae_le_condexp

added theorem MeasureTheory.Submartingale.condExp_sub_nonneg

deleted theorem MeasureTheory.Submartingale.condexp_sub_nonneg

added theorem MeasureTheory.Supermartingale.condExp_ae_le

deleted theorem MeasureTheory.Supermartingale.condexp_ae_le

added theorem MeasureTheory.martingale_condExp

deleted theorem MeasureTheory.martingale_condexp

added theorem MeasureTheory.martingale_of_condExp_sub_eq_zero_nat

deleted theorem MeasureTheory.martingale_of_condexp_sub_eq_zero_nat

added theorem MeasureTheory.submartingale_iff_condExp_sub_nonneg

deleted theorem MeasureTheory.submartingale_iff_condexp_sub_nonneg

added theorem MeasureTheory.submartingale_of_condExp_sub_nonneg

added theorem MeasureTheory.submartingale_of_condExp_sub_nonneg_nat

deleted theorem MeasureTheory.submartingale_of_condexp_sub_nonneg

deleted theorem MeasureTheory.submartingale_of_condexp_sub_nonneg_nat

added theorem MeasureTheory.supermartingale_of_condExp_sub_nonneg_nat

deleted theorem MeasureTheory.supermartingale_of_condexp_sub_nonneg_nat

Modified Mathlib/Probability/Martingale/BorelCantelli.lean

Modified Mathlib/Probability/Martingale/Centering.lean

Modified Mathlib/Probability/Martingale/Convergence.lean

added theorem MeasureTheory.Integrable.tendsto_ae_condExp

deleted theorem MeasureTheory.Integrable.tendsto_ae_condexp

added theorem MeasureTheory.Integrable.tendsto_eLpNorm_condExp

deleted theorem MeasureTheory.Integrable.tendsto_eLpNorm_condexp

added theorem MeasureTheory.Martingale.ae_eq_condExp_limitProcess

deleted theorem MeasureTheory.Martingale.ae_eq_condexp_limitProcess

added theorem MeasureTheory.Martingale.eq_condExp_of_tendsto_eLpNorm

deleted theorem MeasureTheory.Martingale.eq_condexp_of_tendsto_eLpNorm

added theorem MeasureTheory.tendsto_ae_condExp

deleted theorem MeasureTheory.tendsto_ae_condexp

added theorem MeasureTheory.tendsto_eLpNorm_condExp

deleted theorem MeasureTheory.tendsto_eLpNorm_condexp

Modified Mathlib/Probability/Martingale/OptionalSampling.lean

added theorem MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le

added theorem MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const

added theorem MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const

deleted theorem MeasureTheory.Martingale.condexp_stoppedValue_stopping_time_ae_eq_restrict_le

deleted theorem MeasureTheory.Martingale.condexp_stopping_time_ae_eq_restrict_eq_const

deleted theorem MeasureTheory.Martingale.condexp_stopping_time_ae_eq_restrict_eq_const_of_le_const

added theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le

added theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const

added theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range

added theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_of_countable_range

deleted theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le

deleted theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_const

deleted theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_const_of_countable_range

deleted theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_of_countable_range

added theorem MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp

deleted theorem MeasureTheory.Martingale.stoppedValue_min_ae_eq_condexp

Modified Mathlib/Probability/Notation.lean

Modified Mathlib/Probability/Process/Filtration.lean

added theorem MeasureTheory.Integrable.uniformIntegrable_condExp_filtration

deleted theorem MeasureTheory.Integrable.uniformIntegrable_condexp_filtration

Modified Mathlib/Probability/Process/Stopping.lean

added theorem MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le

added theorem MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le_const

added theorem MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq

added theorem MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable

added theorem MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable_range

deleted theorem MeasureTheory.condexp_min_stopping_time_ae_eq_restrict_le

deleted theorem MeasureTheory.condexp_min_stopping_time_ae_eq_restrict_le_const

deleted theorem MeasureTheory.condexp_stopping_time_ae_eq_restrict_eq

deleted theorem MeasureTheory.condexp_stopping_time_ae_eq_restrict_eq_of_countable

deleted theorem MeasureTheory.condexp_stopping_time_ae_eq_restrict_eq_of_countable_range

Modified docs/overview.yaml

Modified scripts/nolints_prime_decls.txt