Independence

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

Statistics

Metric	Count
Definitions	0
Theorems iIndepFun_of_covariance_eq_zero, iIndepFun_of_covariance_inner, iIndepFun_of_covariance_strongDual, indepFun_of_covariance_eq_zero, indepFun_of_covariance_inner, indepFun_of_covariance_strongDual	6
Total	6

ProbabilityTheory.IsGaussianProcess

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iIndepFun_of_covariance_eq_zero 📖	mathematical	ProbabilityTheory.IsGaussianProcess Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal AEMeasurable ProbabilityTheory.covariance Real.instZero	ProbabilityTheory.iIndepFun MeasurableSpace.pi Real Real.measurableSpace	—	iIndepFun_of_covariance_inner Real.borelSpace instSecondCountableTopologyReal Real.instCompleteSpace conj_trivial instTrivialStarReal ProbabilityTheory.covariance_mul_const_right ProbabilityTheory.covariance_mul_const_left MulZeroClass.zero_mul
iIndepFun_of_covariance_inner 📖	mathematical	ProbabilityTheory.IsGaussianProcess UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike AEMeasurable ProbabilityTheory.covariance Inner.inner InnerProductSpace.toInner Real.instZero	ProbabilityTheory.iIndepFun MeasurableSpace.pi	—	iIndepFun_of_covariance_strongDual RingHomInvPair.instStarRingEnd RingHomIsometric.ids Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup InnerProductSpace.toDual_symm_apply
iIndepFun_of_covariance_strongDual 📖	mathematical	ProbabilityTheory.IsGaussianProcess UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField AEMeasurable ProbabilityTheory.covariance DFunLike.coe StrongDual Real.semiring Real.pseudoMetricSpace ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instZero	ProbabilityTheory.iIndepFun MeasurableSpace.pi	—	isProbabilityMeasure ProbabilityTheory.iIndepFun.iIndepFun_process₀ ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_strongDual Finite.of_fintype Pi.complete Pi.borelSpace Finite.to_countable TopologicalSpace.instSecondCountableTopologyForallOfCountable continuous_pi continuous_apply ProbabilityTheory.HasGaussianLaw.map hasGaussianLaw RingHomCompTriple.ids ContinuousLinearMap.sum_comp_single Finset.sum_congr Finset.sum_apply ProbabilityTheory.covariance_sum_sum MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure ProbabilityTheory.HasGaussianLaw.memLp_two Real.borelSpace Real.instCompleteSpace instSecondCountableTopologyReal hasGaussianLaw_eval Finset.sum_eq_zero
indepFun_of_covariance_eq_zero 📖	mathematical	ProbabilityTheory.IsGaussianProcess Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal AEMeasurable ProbabilityTheory.covariance Real.instZero	ProbabilityTheory.IndepFun MeasurableSpace.pi Real Real.measurableSpace	—	indepFun_of_covariance_inner Real.borelSpace instSecondCountableTopologyReal Real.instCompleteSpace conj_trivial instTrivialStarReal ProbabilityTheory.covariance_mul_const_right ProbabilityTheory.covariance_mul_const_left MulZeroClass.zero_mul
indepFun_of_covariance_inner 📖	mathematical	ProbabilityTheory.IsGaussianProcess UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike AEMeasurable ProbabilityTheory.covariance Inner.inner InnerProductSpace.toInner Real.instZero	ProbabilityTheory.IndepFun MeasurableSpace.pi	—	indepFun_of_covariance_strongDual RingHomInvPair.instStarRingEnd RingHomIsometric.ids Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup InnerProductSpace.toDual_symm_apply
indepFun_of_covariance_strongDual 📖	mathematical	ProbabilityTheory.IsGaussianProcess UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField AEMeasurable ProbabilityTheory.covariance DFunLike.coe StrongDual Real.semiring Real.pseudoMetricSpace ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instZero	ProbabilityTheory.IndepFun MeasurableSpace.pi	—	isProbabilityMeasure ProbabilityTheory.IndepFun.process_indepFun_process₀ ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_strongDual Pi.complete Pi.borelSpace Finite.to_countable Finite.of_fintype TopologicalSpace.instSecondCountableTopologyForallOfCountable Finset.inl_mem_disjSum Finset.inr_mem_disjSum Continuous.prodMk continuous_pi continuous_apply ProbabilityTheory.HasGaussianLaw.map Prod.borelSpace secondCountableTopologyEither_of_right hasGaussianLaw RingHomCompTriple.ids ContinuousLinearMap.sum_comp_single Finset.sum_congr Finset.sum_apply ProbabilityTheory.covariance_sum_sum MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure ProbabilityTheory.HasGaussianLaw.memLp_two Real.borelSpace Real.instCompleteSpace instSecondCountableTopologyReal hasGaussianLaw_eval Finset.sum_eq_zero

---

← Back to Index