Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `IsGaussian`	1
Theorems `charFunDual_eq`, `charFun_eq`, `eq_gaussianReal`, `integrable_dual`, `map_eq_gaussianReal`, `memLp_dual`, `toIsProbabilityMeasure`, `instIsGaussianDirac`, `instIsGaussianMapHAdd`, `instIsGaussianMapHAdd_1`, `instIsGaussianMapHSub`, `instIsGaussianMapHSub_1`, `instIsGaussianMapNeg`, `instIsGaussianProdProdOfSecondCountableTopologyEither`, `isGaussian_conv`, `isGaussian_gaussianReal`, `isGaussian_iff_charFunDual_eq`, `isGaussian_iff_charFun_eq`, `isGaussian_map`, `isGaussian_map_equiv`, `isGaussian_map_equiv_iff`, `isGaussian_map_of_measurable`, `isGaussian_of_charFunDual_eq`, `isGaussian_of_isGaussian_map`, `isGaussian_of_map_eq_gaussianReal`	25
Total	26

ProbabilityTheory

Definitions

Name	Category	Theorems
`IsGaussian` 📖	CompData	20 math math: `isGaussian_iff_gaussian_charFun`, `isGaussian_map_equiv_iff`, `instIsGaussianMapHSub`, `isGaussian_iff_charFun_eq`, `instIsGaussianDirac`, `isGaussian_gaussianReal`, `isGaussian_map`, `isGaussian_map_of_measurable`, `isGaussian_iff_gaussian_charFunDual`, `isGaussian_of_map_eq_gaussianReal`, `instIsGaussianMapHAdd_1`, `isGaussian_conv`, `HasGaussianLaw.isGaussian_map`, `isGaussian_iff_charFunDual_eq`, `isGaussian_of_charFunDual_eq`, `isGaussian_map_equiv`, `instIsGaussianMapHAdd`, `instIsGaussianProdProdOfSecondCountableTopologyEither`, `instIsGaussianMapHSub_1`, `instIsGaussianMapNeg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsGaussianDirac` 📖	mathematical	—	`IsGaussian` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `MeasureTheory.Measure.dirac`	—	`MeasureTheory.Measure.map_dirac` `ContinuousLinearMap.measurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `MeasureTheory.integral_dirac` `Real.instCompleteSpace` `OpensMeasurableSpace.toMeasurableSingletonClass` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `variance_dirac` `Real.toNNReal_zero` `gaussianReal_zero_var`
`instIsGaussianMapHAdd` 📖	mathematical	—	`IsGaussian` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `MeasureTheory.Measure.map` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`isGaussian_of_charFunDual_eq` `MeasureTheory.Measure.isFiniteMeasure_map` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `IsGaussian.toIsProbabilityMeasure` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.charFunDual_map_add_const` `IsGaussian.charFunDual_eq` `Complex.exp_add` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `variance_map` `Measurable.aemeasurable` `ContinuousLinearMap.measurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `AEMeasurable.add_const` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `aemeasurable_id` `MeasureTheory.integral_map` `Continuous.comp_aestronglyMeasurable` `Complex.continuous_ofReal` `Continuous.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `Continuous.clm_apply` `continuous_const` `continuous_id'` `variance_add_const` `integral_complex_ofReal` `MeasureTheory.integral_add` `IsGaussian.integrable_dual` `MeasureTheory.integrable_const` `MeasureTheory.integral_const` `Real.instCompleteSpace` `MeasureTheory.probReal_univ` `one_mul` `Complex.ofReal_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Complex.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt`
`instIsGaussianMapHAdd_1` 📖	mathematical	—	`IsGaussian` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `MeasureTheory.Measure.map` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`add_comm` `instIsGaussianMapHAdd`
`instIsGaussianMapHSub` 📖	mathematical	—	`IsGaussian` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `MeasureTheory.Measure.map` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `instIsGaussianMapHAdd`
`instIsGaussianMapHSub_1` 📖	mathematical	—	`IsGaussian` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `MeasureTheory.Measure.map` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `instIsGaussianMapHAdd_1` `instIsGaussianMapNeg` `MeasureTheory.Measure.map_map` `Measurable.const_add` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `measurable_id'` `Measurable.neg` `ContinuousNeg.measurableNeg` `IsTopologicalAddGroup.toContinuousNeg`
`instIsGaussianMapNeg` 📖	mathematical	—	`IsGaussian` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `MeasureTheory.Measure.map` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `isGaussian_map_equiv`
`instIsGaussianProdProdOfSecondCountableTopologyEither` 📖	mathematical	—	`IsGaussian` `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` `MeasureTheory.Measure.prod`	—	`isGaussian_of_charFunDual_eq` `Prod.borelSpace` `MeasureTheory.Measure.prod.instIsFiniteMeasure` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `IsGaussian.toIsProbabilityMeasure` `Nat.instAtLeastTwoHAddOfNat` `RingHomCompTriple.ids` `MeasureTheory.charFunDual_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `IsGaussian.charFunDual_eq` `Complex.exp_add` `sub_add_sub_comm` `add_mul` `Distrib.rightDistribClass` `integral_complex_ofReal` `MeasureTheory.integral_continuousLinearMap_prod'` `Real.instCompleteSpace` `IsGaussian.integrable_dual` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `Complex.instCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `variance_dual_prod'` `IsGaussian.memLp_dual`
`isGaussian_conv` 📖	mathematical	—	`IsGaussian` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `MeasureTheory.Measure.conv` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid`	—	`MeasureTheory.Measure.map_conv_continuousLinearMap` `ContinuousAdd.measurableMul₂` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Real.borelSpace` `instSecondCountableTopologyReal` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `BorelSpace.opensMeasurable` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `IsGaussian.toIsProbabilityMeasure` `MeasureTheory.integral_map` `Measurable.aemeasurable` `ContinuousLinearMap.measurable` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `variance_id_map` `IsGaussian.map_eq_gaussianReal` `gaussianReal_conv_gaussianReal` `integral_id_gaussianReal` `variance_id_gaussianReal` `sup_of_le_left` `Real.toNNReal_add`
`isGaussian_gaussianReal` 📖	mathematical	—	`IsGaussian` `Real` `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` `Real.measurableSpace` `gaussianReal`	—	`gaussianReal_map_continuousLinearMap` `integral_continuousLinearMap_gaussianReal` `variance_continuousLinearMap_gaussianReal` `Real.toNNReal_mul` `le_max_of_le_left` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Nat.instAtLeastTwoHAddOfNat` `even_two_mul` `Real.toNNReal_coe`
`isGaussian_iff_charFunDual_eq` 📖	mathematical	—	`IsGaussian` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `MeasureTheory.charFunDual` `Complex.exp` `Complex` `Complex.instSub` `Complex.instMul` `MeasureTheory.integral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `Complex.ofReal` `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` `IsGaussian.charFunDual_eq` `MeasureTheory.Measure.ext_of_charFun` `Real.borelSpace` `instSecondCountableTopologyReal` `Real.instCompleteSpace` `MeasureTheory.Measure.isFiniteMeasure_map` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasureGaussianReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.charFun_map_eq_charFunDual_smul` `BorelSpace.opensMeasurable` `charFun_gaussianReal` `Complex.ofReal_mul` `MeasureTheory.integral_const_mul` `integral_complex_ofReal` `max_eq_left` `variance_nonneg` `mul_comm` `Complex.ofReal_pow` `variance_const_mul`
`isGaussian_iff_charFun_eq` 📖	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` `MeasureTheory.charFun` `InnerProductSpace.toInner` `Complex.exp` `Complex` `Complex.instSub` `Complex.instMul` `MeasureTheory.integral` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.ofReal` `Complex.I` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `variance` `Inner.inner` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `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` `Function.Surjective.forall` `LinearIsometryEquiv.surjective` `MeasureTheory.charFun_eq_charFunDual_toDualMap` `innerSL_apply_norm` `LinearIsometryEquiv.coe_ofSurjective`
`isGaussian_map` 📖	mathematical	—	`IsGaussian` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `MeasureTheory.Measure.map` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	—	`isGaussian_map_of_measurable` `BorelSpace.opensMeasurable` `ContinuousLinearMap.measurable`
`isGaussian_map_equiv` 📖	mathematical	—	`IsGaussian` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `MeasureTheory.Measure.map` `DFunLike.coe` `ContinuousLinearEquiv` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike`	—	`RingHomInvPair.ids` `isGaussian_map`
`isGaussian_map_equiv_iff` 📖	mathematical	—	`IsGaussian` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `MeasureTheory.Measure.map` `DFunLike.coe` `ContinuousLinearEquiv` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike`	—	`RingHomInvPair.ids` `MeasureTheory.Measure.map_map` `Continuous.measurable` `BorelSpace.opensMeasurable` `ContinuousMapClass.map_continuous` `ContinuousSemilinearMapClass.toContinuousMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass` `ContinuousLinearEquiv.symm_comp_self` `MeasureTheory.Measure.map_id` `isGaussian_map_equiv`
`isGaussian_map_of_measurable` 📖	mathematical	`Measurable` `DFunLike.coe` `ContinuousLinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	`IsGaussian` `MeasureTheory.Measure.map`	—	`isGaussian_of_map_eq_gaussianReal` `RingHomCompTriple.ids` `MeasureTheory.Measure.map_map` `Continuous.measurable` `Real.borelSpace` `ContinuousLinearMap.continuous` `ContinuousLinearMap.coe_comp'` `IsGaussian.map_eq_gaussianReal`
`isGaussian_of_charFunDual_eq` 📖	mathematical	`MeasureTheory.charFunDual` `Complex.exp` `Complex` `Complex.instSub` `Complex.instMul` `MeasureTheory.integral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.ofReal` `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` `Complex.I` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `variance` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`IsGaussian`	—	`Nat.instAtLeastTwoHAddOfNat` `isGaussian_iff_charFunDual_eq`
`isGaussian_of_isGaussian_map` 📖	—	`IsGaussian` `Real` `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` `Real.measurableSpace` `MeasureTheory.Measure.map` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	—	—	`IsGaussian.eq_gaussianReal` `MeasureTheory.integral_map` `Continuous.aemeasurable` `Real.borelSpace` `ContinuousLinearMap.continuous` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `instSecondCountableTopologyReal` `variance_map` `aemeasurable_id` `CompTriple.comp_eq` `CompTriple.instId_comp` `CompTriple.instIsIdId`
`isGaussian_of_map_eq_gaussianReal` 📖	mathematical	`MeasureTheory.Measure.map` `Real` `Real.measurableSpace` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `ContinuousLinearMap.funLike` `gaussianReal`	`IsGaussian`	—	`isGaussian_of_isGaussian_map` `isGaussian_gaussianReal`

