Theorem ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self'

Modification history

2025-10-03 10:42
Mathlib/Probability/Distributions/Fernique.lean
feat(Probability): Fernique's theorem for distributions that are invariant by rotation (#28343) …
Added ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self'View on Github →