Commit 2025-12-15 20:43 6dd3a14d

View on Github →

chore: smaller imports in IonescuTulcea.traj (#32895) This file doesn't use the topology on the space of probability measures, so it shouldn't need to import ProbabilityMeasure. It did, for a lemma that deserves a version for IsProbabilityMeasure but only exists for ProbabilityMeasure. This PR adds the lemma, uses it in IonescuTulcea.traj, and trims the imports.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

modified theorem MeasureTheory.ProbabilityMeasure.nonempty

Modified Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean

added theorem MeasureTheory.nonempty_of_isProbabilityMeasure

Modified Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean

Modified Mathlib/Probability/ProductMeasure.lean