Commit 2024-08-15 14:22 665c7ae3

feat(MeasureTheory): method of exhaustion (#14471) If μ, ν are two measures with ν s-finite, then there exists a set s such that μ is sigma-finite on s, and for all sets t ⊆ sᶜ, either ν t = 0 or μ t = ∞. The technique used to obtain this result is what Halmos calls the "method of exhaustion". We use this to prove that if μ ≪ ν and ν is s-finite, then μ is s-finite. This PR also moves the definition of sigmaFiniteSet to the new file and refactors it with the new definition sigmaFiniteSetWRT.