Commit 2025-09-26 11:33 26e837d6

feat(MeasureTheory/ProbabilityTheory): Is(Probability/Finite)Measure iff map Is(Probability/Finite)Measure (#29922) Adds theorems stating that if the pushforward of a measure is a probability/finite measure than the original measure is a probability/finite measure. Add the corresponding iff theorems and HasLaw versions. I also thought that these theorems should be under the same namespace whereas currently isFiniteMeasure_map is under MeasureTheory.Measure but isProbabilityMeasure_map is under MeasureTheory. I felt it more appropriate that they be in the MeasureTheory.Measure namespace so I made that change and updated downstream accordingly but I could change both to MeasureTheory (no Measure) instead if preferred.