Independence

📁 Source: Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean

Statistics

Metric	Count
Definitions	0
Theorems iIndepFun_of_covariance_eq_zero, iIndepFun_of_covariance_eval, iIndepFun_of_covariance_inner, iIndepFun_of_covariance_strongDual, indepFun_of_covariance_eq_zero, indepFun_of_covariance_eval, indepFun_of_covariance_inner, indepFun_of_covariance_strongDual, hasGaussianLaw, hasGaussianLaw_sub_of_sub, hasGaussianLaw, hasGaussianLaw_add, hasGaussianLaw_fun_add, hasGaussianLaw_fun_sub, hasGaussianLaw_fun_sum, hasGaussianLaw_sub, hasGaussianLaw_sum	17
Total	17

ProbabilityTheory.HasGaussianLaw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iIndepFun_of_covariance_eq_zero 📖	mathematical	ProbabilityTheory.HasGaussianLaw Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid Pi.Function.module Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MeasurableSpace.pi Real.measurableSpace ProbabilityTheory.covariance Real.instZero	ProbabilityTheory.iIndepFun	—	iIndepFun_of_covariance_strongDual Real.instCompleteSpace Real.borelSpace instSecondCountableTopologyReal RingHomInvPair.instStarRingEnd RingHomIsometric.ids Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup conj_trivial instTrivialStarReal ProbabilityTheory.covariance_mul_const_right ProbabilityTheory.covariance_mul_const_left MulZeroClass.zero_mul
iIndepFun_of_covariance_eval 📖	mathematical	Finite ProbabilityTheory.HasGaussianLaw Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommMonoid Real.instAddCommMonoid Pi.module Real.semiring Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MeasurableSpace.pi Real.measurableSpace ProbabilityTheory.covariance Real.instZero	ProbabilityTheory.iIndepFun	—	isProbabilityMeasure Nat.instAtLeastTwoHAddOfNat ProbabilityTheory.iIndepFun.comp iIndepFun_of_covariance_inner fact_one_le_two_ennreal PiLp.completeSpace Real.instCompleteSpace PiLp.borelSpace Finite.to_countable Real.borelSpace instSecondCountableTopologyReal PiLp.secondCountableTopology map_equiv Pi.borelSpace TopologicalSpace.instSecondCountableTopologyForallOfCountable RingHomInvPair.ids OrthonormalBasis.sum_repr Finset.sum_congr sum_inner inner_smul_left ProbabilityTheory.covariance_fun_sum_fun_sum MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure conj_trivial instTrivialStarReal EuclideanSpace.basisFun_inner MeasureTheory.MemLp.const_mul memLp_two eval Finset.sum_eq_zero ProbabilityTheory.covariance_const_mul_left ProbabilityTheory.covariance_const_mul_right MulZeroClass.mul_zero WithLp.measurable_ofLp
iIndepFun_of_covariance_inner 📖	mathematical	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BorelSpace UniformSpace.toTopologicalSpace SecondCountableTopology ProbabilityTheory.HasGaussianLaw Pi.topologicalSpace Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.module Real Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike MeasurableSpace.pi ProbabilityTheory.covariance Inner.inner InnerProductSpace.toInner Real.instZero	ProbabilityTheory.iIndepFun	—	iIndepFun_of_covariance_strongDual RingHomInvPair.instStarRingEnd RingHomIsometric.ids Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup InnerProductSpace.toDual_symm_apply
iIndepFun_of_covariance_strongDual 📖	mathematical	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BorelSpace UniformSpace.toTopologicalSpace SecondCountableTopology ProbabilityTheory.HasGaussianLaw Pi.topologicalSpace Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.module Real Real.semiring NormedSpace.toModule Real.normedField MeasurableSpace.pi ProbabilityTheory.covariance DFunLike.coe StrongDual Real.pseudoMetricSpace ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instZero	ProbabilityTheory.iIndepFun	—	isProbabilityMeasure RingHomCompTriple.ids ProbabilityTheory.iIndepFun_iff_charFunDual_pi AEMeasurable.eval aemeasurable Finset.sum_congr DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass LinearMap.sum_single_apply Nat.instAtLeastTwoHAddOfNat charFunDual_map_eq_fun Pi.borelSpace Finite.to_countable Finset.prod_congr eval Finset.sum_sub_distrib MeasureTheory.integral_finset_sum MeasureTheory.Integrable.ofReal integrable Real.borelSpace Real.instCompleteSpace instSecondCountableTopologyReal map_fun ProbabilityTheory.variance_fun_sum MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure memLp_two Complex.instCharZero Finset.sum_eq_single_of_mem ProbabilityTheory.covariance_self
indepFun_of_covariance_eq_zero 📖	mathematical	ProbabilityTheory.HasGaussianLaw Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Prod.instAddCommMonoid Real.instAddCommMonoid Prod.instModule Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Prod.instMeasurableSpace Real.measurableSpace ProbabilityTheory.covariance Real.instZero	ProbabilityTheory.IndepFun	—	indepFun_of_covariance_strongDual Real.instCompleteSpace Real.borelSpace instSecondCountableTopologyReal RingHomInvPair.instStarRingEnd RingHomIsometric.ids Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup conj_trivial instTrivialStarReal ProbabilityTheory.covariance_mul_const_right ProbabilityTheory.covariance_mul_const_left MulZeroClass.zero_mul
indepFun_of_covariance_eval 📖	mathematical	ProbabilityTheory.HasGaussianLaw instTopologicalSpaceProd Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Prod.instAddCommMonoid Pi.addCommMonoid Real.instAddCommMonoid Prod.instModule Real.semiring Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Prod.instMeasurableSpace MeasurableSpace.pi Real.measurableSpace ProbabilityTheory.covariance Real.instZero	ProbabilityTheory.IndepFun	—	isProbabilityMeasure Nat.instAtLeastTwoHAddOfNat ProbabilityTheory.IndepFun.comp indepFun_of_covariance_inner fact_one_le_two_ennreal PiLp.completeSpace Real.instCompleteSpace PiLp.borelSpace Finite.to_countable Real.borelSpace instSecondCountableTopologyReal PiLp.secondCountableTopology map_equiv Prod.borelSpace Pi.borelSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable RingHomInvPair.ids OrthonormalBasis.sum_repr Finset.sum_congr sum_inner inner_smul_left ProbabilityTheory.covariance_fun_sum_fun_sum MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure conj_trivial instTrivialStarReal EuclideanSpace.basisFun_inner MeasureTheory.MemLp.const_mul memLp_two eval fst snd Finset.sum_eq_zero ProbabilityTheory.covariance_const_mul_left ProbabilityTheory.covariance_const_mul_right MulZeroClass.mul_zero WithLp.measurable_ofLp
indepFun_of_covariance_inner 📖	mathematical	ProbabilityTheory.HasGaussianLaw instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Prod.instModule Real Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Prod.instMeasurableSpace ProbabilityTheory.covariance Inner.inner InnerProductSpace.toInner Real.instZero	ProbabilityTheory.IndepFun	—	indepFun_of_covariance_strongDual RingHomInvPair.instStarRingEnd RingHomIsometric.ids Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup InnerProductSpace.toDual_symm_apply
indepFun_of_covariance_strongDual 📖	mathematical	ProbabilityTheory.HasGaussianLaw instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Prod.instModule Real Real.semiring NormedSpace.toModule Real.normedField Prod.instMeasurableSpace ProbabilityTheory.covariance DFunLike.coe StrongDual Real.pseudoMetricSpace ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instZero	ProbabilityTheory.IndepFun	—	isProbabilityMeasure RingHomCompTriple.ids ProbabilityTheory.indepFun_iff_charFunDual_prod MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure aemeasurable fst snd Nat.instAtLeastTwoHAddOfNat charFunDual_map_eq Prod.borelSpace secondCountableTopologyEither_of_right Complex.exp_add sub_add_sub_comm add_mul Distrib.rightDistribClass Complex.ofReal_add MeasureTheory.integral_add integrable Real.borelSpace Real.instCompleteSpace instSecondCountableTopologyReal map add_div ProbabilityTheory.variance_add memLp_two MulZeroClass.mul_zero add_zero

