Brownian motion

Indexing the elements of a finset in order

noncomputable def Finset.ofFin {T : Type u_1} [LinearOrder T] (I : Finset T) (i : Fin I.card) : T

Given a finite set I : Finset T of cardinality n, ofFin : Fin #I → T is the map (t₁, ..., tₙ), where t₁ < ... < tₙ are the elements of I.

Equations

• I.ofFin i = (I.sort fun (x1 x2 : T) => x1 ≤ x2).get (Fin.cast ⋯ i)

theorem Finset.monotone_ofFin {T : Type u_1} [LinearOrder T] (I : Finset T) : Monotone I.ofFin

theorem Finset.ofFin_mem {T : Type u_1} [LinearOrder T] (I : Finset T) (i : Fin I.card) : I.ofFin i ∈ I

noncomputable def Finset.toFin {T : Type u_1} [LinearOrder T] (I : Finset T) (i : ↥I) : Fin I.card

Given a finite set I : Finset T, and t : I, I.toFin t returns the position of t in I.

Equations

• I.toFin i = Fin.ofNat I.card (List.idxOf (↑i) (I.sort fun (x1 x2 : T) => x1 ≤ x2))

@[simp]

theorem Finset.ofFin_toFin {T : Type u_1} [LinearOrder T] (I : Finset T) (i : ↥I) : I.ofFin (I.toFin i) = ↑i

@[simp]

theorem Finset.toFin_ofFin {T : Type u_1} [LinearOrder T] (I : Finset T) (i : Fin I.card) : I.toFin ⟨I.ofFin i, ⋯⟩ = i

noncomputable def Finset.ofFin' {T : Type u_1} [LinearOrder T] (I : Finset T) [Bot T] (i : Fin (I.card + 1)) : T

Given a finite set I : Finset T of cardinality n, ofFin' : Fin (#I + 1) → T is the map (⊥, t₁, ..., tₙ), where t₁ < ... < tₙ are the elements of I.

Equations

• I.ofFin' i = if h : i = 0 then ⊥ else I.ofFin (i.pred h)

@[simp]

theorem Finset.ofFin'_zero {T : Type u_1} [LinearOrder T] (I : Finset T) [Bot T] : I.ofFin' 0 = ⊥

theorem Finset.ofFin'_of_ne_zero {T : Type u_1} [LinearOrder T] (I : Finset T) [Bot T] (i : Fin (I.card + 1)) (hi : i ≠ 0) : I.ofFin' i = I.ofFin (i.pred hi)

@[simp]

theorem Finset.ofFin'_succ {T : Type u_1} [LinearOrder T] (I : Finset T) [Bot T] (i : Fin I.card) : I.ofFin' i.succ = I.ofFin i

theorem Finset.ofFin'_mem {T : Type u_1} [LinearOrder T] (I : Finset T) [Bot T] (i : Fin (I.card + 1)) (hi : i ≠ 0) : I.ofFin' i ∈ I

theorem Finset.monotone_ofFin' {T : Type u_1} [LinearOrder T] (I : Finset T) [OrderBot T] : Monotone I.ofFin'

Independent increments

noncomputable def ProbabilityTheory.incrementsToRestrict {T : Type u_1} {E : Type u_3} [LinearOrder T] (R : Type u_4) [Semiring R] [AddCommMonoid E] [Module R E] [TopologicalSpace E] [ContinuousAdd E] (I : Finset T) : (Fin I.card → E) →L[R] ↥I → E

incrementsToRestrict I is a continuous linear map f such that f (xₜ₁, xₜ₂ - xₜ₁, ..., xₜₙ - xₜₙ₋₁) = (xₜ₁, ..., xₜₙ).

Equations

• ProbabilityTheory.incrementsToRestrict R I = { toFun := fun (x : Fin I.card → E) (i : ↥I) => ∑ j ∈ Finset.Iic (I.toFin i), x j, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem ProbabilityTheory.incrementsToRestrict_increments_ofFin'_ae_eq_restrict {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder T] (R : Type u_4) [OrderBot T] [Semiring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [ContinuousAdd E] {X : T → Ω → E} (h : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0) (I : Finset T) : (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) =ᵐ[P] ⇑(incrementsToRestrict R I) ∘ fun (ω : Ω) (i : Fin I.card) => X (I.ofFin' i.succ) ω - X (I.ofFin' i.castSucc) ω

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

@[implicit_reducible]

instance ProbabilityTheory.instMeasurableSpaceContinuousMap_brownianMotion {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] : MeasurableSpace C(X, Y)

Equations

• ProbabilityTheory.instMeasurableSpaceContinuousMap_brownianMotion = borel C(X, Y)

instance ProbabilityTheory.instBorelSpaceContinuousMap_brownianMotion {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] : BorelSpace C(X, Y)

theorem ProbabilityTheory.isClosed_sUnion_of_finite {X : Type u_6} [TopologicalSpace X] {s : Set (Set X)} (h1 : s.Finite) (h2 : ∀ t ∈ s, IsClosed t) : IsClosed (⋃₀ s)

theorem ProbabilityTheory.ContinuousMap.borel_eq_iSup_comap_eval {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [LocallyCompactSpace X] [RegularSpace Y] [MeasurableSpace Y] [BorelSpace Y] : borel C(X, Y) = ⨆ (a : X), MeasurableSpace.comap (fun (b : C(X, Y)) => b a) (borel Y)

theorem ProbabilityTheory.ContinuousMap.measurableSpace_eq_iSup_comap_eval {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [LocallyCompactSpace X] [RegularSpace Y] [MeasurableSpace Y] [BorelSpace Y] : inferInstance = ⨆ (a : X), MeasurableSpace.comap (fun (b : C(X, Y)) => b a) inferInstance

theorem ProbabilityTheory.ContinuousMap.measurable_iff_eval {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] {α : Type u_6} [MeasurableSpace α] [SecondCountableTopology X] [SecondCountableTopology Y] [LocallyCompactSpace X] [RegularSpace Y] [MeasurableSpace Y] [BorelSpace Y] (g : α → C(X, Y)) : Measurable g ↔ ∀ (x : X), Measurable fun (a : α) => (g a) x

def ProbabilityTheory.MeasurableEquiv.continuousMap : { f : NNReal → ℝ // Continuous f } ≃ᵐ C(NNReal, ℝ)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ProbabilityTheory.wienerMeasure = MeasureTheory.Measure.map (⇑ProbabilityTheory.MeasurableEquiv.continuousMap) ProbabilityTheory.wienerMeasureAux