Covariance

📁 Source: Mathlib/Probability/Moments/Covariance.lean

Statistics

Metric	Count
Definitions covariance, «termCov[_,_;_]», «termCov[_,_]»	3
Theorems covariance_eq_zero, covariance_add_const_left, covariance_add_const_right, covariance_add_left, covariance_add_right, covariance_comm, covariance_const_add_left, covariance_const_add_right, covariance_const_left, covariance_const_mul_left, covariance_const_mul_right, covariance_const_right, covariance_const_sub_left, covariance_const_sub_right, covariance_eq_sub, covariance_fst_snd_prod, covariance_fun_neg_left, covariance_fun_neg_right, covariance_fun_sum_fun_sum, covariance_fun_sum_fun_sum', covariance_fun_sum_left, covariance_fun_sum_left', covariance_fun_sum_right, covariance_fun_sum_right', covariance_map, covariance_map_equiv, covariance_map_fun, covariance_mul_const_left, covariance_mul_const_right, covariance_mul_left, covariance_mul_right, covariance_neg_left, covariance_neg_right, covariance_smul_left, covariance_smul_right, covariance_sub_const_left, covariance_sub_const_right, covariance_sub_left, covariance_sub_right, covariance_sum_left, covariance_sum_left', covariance_sum_right, covariance_sum_right', covariance_sum_sum, covariance_sum_sum', covariance_zero_left, covariance_zero_measure, covariance_zero_right	48
Total	51

ProbabilityTheory

Definitions