ProbabilityTheory.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasGaussianLaw 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField ProbabilityTheory.IndepFun	instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule Real.semiring Prod.instMeasurableSpace	—	ProbabilityTheory.HasGaussianLaw.isProbabilityMeasure instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat ProbabilityTheory.isGaussian_iff_gaussian_charFunDual TopologicalSpace.instSecondCountableTopologyProd CompleteSpace.prod Prod.borelSpace secondCountableTopologyEither_of_right MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure ProbabilityTheory.isPosSemidef_covarianceBilinDual RingHomCompTriple.ids ProbabilityTheory.indepFun_iff_charFunDual_prod ProbabilityTheory.HasGaussianLaw.aemeasurable add_zero zero_add map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Complex.ofReal_add add_mul Distrib.rightDistribClass add_div add_sub_add_comm Complex.exp_add ProbabilityTheory.IsGaussian.charFunDual_eq ProbabilityTheory.HasGaussianLaw.isGaussian_map integral_complex_ofReal ContinuousLinearMap.integral_comp_id_comm Real.instCompleteSpace ProbabilityTheory.IsGaussian.integrable_id ProbabilityTheory.covarianceBilinDual_self_eq_variance ProbabilityTheory.IsGaussian.memLp_two_id
hasGaussianLaw_sub_of_sub 📖	—	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField ProbabilityTheory.IndepFun Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	—	ProbabilityTheory.HasGaussianLaw.isProbabilityMeasure Nat.instAtLeastTwoHAddOfNat ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure AEMeasurable.sub' ContinuousSub.measurableSub₂ IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup ProbabilityTheory.HasGaussianLaw.aemeasurable mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq Pi.mul_apply charFunDual_map_add_eq_mul add_sub_cancel Complex.exp_add sub_add_sub_comm add_mul Distrib.rightDistribClass Complex.ofReal_add MeasureTheory.integral_add ProbabilityTheory.HasGaussianLaw.integrable Real.borelSpace Real.instCompleteSpace instSecondCountableTopologyReal ProbabilityTheory.HasGaussianLaw.map map_comp_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass MeasureTheory.Integrable.sub add_div variance_add ProbabilityTheory.HasGaussianLaw.memLp_two MeasureTheory.MemLp.sub comp ContinuousLinearMap.measurable BorelSpace.opensMeasurable map_sub

