Pre-Brownian motion relative to a filtration

Mathlib's ProbabilityTheory.IsPreBrownianReal prescribes only the finite-dimensional laws of W. A martingale statement needs a filtration, and the law of W alone does not say how W interacts with it: TauCeti.Probability.IsFilteredPreBrownianReal ℱ W P adds that W is adapted to ℱ and that every increment W_t - W_s, s ≤ t, is independent of ℱ_s. A pre-Brownian motion is a pre-Brownian motion relative to its own natural filtration (ProbabilityTheory.IsPreBrownianReal.isFilteredPreBrownianReal_natural). Conversely, an adapted process started at 0 whose increments W_t - W_s have law N(0, t - s) and are independent of ℱ_s is a pre-Brownian motion relative to ℱ (MeasureTheory.Adapted.isFilteredPreBrownianReal); this is how a change of measure is shown to produce a new Brownian motion.

Main declarations

• TauCeti.Probability.IsFilteredPreBrownianReal: a pre-Brownian motion relative to a filtration.
• ProbabilityTheory.IsPreBrownianReal.isFilteredPreBrownianReal_natural: the natural filtration.
• ProbabilityTheory.IsPreBrownianReal.hasLaw_sub_of_le: for s ≤ t, the increment W_t - W_s has law N(0, t - s).
• MeasureTheory.Adapted.isFilteredPreBrownianReal: the characterization by Gaussian increments independent of the past.

References

• I. Karatzas, S. E. Shreve, Brownian Motion and Stochastic Calculus, Springer, 1991, §2.1.

structure TauCeti.Probability.IsFilteredPreBrownianReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (ℱ : MeasureTheory.Filtration NNReal mΩ) (W : NNReal → Ω → ℝ) (P : MeasureTheory.Measure Ω := by volume_tac) extends ProbabilityTheory.IsPreBrownianReal W P : Prop

W is a pre-Brownian motion relative to the filtration ℱ under P: its finite-dimensional laws are those of Brownian motion, it is adapted to ℱ, and for s ≤ t the increment W t - W s is independent of ℱ s.

• hasLaw (I : Finset NNReal) : HasLaw (fun (ω : Ω) => I.restrict fun (x : NNReal) => W x ω) (BrownianReal.projectiveFamily I) P
• adapted : MeasureTheory.Adapted ℱ W

  W t is ℱ t-measurable.

• indep_sub ⦃s t : NNReal⦄ : s ≤ t → ProbabilityTheory.Indep (MeasurableSpace.comap (W t - W s) inferInstance) (↑ℱ s) P

  The increment W t - W s is independent of ℱ s.

theorem TauCeti.Probability.IsFilteredPreBrownianReal.indepFun_eval_of_measurable_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : IsFilteredPreBrownianReal ℱ W P) {E : Type u_2} [MeasurableSpace E] {ξ : Ω → E} (hξ : Measurable ξ) (t : NNReal) : ProbabilityTheory.IndepFun (W t) ξ P

A Brownian value is independent of every random variable known at time zero.

theorem TauCeti.Probability.IsFilteredPreBrownianReal.congr {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {B W : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsFilteredPreBrownianReal ℱ B P) (hW : MeasureTheory.Adapted ℱ W) (h : ∀ (t : NNReal), B t =ᵐ[P] W t) : IsFilteredPreBrownianReal ℱ W P

Fixed-time almost-sure equality preserves the filtered pre-Brownian property, provided the replacement is adapted to the same filtration. Adaptedness is not inferred from a.e. equality on a raw filtration.

theorem ProbabilityTheory.IsPreBrownianReal.isFilteredPreBrownianReal_natural {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ} (hB : IsPreBrownianReal B P) (hmeas : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) : TauCeti.Probability.IsFilteredPreBrownianReal (MeasureTheory.Filtration.natural B hmeas) B P

A pre-Brownian motion is a pre-Brownian motion relative to its natural filtration: by the weak Markov property ProbabilityTheory.IsPreBrownianReal.indepFun_shift, the increments after time s are independent of (B u, u ≤ s).

theorem ProbabilityTheory.IsPreBrownianReal.hasLaw_sub_of_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ} (hB : IsPreBrownianReal B P) {s t : NNReal} (hst : s ≤ t) : HasLaw (B t - B s) (gaussianReal 0 (t - s)) P

For s ≤ t, the increment B t - B s of a pre-Brownian motion has law N(0, t - s).

theorem MeasureTheory.Adapted.isFilteredPreBrownianReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : Measure Ω} {ℱ : Filtration NNReal mΩ} {X : NNReal → Ω → ℝ} (hX : Adapted ℱ X) (h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0) (hlaw : ∀ ⦃s t : NNReal⦄, s ≤ t → ProbabilityTheory.HasLaw (X t - X s) (ProbabilityTheory.gaussianReal 0 (t - s)) P) (hindep : ∀ ⦃s t : NNReal⦄, s ≤ t → ProbabilityTheory.Indep (MeasurableSpace.comap (X t - X s) inferInstance) (↑ℱ s) P) : TauCeti.Probability.IsFilteredPreBrownianReal ℱ X P

An adapted process that starts at 0 and whose increments X t - X s, s ≤ t, have law N(0, t - s) and are independent of ℱ s is a pre-Brownian motion relative to ℱ.