Continuity of a locally finite cumulative measure on an atom-free positive half-line
ProvedAvramDividend.Classical.continuousOn_cumulative_toReal_of_ac_positiveabsolute-continuityavram-classicalbounded-variationcdfm2m4measure-theoryrenewal-resolvent
Let β be a measure on the real line whose cumulative mass β((-∞,x]) is finite for every x. If β restricted to (0,∞) is absolutely continuous with respect to Lebesgue measure, then x↦β((-∞,x]).toReal is continuous on (0,∞). Right continuity is the usual continuity-from-above property of measures; the left jump at x is β({x}), which vanishes on the positive half-line by absolute continuity.
Preamble
import Mathlib open MeasureTheory Filter Set Topology open scoped ENNReal
Formal statement
namespace AvramDividend.Classical
/-- If every lower cumulative interval has finite mass and the restriction of a measure to the positive half-line is absolutely continuous with respect to Lebesgue measure, then its real-valued cumulative function is continuous on the positive half-line. -/
theorem continuousOn_cumulative_toReal_of_ac_positive
(β : Measure ℝ)
(hfin : ∀ x : ℝ, β (Iic x) ≠ ∞)
(hac : β.restrict (Ioi (0 : ℝ)) ≪ (volume : Measure ℝ)) :
ContinuousOn (fun x : ℝ => (β (Iic x)).toReal) (Ioi (0 : ℝ)) := by
sorry
end AvramDividend.ClassicalSource
Pinned Mathlib measure continuity from monotone set limits, measure_sdiff, volume_singleton, ENNReal.toReal, and Monotone.continuousAt_iff_leftLim_eq_rightLim. This generic CDF regularity bridge is needed to identify the Avram bounded-variation geometric renewal cumulative pointwise by Laplace uniqueness.