Basic

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

Statistics

Metric	Count
Definitions	0
Theorems add, aemeasurable, charFunDual_map_eq, charFunDual_map_eq_fun, charFun_map_eq, eval, fst, fun_add, fun_neg, fun_smul, fun_sub, fun_sum, integrable, isProbabilityMeasure, map, map_equiv, map_equiv_fun, map_fun, map_of_measurable, memLp, memLp_two, neg, prodMk, smul, snd, sub, sum, toLp_pi, toLp_prodMk, hasGaussianLaw, hasGaussianLaw, hasGaussianLaw_id, hasGaussianLaw_iff_charFunDual_map_eq, hasGaussianLaw_iff_charFun_map_eq	34
Total	34

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasGaussianLaw_iff_charFunDual_map_eq 📖	mathematical	AEMeasurable	HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField MeasureTheory.charFunDual MeasureTheory.Measure.map Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal DFunLike.coe StrongDual Real.semiring Real.pseudoMetricSpace ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid variance instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat HasGaussianLaw.charFunDual_map_eq isGaussian_iff_charFunDual_eq MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.integral_map Continuous.comp_aestronglyMeasurable Complex.continuous_ofReal Continuous.aestronglyMeasurable BorelSpace.opensMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal Continuous.clm_apply continuous_const SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_id' variance_map Measurable.aemeasurable ContinuousLinearMap.measurable Real.borelSpace integral_complex_ofReal
hasGaussianLaw_iff_charFun_map_eq 📖	mathematical	AEMeasurable	HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike MeasureTheory.charFun InnerProductSpace.toInner MeasureTheory.Measure.map Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal MeasureTheory.integral Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid variance Inner.inner instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat HasGaussianLaw.charFun_map_eq isGaussian_iff_charFun_eq MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.integral_map Continuous.comp_aestronglyMeasurable Complex.continuous_ofReal Continuous.aestronglyMeasurable BorelSpace.opensMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal Continuous.inner continuous_const continuous_id' variance_map Continuous.aemeasurable Real.borelSpace integral_complex_ofReal

