The drifted canonical Brownian process is adapted to its natural filtration

Proved

AvramDividend.Classical.canonical_drifted_brownian_natural_adapted

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

brownian-motioncounterexample-auditfiltrationlevy-processes

The normalised and drifted canonical Brownian process has measurable coordinates. Its natural filtration is therefore well-defined and the process is adapted to that filtration. The theorem explicitly packages the measurability witness and adaptation needed by the Avram spectrally negative Lévy structure.

Preamble

import Theorems.Thm_AvramDividend_Classical_canonical_drifted_brownian_measurable
import Mathlib.Probability.Process.Adapted
import Mathlib.Tactic

open ProbabilityTheory MeasureTheory
open scoped NNReal

Formal statement

theorem AvramDividend.Classical.canonical_drifted_brownian_natural_adapted :
    let X : ℝ≥0 → (ℝ≥0 → ℝ) → ℝ := fun t ω =>
      ProbabilityTheory.brownian t ω - ProbabilityTheory.brownian 0 ω - (t : ℝ)
    ∃ hmeas : ∀ t : ℝ≥0, StronglyMeasurable (X t),
      Adapted (Filtration.natural X hmeas) X := by sorry

Source

Mathlib Filtration.natural and Filtration.stronglyAdapted_natural; accepted canonical_drifted_brownian_measurable.

View graph