Documentation

BrownianMotion.Gaussian.BrownianMotion

Brownian motion #

def ProbabilityTheory.preBrownian :

NNReal → (NNReal → ℝ) → ℝ

Equations

ProbabilityTheory.preBrownian t ω = ω t

Instances For

theorem ProbabilityTheory.measurable_preBrownian (t : NNReal) :

Measurable (preBrownian t)

theorem ProbabilityTheory.isGaussianProcess_preBrownian :

IsGaussianProcess preBrownian gaussianLimit

theorem ProbabilityTheory.measurePreserving_preBrownian_eval (t : NNReal) :

MeasureTheory.MeasurePreserving (preBrownian t) gaussianLimit (gaussianReal 0 t)

theorem ProbabilityTheory.map_sub_preBrownian (s t : NNReal) :

MeasureTheory.MeasurePreserving (preBrownian s - preBrownian t) gaussianLimit (gaussianReal 0 (max (s - t) (t - s)))

theorem ProbabilityTheory.isMeasurableKolmogorovProcess_preBrownian (n : ℕ) :

IsMeasurableKolmogorovProcess 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), 0 < β → ↑β < ⨆ (n : ℕ), (↑(n + 2) - 1) / (2 * ↑(n + 2)) → ∀ (ω : NNReal → ℝ), MemHolder β fun (x : NNReal) => Y x ω

noncomputable def ProbabilityTheory.brownian :

NNReal → (NNReal → ℝ) → ℝ

Equations

ProbabilityTheory.brownian = ProbabilityTheory.exists_brownian.choose

Instances For

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} (hβ_pos : 0 < β) (hβ_lt : β < 2⁻¹) (ω : NNReal → ℝ) :

MemHolder β fun (x : NNReal) => brownian x ω

theorem ProbabilityTheory.continuous_brownian (ω : NNReal → ℝ) :

Continuous fun (x : NNReal) => brownian x ω

theorem ProbabilityTheory.measurePreserving_brownian_apply {t : NNReal} :

MeasureTheory.MeasurePreserving (brownian t) gaussianLimit (gaussianReal 0 t)

theorem ProbabilityTheory.measurePreserving_brownian_sub {s t : NNReal} :

MeasureTheory.MeasurePreserving (brownian s - brownian t) gaussianLimit (gaussianReal 0 (max (s - t) (t - s)))

theorem ProbabilityTheory.measurable_brownian_uncurry :

Measurable (Function.uncurry brownian)

theorem ProbabilityTheory.isGaussianProcess_brownian :

IsGaussianProcess brownian gaussianLimit

theorem ProbabilityTheory.isMeasurableKolmogorovProcess_brownian (n : ℕ) :

IsMeasurableKolmogorovProcess brownian gaussianLimit (2 * ↑n) ↑n ↑(2 * n - 1).doubleFactorial

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

Instances For

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

Instances For

noncomputable def ProbabilityTheory.wienerMeasure :

MeasureTheory.Measure C(NNReal , ℝ )

Equations

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

Instances For