Brownian motion

theorem ProbabilityTheory.IsPreBrownianReal.hasLaw_gaussianLimit {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hX : IsPreBrownianReal X P) (hXm : AEMeasurable (fun (ω : Ω) (x : NNReal) => X x ω) P) : HasLaw (fun (ω : Ω) (x : NNReal) => X x ω) gaussianLimit P

theorem ProbabilityTheory.HasLaw.IsPreBrownianReal {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hX : HasLaw (fun (ω : Ω) (x : NNReal) => X x ω) gaussianLimit P) : ProbabilityTheory.IsPreBrownianReal X P

theorem ProbabilityTheory.IsPreBrownianReal.isAEKolmogorovProcess {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} {n : ℕ} (hn : 0 < n) (h : IsPreBrownianReal X P) : IsAEKolmogorovProcess X P (2 * ↑n) ↑n ↑(2 * n - 1).doubleFactorial

theorem ProbabilityTheory.IsPreBrownianReal.exists_continuous_modification {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (h : IsPreBrownianReal X P) : ∃ (Y : NNReal → Ω → ℝ), (∀ (t : NNReal), Measurable (Y t)) ∧ (∀ (t : NNReal), Y t =ᵐ[P] X t) ∧ ∀ (ω : Ω) (t β : NNReal), 0 < β → ↑β < ⨆ (n : ℕ), (↑(n + 2) - 1) / (2 * ↑(n + 2)) → ∃ U ∈ nhds t, ∃ (C : NNReal), HolderOnWith C β (fun (x : NNReal) => Y x ω) U

If X is a pre-Brownian process then there exists a modification of X which is measurable and locally β-Hölder for 0 < β < 1/2 (and thus continuous). See IsPreBrownianReal.mk.

noncomputable def ProbabilityTheory.IsPreBrownianReal.mk {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (X : NNReal → Ω → ℝ) (h : IsPreBrownianReal X P) : NNReal → Ω → ℝ

If h : IsPreBrownianReal X P, then h.mk X is a continuous modification of X.

Equations

• ProbabilityTheory.IsPreBrownianReal.mk X h = ⋯.choose

theorem ProbabilityTheory.IsPreBrownianReal.memHolder_mk {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (h : IsPreBrownianReal X P) (ω : Ω) (t β : NNReal) (hβ_pos : 0 < β) (hβ_lt : β < 2⁻¹) : ∃ U ∈ nhds t, ∃ (C : NNReal), HolderOnWith C β (fun (x : NNReal) => IsPreBrownianReal.mk X h x ω) U

theorem ProbabilityTheory.IsPreBrownianReal.measurable_mk {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (h : IsPreBrownianReal X P) (t : NNReal) : Measurable (IsPreBrownianReal.mk X h t)

theorem ProbabilityTheory.IsPreBrownianReal.mk_ae_eq {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (h : IsPreBrownianReal X P) (t : NNReal) : IsPreBrownianReal.mk X h t =ᵐ[P] X t

theorem ProbabilityTheory.IsPreBrownianReal.continuous_mk {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (h : IsPreBrownianReal X P) (ω : Ω) : Continuous fun (x : NNReal) => IsPreBrownianReal.mk X h x ω

class ProbabilityTheory.IsFilteredPreBrownian {Ω : Type u_2} {mΩ : MeasurableSpace Ω} (X : NNReal → Ω → ℝ) (𝓕 : MeasureTheory.Filtration NNReal mΩ) (P : MeasureTheory.Measure Ω) extends ProbabilityTheory.IsPreBrownianReal X P : Prop

A pre-Brownian motion X is filtered with respect to a filtration 𝓕 if it is adapted to 𝓕 and the increments of X after time t are independent of 𝓕 t

• hasLaw (I : Finset NNReal) : HasLaw (fun (ω : Ω) => I.restrict fun (x : NNReal) => X x ω) (BrownianReal.projectiveFamily I) P
• stronglyAdapted : MeasureTheory.StronglyAdapted 𝓕 X
• indep (s t : NNReal) : s ≤ t → Indep (MeasurableSpace.comap (X t - X s) inferInstance) (↑𝓕 s) P

theorem ProbabilityTheory.IsPreBrownianReal.isFilteredPreBrownian {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (h : IsPreBrownianReal X P) (hX : ∀ (t : NNReal), Measurable (X t)) : IsFilteredPreBrownian X (MeasureTheory.Filtration.natural X ⋯) P

theorem ProbabilityTheory.IsPreBrownianReal.isMartingale {Ω : Type u_2} {mΩ : MeasurableSpace Ω} (X : NNReal → Ω → ℝ) (𝓕 : MeasureTheory.Filtration NNReal mΩ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] [hX : IsFilteredPreBrownian X 𝓕 P] : MeasureTheory.Martingale X 𝓕 P

theorem ProbabilityTheory.IsPreBrownianReal.isBrownianReal_mk {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} (h : IsPreBrownianReal X P) : IsBrownianReal (IsPreBrownianReal.mk X h) P

theorem ProbabilityTheory.IsBrownianReal.mk_ae_forall_eq {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} (h : IsBrownianReal X P) : ∀ᵐ (ω : Ω) ∂P, ∀ (t : NNReal), IsPreBrownianReal.mk X ⋯ t ω = X t ω

theorem ProbabilityTheory.IsBrownianReal.aemeasurable {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} (h : IsBrownianReal X P) : AEMeasurable (fun (ω : Ω) (t : NNReal) => X t ω) P

theorem ProbabilityTheory.IsBrownianReal.inv {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} (h : IsBrownianReal X P) : IsBrownianReal (fun (t : NNReal) (ω : Ω) => ↑t * X (1 / t) ω) P

If X is a Brownian motion then so is fun t ω ↦ t * (B (1 / t) ω).

theorem ProbabilityTheory.IsBrownianReal.tendsto_div_id_atTop {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} (h : IsBrownianReal X P) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (t : NNReal) => X t ω / ↑t) Filter.atTop (nhds 0)

theorem ProbabilityTheory.IsBrownianReal.indep_zero {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} (h : IsBrownianReal X P) (hX : ∀ (t : NNReal), Measurable (X t)) (hX' : ∀ (ω : Ω), Continuous fun (x : NNReal) => X x ω) {A : Set Ω} (hA : MeasurableSet A) : P A = 0 ∨ P A = 1

Blumenthal's zero-one law: Let 𝓕 be the canonical filtration associated to a Brownian motion. Then the σ-algebra ⨅ s > 0, 𝓕 s is trivial.

def ProbabilityTheory.preBrownian : NNReal → (NNReal → ℝ) → ℝ

Equations

• ProbabilityTheory.preBrownian t ω = ω t

theorem ProbabilityTheory.measurable_preBrownian (t : NNReal) : Measurable (preBrownian t)

theorem ProbabilityTheory.hasLaw_preBrownian : HasLaw (fun (ω : NNReal → ℝ) (x : NNReal) => preBrownian x ω) gaussianLimit gaussianLimit

theorem ProbabilityTheory.isPreBrownianReal_preBrownian : IsPreBrownianReal preBrownian gaussianLimit

theorem ProbabilityTheory.isGaussianProcess_preBrownian : IsGaussianProcess preBrownian gaussianLimit

theorem ProbabilityTheory.hasLaw_restrict_preBrownian (I : Finset NNReal) : HasLaw (fun (ω : NNReal → ℝ) => I.restrict fun (x : NNReal) => preBrownian x ω) (gaussianProjectiveFamily I) gaussianLimit

theorem ProbabilityTheory.hasLaw_preBrownian_eval (t : NNReal) : HasLaw (preBrownian t) (gaussianReal 0 t) gaussianLimit

theorem ProbabilityTheory.hasLaw_preBrownian_sub (s t : NNReal) : HasLaw (preBrownian s - preBrownian t) (gaussianReal 0 (nndist s t)) gaussianLimit

theorem ProbabilityTheory.isKolmogorovProcess_preBrownian {n : ℕ} (hn : 0 < n) : IsKolmogorovProcess preBrownian gaussianLimit (2 * ↑n) ↑n ↑(2 * n - 1).doubleFactorial

noncomputable def ProbabilityTheory.brownian : NNReal → (NNReal → ℝ) → ℝ

Equations

• ProbabilityTheory.brownian = ProbabilityTheory.IsPreBrownianReal.mk ProbabilityTheory.preBrownian ProbabilityTheory.isPreBrownianReal_preBrownian

theorem ProbabilityTheory.measurable_brownian (t : NNReal) : Measurable (brownian t)

theorem ProbabilityTheory.brownian_ae_eq_preBrownian (t : NNReal) : brownian t =ᵐ[gaussianLimit] preBrownian t

theorem ProbabilityTheory.memHolder_brownian (ω : NNReal → ℝ) (t β : NNReal) (hβ_pos : 0 < β) (hβ_lt : β < 2⁻¹) : ∃ U ∈ nhds t, ∃ (C : NNReal), HolderOnWith C β (fun (x : NNReal) => brownian x ω) U

theorem ProbabilityTheory.continuous_brownian (ω : NNReal → ℝ) : Continuous fun (x : NNReal) => brownian x ω

theorem ProbabilityTheory.isBrownianReal_brownian : IsBrownianReal brownian gaussianLimit

theorem ProbabilityTheory.isGaussianProcess_brownian : IsGaussianProcess brownian gaussianLimit

theorem ProbabilityTheory.hasLaw_restrict_brownian {I : Finset NNReal} : HasLaw (fun (ω : NNReal → ℝ) => I.restrict fun (x : NNReal) => brownian x ω) (gaussianProjectiveFamily I) gaussianLimit

theorem ProbabilityTheory.hasLaw_brownian : HasLaw (fun (ω : NNReal → ℝ) (x : NNReal) => brownian x ω) gaussianLimit gaussianLimit

theorem ProbabilityTheory.hasLaw_brownian_eval {t : NNReal} : HasLaw (brownian t) (gaussianReal 0 t) gaussianLimit

theorem ProbabilityTheory.hasLaw_brownian_sub {s t : NNReal} : HasLaw (brownian s - brownian t) (gaussianReal 0 (nndist s t)) gaussianLimit

theorem ProbabilityTheory.measurable_brownian_uncurry : Measurable (Function.uncurry brownian)

theorem ProbabilityTheory.isKolmogorovProcess_brownian {n : ℕ} (hn : 0 < n) : IsKolmogorovProcess brownian gaussianLimit (2 * ↑n) ↑n ↑(2 * n - 1).doubleFactorial

theorem ProbabilityTheory.covariance_brownian (s t : NNReal) : covariance (brownian s) (brownian t) gaussianLimit = ↑(min s t)

theorem ProbabilityTheory.hasIndepIncrements_brownian : HasIndepIncrements brownian gaussianLimit

noncomputable def ProbabilityTheory.wienerMeasureAux : MeasureTheory.Measure { f : NNReal → ℝ // Continuous f }

Equations

• ProbabilityTheory.wienerMeasureAux = MeasureTheory.Measure.map (fun (ω : NNReal → ℝ) => ⟨fun (t : NNReal) => ProbabilityTheory.brownian t ω, ⋯⟩) ProbabilityTheory.gaussianLimit

noncomputable def ProbabilityTheory.wienerMeasure : MeasureTheory.Measure C(NNReal, ℝ)

Equations

• ProbabilityTheory.wienerMeasure = MeasureTheory.Measure.map (⇑(MeasurableEquiv.continuousMapToFun NNReal ℝ).symm) ProbabilityTheory.wienerMeasureAux