Theorem ProbabilityTheory.IsGaussian.memLp_two_id

Modification history

2026-09-22 11:41
Mathlib/Probability/Distributions/Gaussian/Fernique.lean
chore: use simp instead of norm_num where simp suffices (#43035) …
Modified ProbabilityTheory.IsGaussian.memLp_two_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.memLp_two_idView on Github →