Structures · Analysis
ProbabilityTheory.IsGaussian
A measure is Gaussian if its map by every continuous linear form is a real Gaussian measure.
- Shape
- One type argument · adds map_eq_gaussianReal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Real
- EuclideanSpace
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by39
- ProbabilityTheory.IsGaussian.integrable_id
- ProbabilityTheory.IsGaussian.memLp_two_id
- ProbabilityTheory.IsGaussian.charFunDual_eq
- ProbabilityTheory.IsGaussian.map_eq_gaussianReal
- ProbabilityTheory.IsGaussian.memLp_id
- ProbabilityTheory.IsGaussian.charFunDual_eq'
- ProbabilityTheory.IsGaussian.integral_dual
- ProbabilityTheory.IsGaussian.hasGaussianLaw_id
- ProbabilityTheory.HasLaw.hasGaussianLaw
- ProbabilityTheory.IsGaussian.charFun_eq
- ProbabilityTheory.IsGaussian.memLp_dual
- ProbabilityTheory.IsGaussian.charFunDual_eq_of_forall_strongDual_eq_zero
- ProbabilityTheory.IsGaussian.charFun_eq'
- ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero
- ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero
- ProbabilityTheory.IsGaussian.integrable_exp_sq_of_conv_neg
- ProbabilityTheory.IsGaussian.eq_dirac_of_variance_eq_zero
- ProbabilityTheory.IsGaussian.ext_covarianceBilinDual
- ProbabilityTheory.IsGaussian.integrable_dual
- ProbabilityTheory.isGaussian_map_of_measurable
- ProbabilityTheory.IsGaussian.nullSingletonClass
- ProbabilityTheory.IsGaussian.exists_integrable_exp_sq
- ProbabilityTheory.IsGaussian.integrable_fun_id
- ProbabilityTheory.isGaussian_map
- ProbabilityTheory.instIsGaussianMapHSub
- ProbabilityTheory.instIsGaussianMapHAdd
- ProbabilityTheory.isGaussian_conv
- ProbabilityTheory.instIsGaussianProdProdOfSecondCountableTopologyEither
- ProbabilityTheory.instIsGaussianMapHSub_1
- ProbabilityTheory.IsGaussian.ext_iff_covarianceBilinDual
- ProbabilityTheory.IsGaussian.map_rotation_eq_self
- ProbabilityTheory.IsGaussian.hasGaussianLaw
- ProbabilityTheory.IsGaussian.memLp_two_fun_id
- ProbabilityTheory.IsGaussian.noAtoms
- ProbabilityTheory.isGaussian_map_equiv
- ProbabilityTheory.instIsGaussianMapNeg
- ProbabilityTheory.IsGaussian.charFunDual_eq_of_integral_eq_zero
- ProbabilityTheory.instIsGaussianMapHAdd_1
- ProbabilityTheory.IsGaussian.toIsProbabilityMeasure
Ancestors0
No ancestors.