ProbabilityTheory.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasGaussianLaw 📖	mathematical	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BorelSpace UniformSpace.toTopologicalSpace SecondCountableTopology ProbabilityTheory.HasGaussianLaw ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField ProbabilityTheory.iIndepFun	Pi.topologicalSpace Pi.addCommMonoid Pi.module Real.semiring MeasurableSpace.pi	—	isProbabilityMeasure instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat ProbabilityTheory.isGaussian_iff_gaussian_charFunDual TopologicalSpace.instSecondCountableTopologyForallOfCountable Finite.to_countable Pi.complete Pi.borelSpace MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure ProbabilityTheory.isPosSemidef_covarianceBilinDual RingHomCompTriple.ids ProbabilityTheory.iIndepFun_iff_charFunDual_pi ProbabilityTheory.HasGaussianLaw.aemeasurable LinearMap.sum_single_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Complex.ofReal_sum Finset.sum_mul Finset.sum_div Complex.exp_sum ProbabilityTheory.IsGaussian.charFunDual_eq ProbabilityTheory.HasGaussianLaw.isGaussian_map integral_complex_ofReal ContinuousLinearMap.integral_comp_id_comm Real.instCompleteSpace ProbabilityTheory.IsGaussian.integrable_id ProbabilityTheory.covarianceBilinDual_self_eq_variance ProbabilityTheory.IsGaussian.memLp_two_id
hasGaussianLaw_add 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField ProbabilityTheory.IndepFun	Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	ProbabilityTheory.HasGaussianLaw.add ProbabilityTheory.IndepFun.hasGaussianLaw
hasGaussianLaw_fun_add 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField ProbabilityTheory.IndepFun	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	ProbabilityTheory.HasGaussianLaw.add ProbabilityTheory.IndepFun.hasGaussianLaw
hasGaussianLaw_fun_sub 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField ProbabilityTheory.IndepFun	SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	ProbabilityTheory.HasGaussianLaw.sub ProbabilityTheory.IndepFun.hasGaussianLaw
hasGaussianLaw_fun_sum 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField ProbabilityTheory.iIndepFun	Finset.sum Finset.univ	—	ProbabilityTheory.HasGaussianLaw.fun_sum hasGaussianLaw Finite.of_fintype
hasGaussianLaw_sub 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField ProbabilityTheory.IndepFun	Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	ProbabilityTheory.HasGaussianLaw.sub ProbabilityTheory.IndepFun.hasGaussianLaw
hasGaussianLaw_sum 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField ProbabilityTheory.iIndepFun	Finset.sum Pi.addCommMonoid Finset.univ	—	ProbabilityTheory.HasGaussianLaw.sum hasGaussianLaw Finite.of_fintype

---

← Back to Index