Right-continuous record regulators carry no Stieltjes mass on nonpositive times

Proved

AvramDividend.Classical.reflectedPath_dividendMeasure_zero_nonpositive

by WillR · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

avram-classicalright-continuousrunning-recordstieltjesstrong-markov

For any right-continuous path whose monotone running record M is represented by the supremum over [0,t] and dominates the path, the Stieltjes dividend measure generated by M has no mass on (-∞,0]. The result applies to the post-first-upcrossing future-increment running record without requiring the shifted process to be constructed as another Lévy object.

Preamble

import Mathlib.MeasureTheory.Measure.Stieltjes
import Mathlib.Topology.Order.LeftRightLim
import Mathlib.Data.NNReal.Defs
import Definitions.Def_AvramDividend_Classical_DividendStrategy
import Theorems.Thm_AvramDividend_Classical_runningSup_right_continuous_of_right_continuous
import Theorems.Thm_AvramDividend_Classical_rightLim_comp_toNNReal_of_rightContinuous
import Theorems.Thm_AvramDividend_Classical_dividendMeasure_Iic_zero_of_monotone_rightLim

open MeasureTheory Set Filter Topology
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.reflectedPath_dividendMeasure_zero_nonpositive
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    (f M : ℝ≥0 → ℝ)
    (hM : Monotone M) (hdom : ∀ t, f t ≤ M t)
    (hrepr : ∀ t, M t =
      ⨆ s : Set.Icc (0 : ℝ≥0) t, f s.1)
    (hfRight : ∀ t, Tendsto f (𝓝[≥] t) (𝓝 (f t)))
    (ω : Ω) :
    dividendMeasure (fun t (_ : Ω) => M t) ω
      (Set.Iic (0 : ℝ)) = 0 := by
  sorry

Source

Direct missing hνneg hypothesis of map-shift theorem 3093890e-4ed7-4198-8491-5f41d268763c for strong-Markov child 79978d61-9d1f-4b20-b8a5-114797a8e380. Uses proved generic running-record right-continuity f0c2320c and rightLim extension 95b3270f with pending generic Stieltjes support lemma ab1b11d7.

View graph