Commit 2024-11-14 11:25 59fe8aee

View on Github →

feat(MeasurePreserving): add add_measure and smul_measure (#18953)

  • Generalize Measure.map_smul to work with c of any type.
  • Weaken TC assumptions in ae_smul_measure, add ae_smul_measure_le.
  • Add AbsolutelyContinuous.smul_both.
  • Add MeasurePreserving.add_measure, MeasurePreserving.smul_measure.
  • Add PreErgodic.smul_measure, QuasiErgodic.smul_measure, Ergodic.smul_measure.

Estimated changes

added theorem Ergodic.smul_measure