CondVar

📁 Source: Mathlib/Probability/CondVar.lean

Statistics

Metric	Count
Definitions condVar, «termVar[_;_|_]», «termVar[_|_]»	3
Theorems condVar_ae_eq_condExp_sq_sub_sq_condExp, condVar_ae_le_condExp_sq, condVar_bot, condVar_bot', condVar_bot_ae_eq, condVar_congr_ae, condVar_const, condVar_neg, condVar_of_aestronglyMeasurable, condVar_of_not_integrable, condVar_of_not_le, condVar_of_not_sigmaFinite, condVar_of_sigmaFinite, condVar_of_stronglyMeasurable, condVar_smul, condVar_zero, integrable_condVar, integral_condVar_add_variance_condExp, setIntegral_condVar, stronglyMeasurable_condVar	20
Total	23

ProbabilityTheory

Definitions

Name	Category	Theorems
condVar 📖	CompOp	20 math math: condVar_const, condVar_smul, integrable_condVar, integral_condVar_add_variance_condExp, condVar_of_stronglyMeasurable, condVar_zero, condVar_of_not_le, condVar_ae_le_condExp_sq, condVar_bot', condVar_of_sigmaFinite, setIntegral_condVar, condVar_neg, condVar_bot_ae_eq, condVar_of_aestronglyMeasurable, condVar_bot, condVar_of_not_sigmaFinite, condVar_of_not_integrable, condVar_ae_eq_condExp_sq_sub_sq_condExp, stronglyMeasurable_condVar, condVar_congr_ae
«termVar[_;_|_]» 📖	CompOp	—
«termVar[_|_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condVar_ae_eq_condExp_sq_sub_sq_condExp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.MemLp Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass condVar Pi.instSub Real.instSub MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Pi.monoid Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condVar.eq_1 sub_sq MeasureTheory.MemLp.integrable_sq mul_assoc MeasureTheory.Integrable.const_mul MeasureTheory.memLp_one_iff_integrable MeasureTheory.MemLp.mul MeasureTheory.MemLp.condExp ENNReal.HolderConjugate.instTwoTwo Rat.instIsStrictOrderedRing Filter.mp_mem MeasureTheory.condExp_ofNat MeasureTheory.condExp_mul_of_stronglyMeasurable_right MeasureTheory.stronglyMeasurable_condExp MeasureTheory.MemLp.integrable one_le_two IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid MeasureTheory.condExp_sub MeasureTheory.condExp_add MeasureTheory.Integrable.sub Filter.univ_mem' MeasureTheory.condExp_of_stronglyMeasurable MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.isFiniteMeasure_trim MeasureTheory.StronglyMeasurable.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal AddRightCancelSemigroup.toIsRightCancelAdd sq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add
condVar_ae_le_condExp_sq 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.MemLp Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	Filter.EventuallyLE Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass condVar MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Pi.monoid Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condVar_ae_eq_condExp_sq_sub_sq_condExp Filter.univ_mem' le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.le_of_le_of_eq Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt
condVar_bot 📖	mathematical	AEMeasurable Real Real.measurableSpace	condVar Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder variance	—	condVar_bot' MeasureTheory.IsProbabilityMeasure.neZero MeasureTheory.average_eq_integral variance_eq_integral
condVar_bot' 📖	mathematical	—	condVar Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder MeasureTheory.average Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.instSub	—	Real.instCompleteSpace MeasureTheory.condExp_bot' IsScalarTower.right MeasureTheory.integral_smul_measure ENNReal.toReal_inv
condVar_bot_ae_eq 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass condVar Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder MeasureTheory.average Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.instSub	—	MeasureTheory.Measure.instOuterMeasureClass eq_zero_or_neZero MeasureTheory.ae_zero Filter.eventually_bot Filter.Eventually.of_forall condVar_bot'
condVar_congr_ae 📖	mathematical	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	condVar	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp_congr_ae Real.instCompleteSpace Filter.mp_mem Filter.univ_mem'
condVar_const 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	condVar Pi.instZero Real Real.instZero	—	eq_or_ne condVar_zero Real.instCompleteSpace MeasureTheory.condExp_const sub_self zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MeasureTheory.condExp_zero MeasureTheory.condExp_of_not_integrable MeasureTheory.integrable_const_iff_isFiniteMeasure sub_zero pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
condVar_neg 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass condVar Pi.instNeg Real.instNeg	—	MeasureTheory.condExp_congr_ae Real.instCompleteSpace Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp_neg Filter.univ_mem' sub_neg_eq_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf
condVar_of_aestronglyMeasurable 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Monoid.toNatPow Pi.monoid Real.instMonoid Pi.instSub Real.instSub MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass condVar	—	Real.instCompleteSpace MeasureTheory.condExp_of_aestronglyMeasurable' Continuous.comp_aestronglyMeasurable continuous_pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.AEStronglyMeasurable.sub instIsTopologicalAddGroupReal MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.stronglyMeasurable_condExp
condVar_of_not_integrable 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Monoid.toNatPow Real.instMonoid Real.instSub MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	condVar Pi.instZero Real.instZero	—	Real.instCompleteSpace MeasureTheory.condExp_of_not_integrable
condVar_of_not_le 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	condVar Pi.instZero Real Real.instZero	—	Real.instCompleteSpace condVar.eq_1 MeasureTheory.condExp_of_not_le
condVar_of_not_sigmaFinite 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.SigmaFinite MeasureTheory.Measure.trim	condVar Pi.instZero Real Real.instZero	—	Real.instCompleteSpace condVar.eq_1 MeasureTheory.condExp_of_not_sigmaFinite
condVar_of_sigmaFinite 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	condVar MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Monoid.toNatPow Real.instMonoid Real.instSub MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.StronglyMeasurable SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun.cast MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.condExpL1 MeasureTheory.aestronglyMeasurable_condExpL1 Pi.instZero Real.instZero	—	MeasureTheory.condExp_of_sigmaFinite Real.instCompleteSpace
condVar_of_stronglyMeasurable 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Monoid.toNatPow Pi.monoid Real.instMonoid Pi.instSub Real.instSub MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	condVar	—	Real.instCompleteSpace MeasureTheory.condExp_of_stronglyMeasurable MeasureTheory.StronglyMeasurable.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.StronglyMeasurable.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal MeasureTheory.stronglyMeasurable_condExp
condVar_smul 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass condVar Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Monoid.toNatPow Real.instMonoid	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace condVar.eq_1 MeasureTheory.condExp_congr_ae Filter.mp_mem MeasureTheory.condExp_smul Filter.univ_mem' mul_pow
condVar_zero 📖	mathematical	—	condVar Pi.instZero Real Real.instZero	—	Real.instCompleteSpace MeasureTheory.condExp_zero sub_self zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
integrable_condVar 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing condVar	—	MeasureTheory.integrable_condExp Real.instCompleteSpace
integral_condVar_add_variance_condExp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.MemLp Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	Real.instAdd MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal condVar variance MeasureTheory.condExp Real.instCompleteSpace	—	Nat.instAtLeastTwoHAddOfNat Real.instCompleteSpace MeasureTheory.integral_congr_ae condVar_ae_eq_condExp_sq_sub_sq_condExp MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure variance_eq_sub MeasureTheory.MemLp.condExp MeasureTheory.integral_sub' MeasureTheory.integrable_condExp MeasureTheory.MemLp.integrable_sq MeasureTheory.integral_condExp MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.isFiniteMeasure_trim Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
setIntegral_condVar 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Monoid.toNatPow Pi.monoid Real.instMonoid Pi.instSub Real.instSub MeasureTheory.condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasurableSet	MeasureTheory.integral MeasureTheory.Measure.restrict condVar	—	Real.instCompleteSpace MeasureTheory.setIntegral_condExp
stronglyMeasurable_condVar 📖	mathematical	—	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condVar	—	MeasureTheory.stronglyMeasurable_condExp Real.instCompleteSpace

---

← Back to Index