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	15 math math: hasGaussianLaw_iff_charFunDual_map_eq, hasGaussianLaw_iff_charFun_map_eq, IsGaussianProcess.hasGaussianLaw_fun_sum, IsGaussianProcess.hasGaussianLaw, IsGaussianProcess.hasGaussianLaw_add, IsGaussianProcess.hasGaussianLaw_fun_add, IsGaussianProcess.hasGaussianLaw_increments, IsGaussianProcess.hasGaussianLaw_eval, IsGaussianProcess.hasGaussianLaw_prodMk, IsGaussianProcess.hasGaussianLaw_sum, IsGaussianProcess.hasGaussianLaw_fun_sub, IsGaussian.hasGaussianLaw, IsGaussianProcess.hasGaussianLaw_sub, IsGaussian.hasGaussianLaw_id, HasLaw.hasGaussianLaw

ProbabilityTheory.HasGaussianLaw

Theorems

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

---

← Back to Index