ConditionalLExpectation

📁 Source: Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean

Statistics

Metric	Count
Definitions condLExp, condLExpUnexpander, «term__⁻[_|_]»	3
Theorems ae_eq_condLExp, ae_eq_condLExp₀, condLExp_add_le, condLExp_add_left, condLExp_add_right, condLExp_bot, condLExp_bot', condLExp_bot_ae_eq, condLExp_congr_ae, condLExp_congr_ae_trim, condLExp_const, condLExp_def, condLExp_eq_self, condLExp_mono, condLExp_of_not_le, condLExp_of_not_sigmaFinite, condLExp_of_not_sub_sigma_measurable, condLExp_smul, condLExp_smul', condLExp_smul_le, lintegral_condLExp, measurable_condLExp, measurable_condLExp', setLIntegral_condLExp, setLIntegral_condLExp_trim	25
Total	28

MeasureTheory

Definitions

Name	Category	Theorems
condLExp 📖	CompOp	25 math math: condLExp_add_right, condLExp_bot', condLExp_smul, condLExp_add_left, condLExp_mono, ae_eq_condLExp, condLExp_bot, condLExp_congr_ae_trim, condLExp_congr_ae, condLExp_of_not_le, condLExp_const, condLExp_smul_le, condLExp_eq_self, condLExp_bot_ae_eq, measurable_condLExp', measurable_condLExp, ae_eq_condLExp₀, condLExp_smul', condLExp_def, lintegral_condLExp, setLIntegral_condLExp, condLExp_of_not_sigmaFinite, condLExp_add_le, condLExp_of_not_sub_sigma_measurable, setLIntegral_condLExp_trim
condLExpUnexpander 📖	CompOp	—
«term__⁻[_|_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_condLExp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable ENNReal ENNReal.measurableSpace lintegral Measure.restrict	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condLExp	—	ae_eq_condLExp₀ Measurable.aemeasurable
ae_eq_condLExp₀ 📖	mathematical	MeasurableSpace MeasurableSpace.instLE AEMeasurable ENNReal ENNReal.measurableSpace Measure.trim lintegral Measure.restrict	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condLExp	—	ae_eq_of_ae_eq_trim ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ Measurable.aemeasurable measurable_condLExp setLIntegral_trim_ae setLIntegral_condLExp_trim
condLExp_add_le 📖	mathematical	—	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring condLExp	—	Measure.instOuterMeasureClass ae_le_of_ae_le_trim ae_le_of_forall_setLIntegral_le_of_sigmaFinite Measurable.add' ContinuousAdd.measurableMul₂ ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instContinuousAdd Measurable.fun_comp measurable_condLExp Measurable.snd measurable_id' lintegral_add_left setLIntegral_condLExp_trim le_imp_le_of_le_of_le le_lintegral_add le_refl condLExp_of_not_sigmaFinite Filter.univ_mem' add_zero condLExp_of_not_le
condLExp_add_left 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condLExp Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Measure.instOuterMeasureClass Filter.EventuallyEq.symm ae_eq_condLExp Measurable.add' ContinuousAdd.measurableMul₂ ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instContinuousAdd Measurable.fun_comp measurable_condLExp Measurable.snd measurable_id' lintegral_add_left measurable_condLExp' setLIntegral_condLExp lintegral_add_left' AEMeasurable.restrict condLExp_of_not_sigmaFinite add_zero condLExp_of_not_le
condLExp_add_right 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condLExp Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Measure.instOuterMeasureClass add_comm condLExp_add_left
condLExp_bot 📖	mathematical	—	condLExp Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder lintegral	—	condLExp_bot' IsProbabilityMeasure.neZero IsProbabilityMeasure.measure_univ inv_one one_mul
condLExp_bot' 📖	mathematical	—	condLExp Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder ENNReal Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id ENNReal.instInv DFunLike.coe Measure Set Measure.instFunLike Set.univ lintegral	—	eq_const_of_measurable_bot separatesPointsOfOpensMeasurableSpaceOfT0Space BorelSpace.opensMeasurable ENNReal.borelSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace ENNReal.instMetrizableSpace measurable_condLExp lintegral_condLExp bot_le IsFiniteMeasure.toSigmaFinite isFiniteMeasure_trim lintegral_const mul_comm mul_assoc ENNReal.mul_inv_cancel Measure.instNeZeroENNRealCoeSetUniv measure_ne_top mul_one sigmaFinite_trim_bot_iff condLExp_of_not_sigmaFinite not_isFiniteMeasure_iff ENNReal.inv_top MulZeroClass.zero_mul
condLExp_bot_ae_eq 📖	mathematical	—	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass condLExp Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id ENNReal.instInv DFunLike.coe Set Set.univ lintegral	—	Measure.instOuterMeasureClass eq_zero_or_neZero ae_zero Filter.eventually_bot ae_of_all condLExp_bot'
condLExp_congr_ae 📖	mathematical	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	condLExp	—	Measure.instOuterMeasureClass ae_eq_condLExp measurable_condLExp setLIntegral_condLExp setLIntegral_congr_fun_ae Filter.mp_mem Filter.univ_mem' condLExp_of_not_sigmaFinite condLExp_of_not_le
condLExp_congr_ae_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Measure.trim condLExp	—	Measure.instOuterMeasureClass ae_eq_trim_of_measurable instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space measurable_condLExp condLExp_congr_ae
condLExp_const 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	condLExp	—	condLExp_eq_self measurable_const
condLExp_def 📖	mathematical	—	condLExp MeasurableSpace MeasurableSpace.instLE SigmaFinite Measure.trim Measurable ENNReal ENNReal.measurableSpace Measure.rnDeriv Measure.withDensity Pi.instZero instZeroENNReal	—	—
condLExp_eq_self 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable ENNReal ENNReal.measurableSpace	condLExp	—	condLExp_def
condLExp_mono 📖	mathematical	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	condLExp	—	Measure.instOuterMeasureClass ae_le_of_ae_le_trim ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_condLExp setLIntegral_condLExp_trim setLIntegral_mono_ae' Filter.mp_mem Filter.univ_mem' condLExp_of_not_sigmaFinite condLExp_of_not_le
condLExp_of_not_le 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	condLExp Pi.instZero ENNReal instZeroENNReal	—	condLExp_def
condLExp_of_not_sigmaFinite 📖	mathematical	MeasurableSpace MeasurableSpace.instLE SigmaFinite Measure.trim	condLExp Pi.instZero ENNReal instZeroENNReal	—	condLExp_def
condLExp_of_not_sub_sigma_measurable 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable ENNReal ENNReal.measurableSpace	condLExp Measure.rnDeriv Measure.trim Measure.withDensity	—	condLExp_def
condLExp_smul 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass condLExp Function.hasSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id	—	Measure.instOuterMeasureClass Filter.EventuallyEq.symm ae_eq_condLExp Measurable.const_smul MeasurableSMul.toMeasurableConstSMul measurableSMul_of_mul MeasurableMul₂.toMeasurableMul ENNReal.instMeasurableMul₂ measurable_condLExp lintegral_const_mul measurable_condLExp' lintegral_const_mul'' AEMeasurable.restrict setLIntegral_condLExp condLExp_of_not_sigmaFinite smul_zero condLExp_of_not_le
condLExp_smul' 📖	mathematical	—	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass condLExp Function.hasSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id	—	Measure.instOuterMeasureClass Filter.EventuallyEq.symm ae_eq_condLExp Measurable.const_smul MeasurableSMul.toMeasurableConstSMul measurableSMul_of_mul MeasurableMul₂.toMeasurableMul ENNReal.instMeasurableMul₂ measurable_condLExp lintegral_const_mul' setLIntegral_condLExp condLExp_of_not_sigmaFinite smul_zero condLExp_of_not_le
condLExp_smul_le 📖	mathematical	—	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Function.hasSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id condLExp	—	Measure.instOuterMeasureClass ae_le_of_ae_le_trim ae_le_of_forall_setLIntegral_le_of_sigmaFinite Measurable.const_smul MeasurableSMul.toMeasurableConstSMul measurableSMul_of_mul MeasurableMul₂.toMeasurableMul ENNReal.instMeasurableMul₂ measurable_condLExp lintegral_const_mul setLIntegral_condLExp_trim condLExp_of_not_sigmaFinite Filter.univ_mem' MulZeroClass.mul_zero condLExp_of_not_le
lintegral_condLExp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	lintegral condLExp	—	Measure.restrict_univ setLIntegral_condLExp MeasurableSet.univ
measurable_condLExp 📖	mathematical	—	Measurable ENNReal ENNReal.measurableSpace condLExp	—	condLExp_eq_self condLExp_of_not_sub_sigma_measurable condLExp_of_not_sigmaFinite condLExp_of_not_le
measurable_condLExp' 📖	mathematical	—	Measurable ENNReal ENNReal.measurableSpace condLExp	—	Measurable.mono measurable_condLExp le_refl condLExp_of_not_le
setLIntegral_condLExp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	lintegral Measure.restrict condLExp	—	condLExp_eq_self Measure.AbsolutelyContinuous.trim withDensity_absolutelyContinuous sFinite_of_absolutelyContinuous instSFiniteOfSigmaFinite condLExp_of_not_sub_sigma_measurable lintegral_indicator lintegral_trim Measurable.indicator Measure.measurable_rnDeriv Measure.setLIntegral_rnDeriv' Measure.haveLebesgueDecomposition_of_sigmaFinite trim_measurableSet_eq withDensity_apply
setLIntegral_condLExp_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	lintegral Measure.restrict Measure.trim condLExp	—	setLIntegral_trim measurable_condLExp setLIntegral_condLExp

---

← Back to Index