Canonical drifted Brownian paths satisfy every càdlàg and no-positive-jump Lévy interface

Proved

AvramDividend.Classical.canonical_drifted_brownian_cadlag_no_positive_jumps

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

brownian-motioncounterexample-auditlevy-processessample-paths

Every normalised, drifted canonical Brownian path is continuous. Consequently it is right-continuous and has a finite left limit at every positive time. Uniqueness of the left limit yields the no-positive-jumps property in the exact order and filter conventions used by AvramDividend.Classical.SpectrallyNegativeLevy.

Preamble

import Theorems.Thm_AvramDividend_Classical_canonical_drifted_brownian_zero_continuous
import Mathlib.Topology.Order.DenselyOrdered
import Mathlib.Tactic

open ProbabilityTheory MeasureTheory Filter Set Topology
open scoped NNReal

Formal statement

theorem AvramDividend.Classical.canonical_drifted_brownian_cadlag_no_positive_jumps
    (ω : ℝ≥0 → ℝ) :
    let X : ℝ≥0 → ℝ := fun t =>
      ProbabilityTheory.brownian t ω - ProbabilityTheory.brownian 0 ω - (t : ℝ)
    (∀ t : ℝ≥0, ContinuousWithinAt X (Ici t) t) ∧
    (∀ t : ℝ≥0, 0 < t → ∃ l : ℝ, Tendsto X (𝓝[<] t) (𝓝 l)) ∧
    (∀ (t : ℝ≥0) (l : ℝ), 0 < t →
       Tendsto X (𝓝[<] t) (𝓝 l) → X t ≤ l) := by sorry

Source

Accepted canonical_drifted_brownian_zero_continuous and standard continuous-path properties of one-sided neighbourhood filters.

View graph