Theorem ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero

Modification history

2025-10-09 08:14
Mathlib/Probability/Distributions/Gaussian/Fernique.lean
feat: Fernique's theorem for Gaussian distributions (#30167) …
Added ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zeroView on Github →