Multivariate

📁 Source: Mathlib/Probability/Distributions/Gaussian/Multivariate.lean

Statistics

Metric	Count
Definitions multivariateGaussian, stdGaussian	2
Theorems charFunDual_stdGaussian, charFun_multivariateGaussian, charFun_stdGaussian, covarianceBilin_multivariateGaussian, covarianceBilin_stdGaussian, covariance_eval_multivariateGaussian, integral_id_multivariateGaussian, integral_id_multivariateGaussian', integral_id_stdGaussian, integral_strongDual_stdGaussian, isGaussian_multivariateGaussian, isGaussian_stdGaussian, isProbabilityMeasure_stdGaussian, map_pi_eq_stdGaussian, measurePreserving_eval_multivariateGaussian, measurePreserving_restrict₂_multivariateGaussian, multivariateGaussian_of_not_posSemidef, multivariateGaussian_zero_one, stdGaussian_eq_map_pi_orthonormalBasis, stdGaussian_map, variance_dual_stdGaussian, variance_eval_multivariateGaussian	22
Total	24

ProbabilityTheory

Definitions

Name	Category	Theorems
multivariateGaussian 📖	CompOp	11 math math: isGaussian_multivariateGaussian, covarianceBilin_multivariateGaussian, measurePreserving_restrict₂_multivariateGaussian, charFun_multivariateGaussian, multivariateGaussian_of_not_posSemidef, integral_id_multivariateGaussian, variance_eval_multivariateGaussian, measurePreserving_eval_multivariateGaussian, integral_id_multivariateGaussian', multivariateGaussian_zero_one, covariance_eval_multivariateGaussian
stdGaussian 📖	CompOp	12 math math: integral_id_stdGaussian, covarianceBilin_stdGaussian, map_pi_eq_stdGaussian, isProbabilityMeasure_stdGaussian, integral_strongDual_stdGaussian, variance_dual_stdGaussian, stdGaussian_map, charFun_stdGaussian, stdGaussian_eq_map_pi_orthonormalBasis, multivariateGaussian_zero_one, isGaussian_stdGaussian, charFunDual_stdGaussian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charFunDual_stdGaussian 📖	mathematical	—	MeasureTheory.charFunDual InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup stdGaussian Complex.exp Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm StrongDual Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.hasOpNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RCLike.toInnerProductSpaceReal RingHom.id Semiring.toNonAssocSemiring instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat IsGaussian.charFunDual_eq isGaussian_stdGaussian integral_complex_ofReal integral_strongDual_stdGaussian MulZeroClass.zero_mul variance_dual_stdGaussian Complex.ofReal_pow zero_sub neg_div
charFun_multivariateGaussian 📖	mathematical	Matrix.PosSemidef Real Real.instRing Real.partialOrder instStarRingReal	MeasureTheory.charFun EuclideanSpace Real WithLp.measurableSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasurableSpace.pi Real.measurableSpace InnerProductSpace.toInner Real.instRCLike PiLp.seminormedAddCommGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup PiLp.innerProductSpace RCLike.toInnerProductSpaceReal multivariateGaussian Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal Inner.inner Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid dotProduct Real.instMul Real.instAddCommMonoid WithLp.ofLp Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing Complex.instNatCast	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul PiLp.borelSpace Finite.to_countable Finite.of_fintype Real.borelSpace instSecondCountableTopologyReal IsGaussian.charFun_eq' PiLp.secondCountableTopology PiLp.completeSpace Real.instCompleteSpace isGaussian_multivariateGaussian integral_id_multivariateGaussian covarianceBilin_multivariateGaussian
charFun_stdGaussian 📖	mathematical	—	MeasureTheory.charFun InnerProductSpace.toInner Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup stdGaussian Complex.exp Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Norm.norm NormedAddCommGroup.toNorm instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat MeasureTheory.charFun_apply stdGaussian.eq_1 MeasureTheory.integral_map Measurable.aemeasurable Finset.measurable_sum ContinuousAdd.measurableMul₂ secondCountable_of_proper FiniteDimensional.proper_real IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Measurable.smul_const ContinuousSMul.toMeasurableSMul BorelSpace.opensMeasurable Real.borelSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul measurable_pi_apply Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace Complex.instProperSpace Complex.borelSpace Measurable.cexp Measurable.mul_const ContinuousMul.measurableMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Measurable.complex_ofReal Continuous.measurable Continuous.inner continuous_id' continuous_const sum_inner Complex.ofReal_sum Finset.sum_mul Complex.exp_sum MeasureTheory.integral_fintype_prod_eq_prod MeasureTheory.sigmaFinite_of_locallyFinite instSecondCountableTopologyReal MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace MeasureTheory.instInnerRegularCompactLTTopOfIsCompletelyPseudoMetrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureGaussianReal Finset.prod_congr real_inner_smul_left mul_comm Complex.ofReal_mul charFun_gaussianReal MulZeroClass.mul_zero MulZeroClass.zero_mul one_mul zero_sub Finset.sum_neg_distrib Finset.sum_congr OrthonormalBasis.sum_sq_inner_right neg_div
covarianceBilin_multivariateGaussian 📖	mathematical	Matrix.PosSemidef Real Real.instRing Real.partialOrder instStarRingReal	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring EuclideanSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Real.normedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike PiLp.innerProductSpace RCLike.toInnerProductSpaceReal NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace NormedAddCommGroup.toAddCommGroup Real.instAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul covarianceBilin WithLp.measurableSpace MeasurableSpace.pi Real.measurableSpace PiLp.borelSpace Finite.to_countable Finite.of_fintype Real.borelSpace instSecondCountableTopologyReal multivariateGaussian dotProduct WithLp.ofLp Matrix.mulVec	—	fact_one_le_two_ennreal IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul PiLp.completeSpace RCLike.toCompleteSpace IsScalarTower.right Matrix.instStarOrderedRing ContinuousFunctionalCalculus.toNonUnital IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Matrix.IsHermitian.instContinuousFunctionalCalculus Matrix.instNonnegSpectrumClass instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul PiLp.borelSpace Finite.to_countable Finite.of_fintype Real.borelSpace instSecondCountableTopologyReal MeasureTheory.Measure.map_map MeasurableAdd.measurable_const_add ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd ContinuousLinearMap.measurable BorelSpace.opensMeasurable covarianceBilin_map_const_add Real.instCompleteSpace IsGaussian.toIsProbabilityMeasure isGaussian_map isGaussian_stdGaussian RingHomInvPair.instStarRingEnd RingHomIsometric.ids smulCommClass_self covarianceBilin_map PiLp.secondCountableTopology MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure isProbabilityMeasure_stdGaussian IsGaussian.memLp_two_id covarianceBilin_stdGaussian IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing innerSL_apply_apply ContinuousLinearMap.adjoint_inner_left IsSelfAdjoint.adjoint_eq IsSelfAdjoint.map NonUnitalStarRingHomClass.toStarHomClass NonUnitalAlgHomClass.toNonUnitalRingHomClass Real.isBoundedSMul instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass StarAlgEquiv.instNonUnitalAlgEquivClass NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass RingEquivClass.toNonUnitalRingHomClass NonUnitalAlgEquivClass.toRingEquivClass StarRingEquivClass.instNonUnitalStarRingHomClass StarAlgEquiv.instStarRingEquivClass LE.le.isSelfAdjoint CFC.sqrt_nonneg RingHomCompTriple.ids ContinuousLinearMap.comp_apply ContinuousLinearMap.mul_def map_mul NonUnitalAlgSemiHomClass.toMulHomClass CFC.sqrt_mul_sqrt_self Matrix.topologicalRing instT2SpaceMatrix TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Matrix.PosSemidef.nonneg Nat.instAtLeastTwoHAddOfNat Matrix.inner_toEuclideanCLM
covarianceBilin_stdGaussian 📖	mathematical	—	covarianceBilin stdGaussian innerSL Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul gaussian_charFun_congr secondCountable_of_proper FiniteDimensional.proper_real complete_of_proper MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure isProbabilityMeasure_stdGaussian LinearMap.BilinForm.isPosSemidef_iff isPosSemidef_inner Nat.instAtLeastTwoHAddOfNat charFun_stdGaussian neg_div inner_zero_right MulZeroClass.zero_mul SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing innerSL_apply_apply inner_self_eq_norm_sq_to_K Complex.ofReal_pow zero_sub
covariance_eval_multivariateGaussian 📖	mathematical	Matrix.PosSemidef Real Real.instRing Real.partialOrder instStarRingReal	covariance EuclideanSpace Real WithLp.measurableSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasurableSpace.pi Real.measurableSpace WithLp.ofLp multivariateGaussian	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal EuclideanSpace.basisFun_apply Finset.sum_congr PiLp.single_apply MonoidWithZeroHom.map_ite_one_zero RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq' instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul PiLp.borelSpace Finite.to_countable Finite.of_fintype Real.borelSpace instSecondCountableTopologyReal covarianceBilin_apply_eq_cov PiLp.completeSpace Real.instCompleteSpace MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IsGaussian.toIsProbabilityMeasure isGaussian_multivariateGaussian IsGaussian.memLp_two_id PiLp.secondCountableTopology covarianceBilin_multivariateGaussian Matrix.mulVec_single one_smul single_dotProduct one_mul
integral_id_multivariateGaussian 📖	mathematical	—	MeasureTheory.integral EuclideanSpace Real PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Real.normedAddCommGroup PiLp.normedSpace Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal WithLp.measurableSpace MeasurableSpace.pi Real.measurableSpace multivariateGaussian	—	fact_one_le_two_ennreal Matrix.instStarOrderedRing Matrix.instNonnegSpectrumClass multivariateGaussian.eq_1 MeasureTheory.integral_map AEMeasurable.const_add ContinuousAdd.measurableAdd PiLp.borelSpace Finite.to_countable Finite.of_fintype Real.borelSpace instSecondCountableTopologyReal instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Measurable.aemeasurable ContinuousLinearMap.measurable BorelSpace.opensMeasurable aestronglyMeasurable_id PseudoEMetricSpace.pseudoMetrizableSpace PiLp.secondCountableTopology MeasureTheory.integral_add MeasureTheory.integrable_const MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure isProbabilityMeasure_stdGaussian MeasureTheory.Integrable.comp_measurable IsGaussian.integrable_id isGaussian_map isGaussian_stdGaussian PiLp.completeSpace Real.instCompleteSpace MeasureTheory.integral_const MeasureTheory.probReal_univ one_smul ContinuousLinearMap.integral_comp_comm IsGaussian.integrable_fun_id integral_id_stdGaussian map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass add_zero
integral_id_multivariateGaussian' 📖	mathematical	—	MeasureTheory.integral EuclideanSpace Real PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Real.normedAddCommGroup PiLp.normedSpace Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal WithLp.measurableSpace MeasurableSpace.pi Real.measurableSpace multivariateGaussian	—	fact_one_le_two_ennreal integral_id_multivariateGaussian
integral_id_stdGaussian 📖	mathematical	—	MeasureTheory.integral InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup stdGaussian NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	stdGaussian.eq_1 MeasureTheory.integral_map Measurable.aemeasurable Finset.measurable_sum ContinuousAdd.measurableMul₂ secondCountable_of_proper FiniteDimensional.proper_real IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Measurable.smul_const ContinuousSMul.toMeasurableSMul BorelSpace.opensMeasurable Real.borelSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul measurable_pi_apply aestronglyMeasurable_id PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.integral_finset_sum MeasureTheory.Integrable.smul_const MeasureTheory.integrable_eval MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureGaussianReal IsGaussian.integrable_id isGaussian_gaussianReal Real.instCompleteSpace instSecondCountableTopologyReal Finset.sum_congr integral_smul_const complete_of_proper MeasureTheory.integral_eval integral_id_gaussianReal zero_smul Finset.sum_const_zero
integral_strongDual_stdGaussian 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal stdGaussian DFunLike.coe StrongDual Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instZero	—	ContinuousLinearMap.integral_comp_id_comm complete_of_proper FiniteDimensional.proper_real Real.instCompleteSpace IsGaussian.integrable_id isGaussian_stdGaussian secondCountable_of_proper integral_id_stdGaussian map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
isGaussian_multivariateGaussian 📖	mathematical	—	IsGaussian EuclideanSpace Real PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.normedAddCommGroup fact_one_le_two_ennreal Real.normedAddCommGroup WithLp.instModule Real.semiring Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring Real.instRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal WithLp.measurableSpace MeasurableSpace.pi Real.measurableSpace multivariateGaussian	—	fact_one_le_two_ennreal IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul PiLp.completeSpace RCLike.toCompleteSpace IsScalarTower.right Matrix.instStarOrderedRing ContinuousFunctionalCalculus.toNonUnital IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Matrix.IsHermitian.instContinuousFunctionalCalculus Matrix.instNonnegSpectrumClass MeasureTheory.Measure.map_map MeasurableAdd.measurable_const_add ContinuousAdd.measurableAdd PiLp.borelSpace Finite.to_countable Finite.of_fintype Real.borelSpace instSecondCountableTopologyReal instSeparatelyContinuousAddOfContinuousAdd ContinuousLinearMap.measurable BorelSpace.opensMeasurable instIsGaussianMapHAdd_1 isGaussian_map isGaussian_stdGaussian
isGaussian_stdGaussian 📖	mathematical	—	IsGaussian UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike stdGaussian	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul Nat.instAtLeastTwoHAddOfNat isGaussian_iff_gaussian_charFun secondCountable_of_proper FiniteDimensional.proper_real complete_of_proper MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure isProbabilityMeasure_stdGaussian LinearMap.BilinForm.isPosSemidef_iff isPosSemidef_inner charFun_stdGaussian neg_div inner_zero_right MulZeroClass.zero_mul SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing innerSL_apply_apply inner_self_eq_norm_sq_to_K Complex.ofReal_pow zero_sub
isProbabilityMeasure_stdGaussian 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure stdGaussian	—	MeasureTheory.Measure.isProbabilityMeasure_map MeasureTheory.Measure.pi.instIsProbabilityMeasure instIsProbabilityMeasureGaussianReal Measurable.aemeasurable Finset.measurable_sum ContinuousAdd.measurableMul₂ secondCountable_of_proper FiniteDimensional.proper_real IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Measurable.smul_const ContinuousSMul.toMeasurableSMul BorelSpace.opensMeasurable Real.borelSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul measurable_pi_apply
map_pi_eq_stdGaussian 📖	mathematical	—	MeasureTheory.Measure.map WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasurableSpace.pi Real Real.measurableSpace WithLp.measurableSpace WithLp.toLp MeasureTheory.Measure.pi gaussianReal Real.instZero NNReal NNReal.instOne stdGaussian EuclideanSpace PiLp.normedAddCommGroup fact_one_le_two_ennreal Real.normedAddCommGroup PiLp.innerProductSpace Real.instRCLike RCLike.toInnerProductSpaceReal WithLp.instModuleFinite DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Real.instDivisionRing Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedSpace.toModule FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real	—	MeasureTheory.Measure.ext_of_charFun Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real PiLp.borelSpace Finite.to_countable Real.borelSpace instSecondCountableTopologyReal PiLp.secondCountableTopology PiLp.completeSpace Real.instCompleteSpace MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.Measure.pi.instIsFiniteMeasure MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureGaussianReal isProbabilityMeasure_stdGaussian charFun_stdGaussian MeasureTheory.charFun_pi MeasureTheory.sigmaFinite_of_locallyFinite MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.instInnerRegularCompactLTTopOfIsCompletelyPseudoMetrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Finset.prod_congr charFun_gaussianReal Finset.sum_congr EuclideanSpace.real_norm_sq_eq MulZeroClass.mul_zero MulZeroClass.zero_mul Complex.ofReal_pow one_mul zero_sub Finset.sum_neg_distrib Complex.ofReal_sum neg_div Finset.sum_div
measurePreserving_eval_multivariateGaussian 📖	mathematical	Matrix.PosSemidef Real Real.instRing Real.partialOrder instStarRingReal	MeasureTheory.MeasurePreserving EuclideanSpace Real WithLp.measurableSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasurableSpace.pi Real.measurableSpace WithLp.ofLp multivariateGaussian gaussianReal Real.toNNReal	—	Measurable.fun_comp measurable_pi_apply WithLp.measurable_ofLp EuclideanSpace.coe_proj IsGaussian.map_eq_gaussianReal isGaussian_multivariateGaussian fact_one_le_two_ennreal ContinuousLinearMap.integral_comp_id_comm PiLp.completeSpace Real.instCompleteSpace IsGaussian.integrable_id PiLp.borelSpace Finite.to_countable Finite.of_fintype Real.borelSpace instSecondCountableTopologyReal PiLp.secondCountableTopology integral_id_multivariateGaussian variance_eval_multivariateGaussian
measurePreserving_restrict₂_multivariateGaussian 📖	mathematical	Matrix.PosSemidef Finset SetLike.instMembership Finset.instSetLike Real Real.instRing Real.partialOrder instStarRingReal Finset.instHasSubset	MeasureTheory.MeasurePreserving EuclideanSpace Real Finset SetLike.instMembership Finset.instSetLike WithLp.measurableSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasurableSpace.pi Real.measurableSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike RingHom.id Semiring.toNonAssocSemiring PiLp.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.normedAddCommGroup fact_one_le_two_ennreal Finset.Subtype.fintype NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace ContinuousLinearMap.funLike EuclideanSpace.restrict₂ multivariateGaussian Matrix.submatrix	—	fact_one_le_two_ennreal ContinuousLinearMap.measurable BorelSpace.opensMeasurable PiLp.borelSpace Finite.to_countable Finite.of_fintype Real.borelSpace instSecondCountableTopologyReal IsGaussian.ext PiLp.secondCountableTopology PiLp.completeSpace Real.instCompleteSpace isGaussian_map isGaussian_multivariateGaussian integral_id_multivariateGaussian ContinuousLinearMap.integral_id_map IsGaussian.integrable_id instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing LinearMap.BilinForm.ext_basis ContinuousLinearMap.toBilinForm_apply covarianceBilin_apply_eq_cov MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IsGaussian.toIsProbabilityMeasure IsGaussian.memLp_two_id covariance_map Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace Continuous.measurable Continuous.inner Nat.instAtLeastTwoHAddOfNat continuous_const continuous_id' Measurable.aemeasurable EuclideanSpace.basisFun_apply Finset.sum_congr PiLp.single_apply MonoidWithZeroHom.map_ite_one_zero RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq' covariance_eval_multivariateGaussian covarianceBilin_multivariateGaussian Matrix.PosSemidef.submatrix Matrix.mulVec_single one_smul single_dotProduct one_mul
multivariateGaussian_of_not_posSemidef 📖	mathematical	Matrix.PosSemidef Real Real.instRing Real.partialOrder instStarRingReal	multivariateGaussian MeasureTheory.Measure.dirac EuclideanSpace Real WithLp.measurableSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasurableSpace.pi Real.measurableSpace	—	fact_one_le_two_ennreal Matrix.instStarOrderedRing Matrix.instNonnegSpectrumClass multivariateGaussian.eq_1 NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instNonUnitalContinuousFunctionalCalculus CFC.sqrt.eq_1 cfcₙ_apply_of_not_predicate sub_zero IsScalarTower.right map_zero MonoidWithZeroHomClass.toZeroHomClass IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass WithLp.instIsScalarTower Pi.isScalarTower UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul PiLp.instIsBoundedSMul Real.isBoundedSMul AlgEquivClass.toAlgHomClass instAlgEquivClassOfNonUnitalAlgEquivClass StarAlgEquiv.instNonUnitalAlgEquivClass add_zero MeasureTheory.Measure.map_const MeasureTheory.IsProbabilityMeasure.measure_univ isProbabilityMeasure_stdGaussian PiLp.borelSpace Finite.to_countable Finite.of_fintype Real.borelSpace instSecondCountableTopologyReal one_smul
multivariateGaussian_zero_one 📖	mathematical	—	multivariateGaussian EuclideanSpace Real NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithLp.instAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Pi.addCommGroup Real.instAddCommGroup Matrix Matrix.one Real.instZero Real.instOne stdGaussian PiLp.normedAddCommGroup fact_one_le_two_ennreal Real.normedAddCommGroup PiLp.innerProductSpace Real.instRCLike RCLike.toInnerProductSpaceReal WithLp.instModuleFinite DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Real.instDivisionRing SeminormedAddCommGroup.toAddCommGroup Pi.module Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedSpace.toModule FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real WithLp.measurableSpace MeasurableSpace.pi Real.measurableSpace	—	fact_one_le_two_ennreal WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real Matrix.instStarOrderedRing Matrix.instNonnegSpectrumClass CFC.sqrt_one Matrix.IsHermitian.instContinuousFunctionalCalculus IsTopologicalRing.toIsSemitopologicalRing Matrix.topologicalRing instIsTopologicalRingReal instT2SpaceMatrix TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace map_one MonoidHomClass.toOneHomClass IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass WithLp.instIsScalarTower Pi.isScalarTower IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul PiLp.instIsBoundedSMul Real.isBoundedSMul AlgEquivClass.toAlgHomClass instAlgEquivClassOfNonUnitalAlgEquivClass StarAlgEquiv.instNonUnitalAlgEquivClass zero_add MeasureTheory.Measure.map_id'
stdGaussian_eq_map_pi_orthonormalBasis 📖	mathematical	—	stdGaussian MeasureTheory.Measure.map MeasurableSpace.pi Real Real.measurableSpace Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike DFunLike.coe OrthonormalBasis OrthonormalBasis.instFunLike MeasureTheory.Measure.pi gaussianReal Real.instZero NNReal NNReal.instOne	—	RingHomInvPair.ids fact_one_le_two_ennreal Nat.instAtLeastTwoHAddOfNat OrthonormalBasis.equiv_apply_euclideanSpace MeasureTheory.Measure.map_map Continuous.measurable BorelSpace.opensMeasurable PiLp.borelSpace Finite.to_countable Finite.of_fintype Real.borelSpace instSecondCountableTopologyReal ContinuousMapClass.map_continuous ContinuousSemilinearMapClass.toContinuousMapClass SemilinearIsometryClass.toContinuousSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass WithLp.measurable_toLp WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' FiniteDimensional.rclike_to_real map_pi_eq_stdGaussian LinearEquiv.finiteDimensional stdGaussian_map
stdGaussian_map 📖	mathematical	—	MeasureTheory.Measure.map DFunLike.coe LinearIsometryEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike stdGaussian LinearEquiv.finiteDimensional Real.instDivisionRing NormedAddCommGroup.toAddCommGroup LinearIsometryEquiv.toLinearEquiv	—	RingHomInvPair.ids LinearEquiv.finiteDimensional MeasureTheory.Measure.ext_of_charFunDual secondCountable_of_proper FiniteDimensional.proper_real complete_of_proper MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure isProbabilityMeasure_stdGaussian RingHomCompTriple.ids MeasureTheory.charFunDual_map BorelSpace.opensMeasurable Nat.instAtLeastTwoHAddOfNat charFunDual_stdGaussian ContinuousLinearMap.opNorm_comp_linearIsometryEquiv RingHomIsometric.ids
variance_dual_stdGaussian 📖	mathematical	—	variance DFunLike.coe StrongDual Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule stdGaussian Monoid.toPow Real.instMonoid Norm.norm ContinuousLinearMap.hasOpNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RCLike.toInnerProductSpaceReal	—	stdGaussian.eq_1 variance_map Continuous.aemeasurable BorelSpace.opensMeasurable Real.borelSpace ContinuousLinearMap.continuous Measurable.aemeasurable Finset.measurable_sum ContinuousAdd.measurableMul₂ secondCountable_of_proper FiniteDimensional.proper_real IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Measurable.smul_const ContinuousSMul.toMeasurableSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul measurable_pi_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass mul_comm Finset.sum_apply variance_sum_pi instIsProbabilityMeasureGaussianReal MeasureTheory.MemLp.const_mul Nat.instAtLeastTwoHAddOfNat IsGaussian.memLp_two_id isGaussian_gaussianReal Real.instCompleteSpace instSecondCountableTopologyReal variance_const_mul variance_id_gaussianReal OrthonormalBasis.norm_dual mul_one
variance_eval_multivariateGaussian 📖	mathematical	Matrix.PosSemidef Real Real.instRing Real.partialOrder instStarRingReal	variance EuclideanSpace Real WithLp.measurableSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasurableSpace.pi Real.measurableSpace WithLp.ofLp multivariateGaussian	—	covariance_self Measurable.aemeasurable Measurable.fun_comp measurable_pi_apply WithLp.measurable_ofLp covariance_eval_multivariateGaussian

---

← Back to Index