Def

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

Statistics

Metric	Count
Definitions HasGaussianLaw	1
Theorems isGaussian_map	1
Total	2

ProbabilityTheory

Definitions

Name	Category	Theorems
HasGaussianLaw 📖	CompData	46 math math: hasGaussianLaw_iff_charFunDual_map_eq, hasGaussianLaw_iff_charFun_map_eq, HasGaussianLaw.toLp_pi, IsGaussianProcess.hasGaussianLaw_fun_sum, HasGaussianLaw.smul, HasGaussianLaw.neg, IsGaussianProcess.hasGaussianLaw, iIndepFun.hasGaussianLaw_fun_sum, IsGaussianProcess.hasGaussianLaw_add, IsGaussianProcess.hasGaussianLaw_fun_add, HasGaussianLaw.add, HasGaussianLaw.fun_smul, iIndepFun.hasGaussianLaw_add, HasGaussianLaw.congr, HasGaussianLaw.map, IsGaussianProcess.hasGaussianLaw_increments, IsGaussianProcess.hasGaussianLaw_eval, HasGaussianLaw.fun_add, HasGaussianLaw.fun_sub, HasGaussianLaw.fun_neg, HasGaussianLaw.map_of_measurable, HasGaussianLaw.sub, HasGaussianLaw.map_fun, iIndepFun.hasGaussianLaw_fun_add, IsGaussianProcess.hasGaussianLaw_prodMk, iIndepFun.hasGaussianLaw, HasGaussianLaw.map_equiv, HasGaussianLaw.prodMk, iIndepFun.hasGaussianLaw_sub, HasGaussianLaw.fun_sum, HasGaussianLaw.map_equiv_fun, HasGaussianLaw.snd, IsGaussianProcess.hasGaussianLaw_sum, IndepFun.hasGaussianLaw, IsGaussianProcess.hasGaussianLaw_fun_sub, iIndepFun.hasGaussianLaw_sum, IsGaussian.hasGaussianLaw, HasGaussianLaw.fst, IndepFun.hasGaussianLaw_sub_of_sub, IsGaussianProcess.hasGaussianLaw_sub, HasGaussianLaw.toLp_prodMk, HasGaussianLaw.eval, IsGaussian.hasGaussianLaw_id, HasGaussianLaw.sum, HasLaw.hasGaussianLaw, iIndepFun.hasGaussianLaw_fun_sub

ProbabilityTheory.HasGaussianLaw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGaussian_map 📖	mathematical	ProbabilityTheory.HasGaussianLaw	ProbabilityTheory.IsGaussian MeasureTheory.Measure.map	—	—

---

← Back to Index