Commit 2025-04-20 11:58 51b4a8da

View on Github →

chore: replace (mu s).toReal with mu.real s, when mu is a measure, throughout the library (#24204) Also

  • add a minimal additional API to Measure.real when it helps streamline proofs
  • rename (and deprecate) a few lemmas when the change impacts their name
  • Move the definition of Measure.real to MeasureSpaceDefs to make sure that imports remain reasonable

Estimated changes

modified theorem MeasureTheory.average_eq
modified theorem MeasureTheory.charFun_zero
added theorem Real.volume_real_Icc
added theorem Real.volume_real_Ico
added theorem Real.volume_real_Ioc
added theorem Real.volume_real_Ioo
added theorem Real.volume_real_ball
modified theorem ProbabilityTheory.cgf_zero'
modified theorem ProbabilityTheory.mgf_zero'