Theorem ProbabilityTheory.covarianceBilinDual_of_not_memLp'

Modification history

2025-11-14 10:06

Mathlib/Probability/Moments/CovarianceBilinDual.lean

feat: drop a finiteness assumptions in covariance results (#31569)

Added ProbabilityTheory.covarianceBilinDual_of_not_memLp'View on Github →