Canonical normalised and drifted Brownian coordinates are measurable
ProvedAvramDividend.Classical.canonical_drifted_brownian_measurablebrownian-motioncounterexample-auditfiltrationlevy-processes
Every coordinate of the canonical continuous Brownian modification is measurable. Taking differences of two coordinates and subtracting a deterministic time preserves measurability. This is needed to construct the natural filtration and the exact Avram Lévy-process adaptedness field.
Preamble
import Definitions.Def_KLSModular_BrownianMotion_Gaussian_BrownianMotion import Mathlib.Probability.Process.Filtration open ProbabilityTheory MeasureTheory open scoped NNReal
Formal statement
theorem AvramDividend.Classical.canonical_drifted_brownian_measurable
(t : ℝ≥0) :
Measurable (fun ω : ℝ≥0 → ℝ =>
ProbabilityTheory.brownian t ω - ProbabilityTheory.brownian 0 ω - (t : ℝ)) := by sorrySource
Canonical Brownian Kolmogorov–Chentsov modification measurable-coordinate certificate.