Commit 2023-06-17 12:30 529b276a

View on Github →

feat: port MeasureTheory.Function.ConditionalExpectation.Basic (#4898)

Estimated changes

Modified Mathlib.lean

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

added theorem MeasureTheory.ae_eq_condexp_of_forall_set_integral_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

added theorem MeasureTheory.integrable_condexp

added theorem MeasureTheory.integral_condexp

added theorem MeasureTheory.set_integral_condexp

added theorem MeasureTheory.stronglyMeasurable_condexp

added theorem MeasureTheory.tendsto_condexpL1_of_dominated_convergence

added theorem MeasureTheory.tendsto_condexp_unique