Theorem ProbabilityTheory.IsGaussian.integrable_fun_id

Modification history

2026-05-17 17:16
Mathlib/Probability/Distributions/Gaussian/Fernique.lean
feat(Tactic/ToFun): allow configuring the name of the generated declaration (#34257) …
Deleted ProbabilityTheory.IsGaussian.integrable_fun_idView on Github →
2025-10-09 08:14
Mathlib/Probability/Distributions/Gaussian/Fernique.lean
feat: Fernique's theorem for Gaussian distributions (#30167) …
Added ProbabilityTheory.IsGaussian.integrable_fun_idView on Github →