Brownian motion

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.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

instance ProbabilityTheory.isGaussianProcess_preBrownian : IsGaussianProcess preBrownian gaussianLimit

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

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

theorem ProbabilityTheory.exists_brownian : ∃ (Y : NNReal → (NNReal → ℝ) → ℝ), (∀ (t : NNReal), Measurable (Y t)) ∧ (∀ (t : NNReal), Y t =ᵐ[gaussianLimit] preBrownian t) ∧ ∀ (ω : NNReal → ℝ) (t β : NNReal), 0 < β → ↑β < ⨆ (n : ℕ), (↑(n + 2) - 1) / (2 * ↑(n + 2)) → ∃ U ∈ nhds t, ∃ (C : NNReal), HolderOnWith C β (fun (x : NNReal) => Y x ω) U

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

Equations

• ProbabilityTheory.brownian = ProbabilityTheory.exists_brownian.choose

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.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 (max (s - t) (t - s))) gaussianLimit

instance ProbabilityTheory.isGaussianProcess_brownian : IsGaussianProcess brownian 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.iIndepFun_iff_charFun_eq_pi {ι : Type u_1} {Ω : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [(i : ι) → MeasurableSpace (E i)] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : (i : ι) → Ω → E i} [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] (mX : ∀ (i : ι), AEMeasurable (X i) μ) : iIndepFun X μ ↔ ∀ (t : WithLp 2 ((x : ι) → E x)), MeasureTheory.charFun (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 fun (x : ι) => X x ω) μ) t = ∏ i : ι, MeasureTheory.charFun (MeasureTheory.Measure.map (X i) μ) (t i)

theorem ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_eq_zero {ι : Type u_1} {Ω : Type u_2} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : ι → Ω → ℝ} [h1 : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P] (h2 : ∀ (i j : ι), i ≠ j → covariance (X i) (X j) P = 0) : iIndepFun X P

def ProbabilityTheory.HasIndepIncrements {Ω : Type u_1} {T : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [Sub E] [Preorder T] [MeasurableSpace E] (X : T → Ω → E) (P : MeasureTheory.Measure Ω) : Prop

A process X : T → Ω → E has independent increments if for any n ≥ 2 and t₁ ≤ ... ≤ tₙ, the random variables X t₂ - X t₁, ..., X tₙ - X tₙ₋₁ are independent.

Equations

• ProbabilityTheory.HasIndepIncrements X P = ∀ (n : ℕ) (t : Fin (n + 2) → T), Monotone t → ProbabilityTheory.iIndepFun (fun (i : Fin (n + 1)) => X (t i.succ) - X (t i.castSucc)) P

theorem ProbabilityTheory.mem_pair_iff {α : Type u_1} [DecidableEq α] {x y z : α} : x ∈ {y, z} ↔ x = y ∨ x = z

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

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

Equations

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

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

theorem ProbabilityTheory.isClosed_sUnion_of_finite {X : Type u_3} [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_1} {Y : Type u_2} [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_1} {Y : Type u_2} [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_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {α : Type u_3} [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