A finite sum of marked right-continuous jump steps has an exact left limit obtained by excluding marks at the current time

Proved

AvramDividend.Classical.finite_marked_step_sum_left_limit

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

avram-classicalcadlagjump-identificationleft-limitmarked-step-processpoisson

Given finitely many marked times tau_i≥0 and real weights w_i, define a right-continuous step path F(s)=Σ_{i∈S} (if tau_i≤s then w_i else 0). At every t≥0 the limit from strictly earlier times equals Σ_{i∈S} (if tau_i<t then w_i else 0). The theorem also handles simultaneous marked times exactly: all marks with tau_i=t are excluded from the left limit. It is the deterministic jump-path identity needed to identify canonical finite-band Poisson marks with càdlàg process jumps before passing through the compensated infinite-annulus limit.

Preamble

import Mathlib.Probability.IdentDistrib
import Mathlib.Data.NNReal.Basic
import Mathlib.Topology.Algebra.Monoid
import Mathlib.Topology.Order.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic

open Filter Set Topology
open scoped NNReal BigOperators

Formal statement

theorem AvramDividend.Classical.finite_marked_step_sum_left_limit
    {ι : Type*} (S : Finset ι) (τ : ι → ℝ≥0) (w : ι → ℝ) (t : ℝ≥0) :
    Tendsto
      (fun s : ℝ≥0 => ∑ i ∈ S, if τ i ≤ s then w i else 0)
      (nhdsWithin t (Iio t))
      (nhds (∑ i ∈ S, if τ i < t then w i else 0)) := by sorry

Source

LeanLevy/RandomMeasure/LevyJumpPath.lean defines finite bandStepFinsetSum as sums of right-continuous marked steps; Mathlib tendsto_finsetSum and one-sided neighbourhoods.

View graph