ProbabilityTheory.HasGaussianLaw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	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	Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	map Prod.borelSpace secondCountableTopologyEither_of_right IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup
aemeasurable 📖	mathematical	ProbabilityTheory.HasGaussianLaw	AEMeasurable	—	AEMeasurable.of_map_ne_zero MeasureTheory.IsProbabilityMeasure.ne_zero ProbabilityTheory.IsGaussian.toIsProbabilityMeasure isGaussian_map
charFunDual_map_eq 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	MeasureTheory.charFunDual MeasureTheory.Measure.map Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal DFunLike.coe StrongDual Real.semiring Real.pseudoMetricSpace ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid ProbabilityTheory.variance instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat ProbabilityTheory.IsGaussian.charFunDual_eq isGaussian_map MeasureTheory.integral_map aemeasurable Continuous.comp_aestronglyMeasurable Complex.continuous_ofReal Continuous.aestronglyMeasurable BorelSpace.opensMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal Continuous.clm_apply continuous_const SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_id' ProbabilityTheory.variance_map Measurable.aemeasurable ContinuousLinearMap.measurable Real.borelSpace integral_complex_ofReal
charFunDual_map_eq_fun 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	MeasureTheory.charFunDual MeasureTheory.Measure.map Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal DFunLike.coe StrongDual Real.semiring Real.pseudoMetricSpace ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid ProbabilityTheory.variance instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat charFunDual_map_eq
charFun_map_eq 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike	MeasureTheory.charFun InnerProductSpace.toInner MeasureTheory.Measure.map Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal MeasureTheory.integral Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid ProbabilityTheory.variance Inner.inner instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat ProbabilityTheory.IsGaussian.charFun_eq isGaussian_map MeasureTheory.integral_map aemeasurable Continuous.comp_aestronglyMeasurable Complex.continuous_ofReal Continuous.aestronglyMeasurable BorelSpace.opensMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal Continuous.inner continuous_const continuous_id' ProbabilityTheory.variance_map Continuous.aemeasurable Real.borelSpace integral_complex_ofReal
eval 📖	—	BorelSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ProbabilityTheory.HasGaussianLaw Pi.topologicalSpace Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.module Real Real.semiring NormedSpace.toModule Real.normedField MeasurableSpace.pi	—	—	map_of_measurable BorelSpace.opensMeasurable measurable_pi_apply
fst 📖	—	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	—	—	map_of_measurable BorelSpace.opensMeasurable measurable_fst
fun_add 📖	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	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	add
fun_neg 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	neg
fun_smul 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring	—	smul
fun_sub 📖	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	SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	sub
fun_sum 📖	mathematical	ProbabilityTheory.HasGaussianLaw Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.Function.module Real Real.semiring NormedSpace.toModule Real.normedField MeasurableSpace.pi	Finset.sum Finset.univ	—	Finset.sum_apply sum
integrable 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	—	MeasureTheory.memLp_one_iff_integrable memLp
isProbabilityMeasure 📖	mathematical	ProbabilityTheory.HasGaussianLaw	MeasureTheory.IsProbabilityMeasure	—	MeasureTheory.Measure.isProbabilityMeasure_of_map ProbabilityTheory.IsGaussian.toIsProbabilityMeasure isGaussian_map
map 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	map_of_measurable BorelSpace.opensMeasurable ContinuousLinearMap.measurable
map_equiv 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	DFunLike.coe ContinuousLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike	—	RingHomInvPair.ids map
map_equiv_fun 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	DFunLike.coe ContinuousLinearEquiv Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike	—	RingHomInvPair.ids map_equiv
map_fun 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	map
map_of_measurable 📖	—	ProbabilityTheory.HasGaussianLaw Measurable DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	—	isGaussian_map AEMeasurable.map_map_of_aemeasurable Measurable.aemeasurable aemeasurable ProbabilityTheory.isGaussian_map_of_measurable
memLp 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	MeasureTheory.MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm	—	MeasureTheory.memLp_map_measure_iff aestronglyMeasurable_id PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable aemeasurable ProbabilityTheory.IsGaussian.memLp_id isGaussian_map
memLp_two 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	MeasureTheory.MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	—	memLp Nat.instAtLeastTwoHAddOfNat
neg 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	neg_smul one_smul smul
prodMk 📖	mathematical	BorelSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SecondCountableTopology ProbabilityTheory.HasGaussianLaw Pi.topologicalSpace Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.module Real Real.semiring NormedSpace.toModule Real.normedField MeasurableSpace.pi	instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule Prod.instMeasurableSpace	—	map Pi.borelSpace Finite.to_countable Prod.borelSpace secondCountableTopologyEither_of_right
smul 📖	mathematical	ProbabilityTheory.HasGaussianLaw UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField	Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring	—	map SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.left
snd 📖	—	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	—	—	map_of_measurable BorelSpace.opensMeasurable measurable_snd
sub 📖	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	Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	map Prod.borelSpace secondCountableTopologyEither_of_right SeminormedAddCommGroup.toIsTopologicalAddGroup
sum 📖	mathematical	ProbabilityTheory.HasGaussianLaw Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.Function.module Real Real.semiring NormedSpace.toModule Real.normedField MeasurableSpace.pi	Finset.sum Finset.univ	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Finset.sum_apply Finset.sum_congr ContinuousLinearMap.coe_sum' map Pi.borelSpace Finite.to_countable Finite.of_fintype
toLp_pi 📖	mathematical	BorelSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SecondCountableTopology ProbabilityTheory.HasGaussianLaw Pi.topologicalSpace Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.module Real Real.semiring NormedSpace.toModule Real.normedField MeasurableSpace.pi	WithLp PiLp.topologicalSpace PiLp.normedAddCommGroup WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup WithLp.measurableSpace WithLp.toLp	—	map_equiv Pi.borelSpace Finite.to_countable Finite.of_fintype PiLp.borelSpace RingHomInvPair.ids
toLp_prodMk 📖	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	WithLp WithLp.instProdTopologicalSpace WithLp.instProdNormedAddCommGroup WithLp.instModule Prod.instAddCommGroup SeminormedAddCommGroup.toAddCommGroup WithLp.measurableSpace WithLp.toLp	—	map_equiv Prod.borelSpace WithLp.borelSpace RingHomInvPair.ids

ProbabilityTheory.HasLaw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasGaussianLaw 📖	mathematical	ProbabilityTheory.HasLaw	ProbabilityTheory.HasGaussianLaw	—	map_eq

ProbabilityTheory.IsGaussian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasGaussianLaw 📖	mathematical	—	ProbabilityTheory.HasGaussianLaw	—	—
hasGaussianLaw_id 📖	mathematical	—	ProbabilityTheory.HasGaussianLaw	—	MeasureTheory.Measure.map_id

---

← Back to Index