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

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

A process X : T → Ω → E has independent increments if for any n ≥ 1 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 + 1) → T), Monotone t → ProbabilityTheory.iIndepFun (fun (i : Fin n) (ω : Ω) => X (t i.succ) ω - X (t i.castSucc) ω) P

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.HasIndepIncrements.indepFun_sub_sub {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [Preorder T] [MeasurableSpace E] [AddGroup E] {X : T → Ω → E} (h : HasIndepIncrements X P) {r s t : T} (hrs : r ≤ s) (hst : s ≤ t) : IndepFun (X s - X r) (X t - X s) P

theorem ProbabilityTheory.HasIndepIncrements.indepFun_eval_sub {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [Preorder T] [MeasurableSpace E] [AddGroup E] {X : T → Ω → E} (h : HasIndepIncrements X P) {r s t : T} (hrs : r ≤ s) (hst : s ≤ t) (hX : ∀ᵐ (ω : Ω) ∂P, X r ω = 0) : IndepFun (X s) (X t - X s) P

theorem ProbabilityTheory.HasIndepIncrements.isGaussianProcess {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [LinearOrder T] [OrderBot T] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {X : T → Ω → E} (law : ∀ (t : T), HasGaussianLaw (X t) P) (h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0) (incr : HasIndepIncrements X P) : IsGaussianProcess X P

A stochastic process X with independent increments and such that X t is gaussian for all t is a Gaussian process.

class ProbabilityTheory.IsPreBrownian {Ω : Type u_2} {mΩ : MeasurableSpace Ω} (X : NNReal → Ω → ℝ) (P : MeasureTheory.Measure Ω := by volume_tac) : Prop

A stochastic process is called pre-Brownian if its finite-dimensional laws are those of a Brownian motion, see gaussianProjectiveFamily.

• mk' :: (
• hasLaw (I : Finset NNReal) : HasLaw (fun (ω : Ω) => I.restrict fun (x : NNReal) => X x ω) (gaussianProjectiveFamily I) P
• )

theorem ProbabilityTheory.IsPreBrownian.congr {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} {Y : NNReal → Ω → ℝ} [hX : IsPreBrownian X P] (h : ∀ (t : NNReal), X t =ᵐ[P] Y t) : IsPreBrownian Y P

instance ProbabilityTheory.IsPreBrownian.isGaussianProcess {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [IsPreBrownian X P] : IsGaussianProcess X P

theorem ProbabilityTheory.IsPreBrownian.aemeasurable {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [IsPreBrownian X P] (t : NNReal) : AEMeasurable (X t) P

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

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

theorem ProbabilityTheory.IsPreBrownian.hasLaw_eval {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [h : IsPreBrownian X P] (t : NNReal) : HasLaw (X t) (gaussianReal 0 t) P

theorem ProbabilityTheory.IsPreBrownian.hasLaw_sub {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [IsPreBrownian X P] (s t : NNReal) : HasLaw (X s - X t) (gaussianReal 0 (max (s - t) (t - s))) P

theorem ProbabilityTheory.IsPreBrownian.integral_eval {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [h : IsPreBrownian X P] (t : NNReal) : ∫ (x : Ω), X t x ∂P = 0

theorem ProbabilityTheory.IsPreBrownian.covariance_eval {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [h : IsPreBrownian X P] (s t : NNReal) : covariance (X s) (X t) P = ↑(min s t)

theorem ProbabilityTheory.IsPreBrownian.covariance_fun_eval {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [h : IsPreBrownian X P] (s t : NNReal) : covariance (fun (ω : Ω) => X s ω) (fun (ω : Ω) => X t ω) P = ↑(min s t)

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

theorem ProbabilityTheory.IsPreBrownian.exists_continuous_modification {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [h : IsPreBrownian 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 IsPreBrownian.mk.

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

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

Equations

• ProbabilityTheory.IsPreBrownian.mk X = ⋯.choose

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

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

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

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

theorem ProbabilityTheory.IsPreBrownian.hasIndepIncrements {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [h : IsPreBrownian X P] : HasIndepIncrements X P

theorem ProbabilityTheory.IsGaussianProcess.isPreBrownian_of_covariance {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (h1 : IsGaussianProcess X P) (h2 : ∀ (t : NNReal), ∫ (x : Ω), X t x ∂P = 0) (h3 : ∀ (s t : NNReal), s ≤ t → covariance (X s) (X t) P = ↑s) : IsPreBrownian X P

theorem ProbabilityTheory.HasIndepIncrements.isPreBrownian_of_hasLaw {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (law : ∀ (t : NNReal), HasLaw (X t) (gaussianReal 0 t) P) (incr : HasIndepIncrements X P) : IsPreBrownian X P

theorem ProbabilityTheory.IsPreBrownian.smul {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [IsPreBrownian X P] {c : NNReal} (hc : c ≠ 0) : IsPreBrownian (fun (t : NNReal) (ω : Ω) => X (c * t) ω / √↑c) P

theorem ProbabilityTheory.IsPreBrownian.shift {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [h : IsPreBrownian X P] (t₀ : NNReal) : IsPreBrownian (fun (t : NNReal) (ω : Ω) => X (t₀ + t) ω - X t₀ ω) P

Weak Markov property: If X is a pre-Brownian motion, then X (t₀ + t) - X t₀ is a pre-Brownian motion which is independent from (B t, t ≤ t₀). This is the proof that it is pre-Brownian, see IsPreBrownian.indepFun_shift for independence.

theorem ProbabilityTheory.IsPreBrownian.indepFun_shift {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} [h : IsPreBrownian X P] (hX : ∀ (t : NNReal), Measurable (X t)) (t₀ : NNReal) : IndepFun (fun (ω : Ω) (t : NNReal) => X (t₀ + t) ω - X t₀ ω) (fun (ω : Ω) (t : ↑(Set.Iic t₀)) => X (↑t) ω) P

Weak Markov property: If X is a pre-Brownian motion, then X (t₀ + t) - X t₀ is a pre-Brownian motion which is independent from (B t, t ≤ t₀). This is the proof that of independence, see IsPreBrownian.shift for the proof that it is pre-Brownian.

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

class ProbabilityTheory.IsBrownian {Ω : Type u_2} {mΩ : MeasurableSpace Ω} (X : NNReal → Ω → ℝ) (P : MeasureTheory.Measure Ω := by volume_tac) extends ProbabilityTheory.IsPreBrownian X P : Prop

A stochastic process is called Brownian if its finite-dimensional laws are those of a Brownian motion, see IsPreBrownian, and if it has almost-sure continuous paths.

• hasLaw (I : Finset NNReal) : HasLaw (fun (ω : Ω) => I.restrict fun (x : NNReal) => X x ω) (gaussianProjectiveFamily I) P
• cont : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : NNReal) => X x ω

instance ProbabilityTheory.IsPreBrownian.isBrownian_mk {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} [h : IsPreBrownian X P] : IsBrownian (IsPreBrownian.mk X) P

theorem ProbabilityTheory.IsBrownian.smul {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} [h : IsBrownian X P] {c : NNReal} (hc : c ≠ 0) : IsBrownian (fun (t : NNReal) (ω : Ω) => X (c * t) ω / √↑c) P

theorem ProbabilityTheory.IsBrownian.shift {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} [h : IsBrownian X P] (t₀ : NNReal) : IsBrownian (fun (t : NNReal) (ω : Ω) => X (t₀ + t) ω - X t₀ ω) P

theorem ProbabilityTheory.IsBrownian.inv {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} [h : IsBrownian X P] : IsBrownian (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.IsBrownian.tendsto_nhds_zero {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} [h : IsBrownian X P] : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : NNReal) => X x ω) (nhds 0) (nhds 0)

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

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

instance ProbabilityTheory.isPreBrownian_preBrownian : IsPreBrownian preBrownian gaussianLimit

instance 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 (max (s - t) (t - s))) 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.IsPreBrownian.mk ProbabilityTheory.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 ω

instance ProbabilityTheory.IsBrownian_brownian : IsBrownian brownian gaussianLimit

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

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