ProbabilityTheory.IsGaussian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charFunDual_eq` 📖	mathematical	—	`MeasureTheory.charFunDual` `Complex.exp` `Complex` `Complex.instSub` `Complex.instMul` `MeasureTheory.integral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.ofReal` `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` `Complex.I` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `ProbabilityTheory.variance` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.charFunDual_eq_charFun_map_one` `BorelSpace.opensMeasurable` `map_eq_gaussianReal` `ProbabilityTheory.charFun_gaussianReal` `one_mul` `one_pow` `mul_one` `integral_complex_ofReal` `ProbabilityTheory.variance_nonneg`
`charFun_eq` 📖	mathematical	—	`MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.exp` `Complex` `Complex.instSub` `Complex.instMul` `MeasureTheory.integral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instInnerProductSpaceRealComplex` `Complex.ofReal` `Complex.I` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `ProbabilityTheory.variance` `Inner.inner` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.charFun_eq_charFunDual_toDualMap` `charFunDual_eq`
`eq_gaussianReal` 📖	mathematical	—	`ProbabilityTheory.gaussianReal` `MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.measurableSpace` `Real.toNNReal` `ProbabilityTheory.variance`	—	`MeasureTheory.Measure.map_id` `map_eq_gaussianReal`
`integrable_dual` 📖	mathematical	—	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `DFunLike.coe` `StrongDual` `Real.semiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`MeasureTheory.memLp_one_iff_integrable` `memLp_dual`
`map_eq_gaussianReal` 📖	mathematical	—	`MeasureTheory.Measure.map` `Real` `Real.measurableSpace` `DFunLike.coe` `StrongDual` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `ProbabilityTheory.gaussianReal` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.toNNReal` `ProbabilityTheory.variance`	—	—
`memLp_dual` 📖	mathematical	—	`MeasureTheory.MemLp` `Real` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Real.pseudoMetricSpace` `DFunLike.coe` `StrongDual` `Real.semiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`MeasureTheory.memLp_map_measure_iff` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `Measurable.aemeasurable` `ContinuousLinearMap.measurable` `map_eq_gaussianReal` `ENNReal.coe_toNNReal` `ProbabilityTheory.memLp_id_gaussianReal`
`toIsProbabilityMeasure` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure`	—	`map_eq_gaussianReal` `MeasureTheory.integral_zero` `MeasureTheory.IsProbabilityMeasure.measure_univ` `ProbabilityTheory.instIsProbabilityMeasureGaussianReal` `MeasureTheory.Measure.map_apply` `measurable_zero` `MeasurableSet.univ`

---

← Back to Index