ConditionalExpectation

📁 Source: Mathlib/Probability/ConditionalExpectation.lean

Statistics

Metric	Count
Definitions	0
Theorems condExp_indep_eq	1
Total	1

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condExp_indep_eq 📖	mathematical	MeasurableSpace MeasurableSpace.instLE StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ProbabilityTheory.Indep	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condExp integral	—	Measure.instOuterMeasureClass Filter.EventuallyEq.symm ae_eq_condExp_of_forall_setIntegral_eq integrableOn_const LT.lt.ne enorm_ne_top setIntegral_const MemLp.induction_stronglyMeasurable fact_one_le_one_ennreal ENNReal.one_ne_top integral_indicator smul_smul measureReal_def ENNReal.toReal_mul mul_comm ProbabilityTheory.Indep_iff setIntegral_indicator Set.inter_comm integral_add' memLp_one_iff_integrable smul_add Integrable.integrableOn SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul integral_congr_ae Filter.EventuallyEq.refl ae_restrict_of_ae Filter.Eventually.of_forall isClosed_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.const_smul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul Continuous.comp continuous_integral ContinuousLinearMap.continuous continuous_setIntegral setIntegral_congr_ae Filter.mp_mem Filter.univ_mem' Filter.EventuallyEq.rfl StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_const condExp_of_not_integrable integral_undef

---

← Back to Index