Commit 2025-11-14 10:06 df3de5d8

View on Github →

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

Estimated changes

Modified Mathlib/Probability/Moments/CovarianceBilin.lean

modified theorem ProbabilityTheory.covarianceBilin_comm

modified theorem ProbabilityTheory.covarianceBilin_of_not_memLp

modified theorem ProbabilityTheory.covarianceBilin_self_nonneg

modified theorem ProbabilityTheory.isPosSemidef_covarianceBilin

Modified Mathlib/Probability/Moments/CovarianceBilinDual.lean

added theorem MeasureTheory.memLp_id_of_self_sub_integral

added theorem ProbabilityTheory.covarianceBilinDual_of_not_memLp'