Commit 2024-04-03 09:14 d6ce8fc2

feat: drop completeness assumptions in theorems involving integrals (#11840) When computing the integral of a function taking values in a noncomplete space, we use the junk value 0. This means that several theorems about integrals hold without completeness assumptions for trivial reasons. We use this to drop several completeness assumptions here and there in mathlib. This involves one nontrivial mathematical fact, that E →L[𝕜] F is complete iff F is complete, for which we add the missing direction (from left to right) in this PR.