Theorem ProbabilityTheory.HasGaussianLaw.integrable

Modification history

2026-01-26 14:59

Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean

feat: add a predicate HasGaussianLaw (#32144) …

Added ProbabilityTheory.HasGaussianLaw.integrable View on Github →