Name	Category	Theorems
covariance 📖	CompOp	63 math math: covariance_neg_left, variance_fun_sum', covariance_add_left, covarianceBilin_apply_eq_cov, covariance_mul_right, covariance_mul_left, covariance_sub_const_right, covariance_fst_snd_prod, covariance_mul_const_left, covariance_fun_neg_right, covariance_add_const_right, covariance_zero_right, covariance_smul_left, covariance_sum_right', covariance_add_const_left, HasLaw.covariance_comp, covariance_sum_right, covariance_const_left, covarianceBilinDual_eq_covariance, covariance_sub_right, variance_sub, covariance_sum_left, covariance_fun_sum_right', covariance_const_add_left, covariance_neg_right, covariance_add_right, covariance_fun_neg_left, covariance_fun_sum_left, covariance_sum_sum, variance_fun_sum, covariance_eq_sub, covariance_sub_left, covariance_const_mul_right, covariance_fun_sum_fun_sum', covarianceBilin_apply_pi, covariance_fun_sum_right, variance_fun_sub, covarianceBilin_apply_basisFun, IndepFun.covariance_eq_zero, covariance_map_equiv, HasLaw.covariance_fun_comp, variance_add, covariance_zero_measure, covariance_smul_right, covariance_sum_left', covariance_const_sub_left, covariance_sum_sum', variance_sum', covariance_const_mul_left, covariance_const_add_right, covariance_comm, covariance_zero_left, variance_fun_add, covariance_mul_const_right, covariance_sub_const_left, covariance_const_right, covariance_const_sub_right, covariance_map, variance_sum, covariance_self, covariance_map_fun, covariance_fun_sum_left', covariance_fun_sum_fun_sum
«termCov[_,_;_]» 📖	CompOp	—
«termCov[_,_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
covariance_add_const_left 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	covariance Real.instAdd	—	MeasureTheory.integral_add MeasureTheory.integrable_const MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.probReal_univ one_mul add_sub_add_right_eq_sub
covariance_add_const_right 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	covariance Real.instAdd	—	covariance_comm covariance_add_const_left
covariance_add_left 📖	mathematical	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	covariance Pi.instAdd Real.instAdd	—	Nat.instAtLeastTwoHAddOfNat MeasureTheory.integral_add MeasureTheory.MemLp.integrable_mul MeasureTheory.MemLp.sub MeasureTheory.memLp_const ENNReal.HolderConjugate.instTwoTwo MeasureTheory.MemLp.integrable IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing ENNReal.instCharZero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt
covariance_add_right 📖	mathematical	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	covariance Pi.instAdd Real.instAdd	—	Nat.instAtLeastTwoHAddOfNat covariance_comm covariance_add_left
covariance_comm 📖	mathematical	—	covariance	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt
covariance_const_add_left 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	covariance Real.instAdd	—	add_comm covariance_add_const_left
covariance_const_add_right 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	covariance Real.instAdd	—	add_comm covariance_add_const_right
covariance_const_left 📖	mathematical	—	covariance Real Real.instZero	—	MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.probReal_univ one_mul sub_self MulZeroClass.zero_mul MeasureTheory.integral_zero
covariance_const_mul_left 📖	mathematical	—	covariance Real Real.instMul	—	covariance_smul_left
covariance_const_mul_right 📖	mathematical	—	covariance Real Real.instMul	—	covariance_smul_right
covariance_const_right 📖	mathematical	—	covariance Real Real.instZero	—	MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.probReal_univ one_mul sub_self MulZeroClass.mul_zero MeasureTheory.integral_zero
covariance_const_sub_left 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	covariance Real.instSub Real.instNeg	—	sub_eq_add_neg covariance_const_add_left MeasureTheory.Integrable.neg' covariance_fun_neg_left
covariance_const_sub_right 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	covariance Real.instSub Real.instNeg	—	sub_eq_add_neg covariance_const_add_right MeasureTheory.Integrable.neg' covariance_fun_neg_right
covariance_eq_sub 📖	mathematical	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	covariance Real.instSub MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Pi.instMul Real.instMul	—	Nat.instAtLeastTwoHAddOfNat sub_mul mul_sub MeasureTheory.integral_sub MeasureTheory.Integrable.sub MeasureTheory.MemLp.integrable_mul ENNReal.HolderConjugate.instTwoTwo MeasureTheory.MemLp.integrable IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing ENNReal.instCharZero MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.MemLp.mul_const MeasureTheory.MemLp.const_mul MeasureTheory.integrable_const MeasureTheory.integral_mul_const MeasureTheory.integral_const_mul MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.probReal_univ one_smul sub_self sub_zero
covariance_fst_snd_prod 📖	mathematical	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	covariance Prod.instMeasurableSpace MeasureTheory.Measure.prod Real.instZero	—	Nat.instAtLeastTwoHAddOfNat IndepFun.covariance_eq_zero indepFun_prod₀ MeasureTheory.MemLp.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace MeasureTheory.MemLp.comp_fst MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.MemLp.comp_snd MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite
covariance_fun_neg_left 📖	mathematical	—	covariance Real Real.instNeg	—	covariance_neg_left
covariance_fun_neg_right 📖	mathematical	—	covariance Real Real.instNeg	—	covariance_neg_right
covariance_fun_sum_fun_sum 📖	mathematical	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	covariance Finset.sum Real.instAddCommMonoid Finset.univ	—	Nat.instAtLeastTwoHAddOfNat covariance_fun_sum_fun_sum'
covariance_fun_sum_fun_sum' 📖	mathematical	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	covariance Finset.sum Real.instAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat Finset.sum_apply covariance_sum_sum'
covariance_fun_sum_left 📖	mathematical	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	covariance Finset.sum Real.instAddCommMonoid Finset.univ	—	Nat.instAtLeastTwoHAddOfNat Finset.sum_apply covariance_sum_left
covariance_fun_sum_left' 📖	mathematical	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	covariance Finset.sum Real.instAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat Finset.sum_apply covariance_sum_left'
covariance_fun_sum_right 📖	mathematical	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	covariance Finset.sum Real.instAddCommMonoid Finset.univ	—	Nat.instAtLeastTwoHAddOfNat covariance_fun_sum_right'
covariance_fun_sum_right' 📖	mathematical	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	covariance Finset.sum Real.instAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat Finset.sum_apply covariance_sum_right'
covariance_map 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.Measure.map AEMeasurable	covariance	—	MeasureTheory.integral_map MeasureTheory.AEStronglyMeasurable.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.AEStronglyMeasurable.sub instIsTopologicalAddGroupReal MeasureTheory.aestronglyMeasurable_const
covariance_map_equiv 📖	mathematical	—	covariance MeasureTheory.Measure.map DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike Real	—	MeasureTheory.integral_map_equiv
covariance_map_fun 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.Measure.map AEMeasurable	covariance	—	covariance_map
covariance_mul_const_left 📖	mathematical	—	covariance Real Real.instMul	—	mul_comm covariance_const_mul_left
covariance_mul_const_right 📖	mathematical	—	covariance Real Real.instMul	—	mul_comm covariance_const_mul_right
covariance_mul_left 📖	mathematical	—	covariance Real Real.instMul	—	covariance_const_mul_left
covariance_mul_right 📖	mathematical	—	covariance Real Real.instMul	—	covariance_const_mul_right
covariance_neg_left 📖	mathematical	—	covariance Pi.instNeg Real Real.instNeg	—	neg_smul one_smul covariance_smul_left neg_mul one_mul
covariance_neg_right 📖	mathematical	—	covariance Pi.instNeg Real Real.instNeg	—	neg_smul one_smul covariance_smul_right neg_mul one_mul
covariance_smul_left 📖	mathematical	—	covariance Real Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instMul	—	mul_sub MeasureTheory.integral_const_mul
covariance_smul_right 📖	mathematical	—	covariance Real Function.hasSMul Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instMul	—	covariance_comm covariance_smul_left
covariance_sub_const_left 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	covariance Real.instSub	—	sub_eq_add_neg covariance_add_const_left
covariance_sub_const_right 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	covariance Real.instSub	—	sub_eq_add_neg covariance_add_const_right
covariance_sub_left 📖	mathematical	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	covariance Pi.instSub Real.instSub	—	Nat.instAtLeastTwoHAddOfNat sub_eq_add_neg covariance_add_left MeasureTheory.MemLp.neg covariance_neg_left
covariance_sub_right 📖	mathematical	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	covariance Pi.instSub Real.instSub	—	Nat.instAtLeastTwoHAddOfNat sub_eq_add_neg covariance_add_right MeasureTheory.MemLp.neg covariance_neg_right
covariance_sum_left 📖	mathematical	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	covariance Finset.sum Pi.addCommMonoid Real.instAddCommMonoid Finset.univ	—	Nat.instAtLeastTwoHAddOfNat covariance_sum_left'
covariance_sum_left' 📖	mathematical	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	covariance Finset.sum Pi.addCommMonoid Real.instAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat Finset.induction covariance_zero_left Finset.sum_insert covariance_add_left MeasureTheory.memLp_finset_sum' IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal
covariance_sum_right 📖	mathematical	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	covariance Finset.sum Pi.addCommMonoid Real.instAddCommMonoid Finset.univ	—	Nat.instAtLeastTwoHAddOfNat covariance_sum_right'
covariance_sum_right' 📖	mathematical	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	covariance Finset.sum Pi.addCommMonoid Real.instAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat covariance_comm covariance_sum_left' Finset.sum_congr
covariance_sum_sum 📖	mathematical	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	covariance Finset.sum Pi.addCommMonoid Real.instAddCommMonoid Finset.univ	—	Nat.instAtLeastTwoHAddOfNat covariance_sum_sum'
covariance_sum_sum' 📖	mathematical	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	covariance Finset.sum Pi.addCommMonoid Real.instAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat covariance_sum_left' MeasureTheory.memLp_finset_sum' IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Finset.sum_congr covariance_sum_right'
covariance_zero_left 📖	mathematical	—	covariance Pi.instZero Real Real.instZero	—	MeasureTheory.integral_zero sub_self MulZeroClass.zero_mul
covariance_zero_measure 📖	mathematical	—	covariance MeasureTheory.Measure MeasureTheory.Measure.instZero Real Real.instZero	—	MeasureTheory.integral_zero_measure sub_zero
covariance_zero_right 📖	mathematical	—	covariance Pi.instZero Real Real.instZero	—	MeasureTheory.integral_zero sub_self MulZeroClass.mul_zero

ProbabilityTheory.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
covariance_eq_zero 📖	mathematical	ProbabilityTheory.IndepFun Real Real.measurableSpace MeasureTheory.MemLp 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	ProbabilityTheory.covariance Real.instZero	—	Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.integral_eq_zero_of_ae Filter.mp_mem Filter.univ_mem' sub_self MulZeroClass.zero_mul MeasureTheory.MemLp.isProbabilityMeasure_of_indepFun BorelSpace.opensMeasurable Real.borelSpace ENNReal.instCharZero ProbabilityTheory.covariance_eq_sub integral_mul_eq_mul_integral MeasureTheory.MemLp.aestronglyMeasurable

---

← Back to Index