Brownian motion in ℝᵈ as independent real coordinates

Category: 1-Mathlib (CSD-free; staged for upstream).

The Brownian motion of the Mathlib pin is real-valued (IsPreBrownianReal, IsBrownianReal). A d-dimensional one is d jointly independent real ones, and this module packages exactly what the Euclidean path-integral chain (HeatSemigroup.lean, TimeSlicedWiener.lean, FeynmanKac.lean) needs of it, on EuclideanSpace ℝ ι:

• IsPreBrownianVec B P — the coordinates B t ω i are pre-Brownian and the coordinate paths are jointly independent (iIndepFun); IsBrownianVec adds almost surely continuous paths;
• ★ indepFun_pi_of_iIndepFun — independent vectors of independent pairs: if F i are jointly independent and, for each i, x i (F i) and y i (F i) are independent, then the vectors (x i (F i))ᵢ and (y i (F i))ᵢ are independent. The joint law of the pairs is a product of products, and Mathlib's measurePreserving_arrowProdEquivProdArrow regroups it as a product of two product measures;
• IsPreBrownianVec.hasLaw_eval — B t has the product Gaussian law (Measure.pi fun _ ↦ gaussianReal 0 t).map (toLp 2);
• IsPreBrownianVec.shift and ★ IsPreBrownianVec.indepFun_shift — the weak Markov property: the process shifted by t₀ is pre-Brownian and independent of B t₀, from the coordinate statements and indepFun_pi_of_iIndepFun.

Everything is conditional: no d-dimensional (or one-dimensional) Brownian motion is constructed, as in FeynmanKac.lean.

References: Mathlib/Probability/BrownianMotion/Basic.lean; specs/BACKLOG.md #41; specs/feynman-continuum-scoping.md §8 D1.

Products of absolutely continuous measures

theorem MeasureTheory.Measure.pi_absolutelyContinuous_pi_fin (n : ℕ) {X : Fin n → Type u} [(i : Fin n) → MeasurableSpace (X i)] (μ ν : (i : Fin n) → Measure (X i)) [∀ (i : Fin n), SigmaFinite (μ i)] [∀ (i : Fin n), SigmaFinite (ν i)] : (∀ (i : Fin n), (μ i).AbsolutelyContinuous (ν i)) → (Measure.pi μ).AbsolutelyContinuous (Measure.pi ν)

theorem MeasureTheory.Measure.pi_absolutelyContinuous_pi {ι : Type u_1} [Fintype ι] {X : ι → Type u} [(i : ι) → MeasurableSpace (X i)] {μ ν : (i : ι) → Measure (X i)} [∀ (i : ι), SigmaFinite (μ i)] [∀ (i : ι), SigmaFinite (ν i)] (h : ∀ (i : ι), (μ i).AbsolutelyContinuous (ν i)) : (Measure.pi μ).AbsolutelyContinuous (Measure.pi ν)

A product of absolutely continuous measures is absolutely continuous.

Independent vectors of independent pairs

theorem ProbabilityTheory.indepFun_pi_of_iIndepFun {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Fintype ι] [MeasureTheory.IsProbabilityMeasure P] {α : ι → Type u_3} [(i : ι) → MeasurableSpace (α i)] {β : Type u_4} {γ : Type u_5} [MeasurableSpace β] [MeasurableSpace γ] {F : (i : ι) → Ω → α i} (hF : iIndepFun F P) (hFm : ∀ (i : ι), Measurable (F i)) {x : (i : ι) → α i → β} {y : (i : ι) → α i → γ} (hx : ∀ (i : ι), Measurable (x i)) (hy : ∀ (i : ι), Measurable (y i)) (hxy : ∀ (i : ι), IndepFun (fun (ω : Ω) => x i (F i ω)) (fun (ω : Ω) => y i (F i ω)) P) : IndepFun (fun (ω : Ω) (i : ι) => x i (F i ω)) (fun (ω : Ω) (i : ι) => y i (F i ω)) P

★ Independent vectors of independent pairs. If F i are jointly independent and, for each i, x i (F i) and y i (F i) are independent, then the vectors (x i (F i))ᵢ and (y i (F i))ᵢ are independent.

Brownian motion in ℝᵈ

structure ProbabilityTheory.IsPreBrownianVec {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} (B : NNReal → Ω → EuclideanSpace ℝ ι) (P : MeasureTheory.Measure Ω) : Prop

A pre-Brownian motion in ℝᵈ: the coordinate processes are real pre-Brownian motions and the coordinate paths are jointly independent.

• coord (i : ι) : IsPreBrownianReal (fun (t : NNReal) (ω : Ω) => (B t ω).ofLp i) P
• iIndep : iIndepFun (fun (i : ι) (ω : Ω) (t : NNReal) => (B t ω).ofLp i) P

structure ProbabilityTheory.IsBrownianVec {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} (B : NNReal → Ω → EuclideanSpace ℝ ι) (P : MeasureTheory.Measure Ω) extends ProbabilityTheory.IsPreBrownianVec B P : Prop

A Brownian motion in ℝᵈ: pre-Brownian with almost surely continuous paths.

• coord (i : ι) : IsPreBrownianReal (fun (t : NNReal) (ω : Ω) => (B t ω).ofLp i) P
• iIndep : iIndepFun (fun (i : ι) (ω : Ω) (t : NNReal) => (B t ω).ofLp i) P
• cont : ∀ᵐ (ω : Ω) ∂P, Continuous fun (t : NNReal) => B t ω

noncomputable def ProbabilityTheory.gaussianVec (ι : Type u_3) [Fintype ι] (v : NNReal) : MeasureTheory.Measure (EuclideanSpace ℝ ι)

The product Gaussian on EuclideanSpace ℝ ι with variance v in every coordinate.

Equations

• ProbabilityTheory.gaussianVec ι v = MeasureTheory.Measure.map (WithLp.toLp 2) (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 v)

instance ProbabilityTheory.instIsProbabilityMeasureEuclideanSpaceRealGaussianVec {ι : Type u_2} [Fintype ι] (v : NNReal) : MeasureTheory.IsProbabilityMeasure (gaussianVec ι v)

theorem ProbabilityTheory.charFun_gaussianVec {ι : Type u_2} [Fintype ι] (v : NNReal) (ξ : EuclideanSpace ℝ ι) : MeasureTheory.charFun (gaussianVec ι v) ξ = Complex.exp (-↑↑v * ↑‖ξ‖ ^ 2 / 2)

The characteristic function of the product Gaussian: e^{−v‖ξ‖²/2}.

theorem ProbabilityTheory.gaussianVec_absolutelyContinuous {ι : Type u_2} [Fintype ι] {v : NNReal} (hv : v ≠ 0) : (gaussianVec ι v).AbsolutelyContinuous MeasureTheory.volume

The product Gaussian of positive variance is absolutely continuous with respect to Lebesgue measure.

theorem ProbabilityTheory.measurable_coord {ι : Type u_2} (i : ι) : Measurable fun (x : EuclideanSpace ℝ ι) => x.ofLp i

theorem ProbabilityTheory.IsPreBrownianVec.eval_zero_ae_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Fintype ι] {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : IsPreBrownianVec B P) : ∀ᵐ (ω : Ω) ∂P, B 0 ω = 0

Almost surely B 0 = 0.

theorem ProbabilityTheory.IsPreBrownianVec.hasLaw_eval {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Fintype ι] {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : IsPreBrownianVec B P) (hBm : ∀ (t : NNReal), Measurable (B t)) (t : NNReal) : HasLaw (B t) (gaussianVec ι t) P

B t has the product Gaussian law.

theorem ProbabilityTheory.IsPreBrownianVec.shift {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {ι : Type u_2} {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : IsPreBrownianVec B P) (t₀ : NNReal) : IsPreBrownianVec (fun (t : NNReal) (ω : Ω) => B (t₀ + t) ω - B t₀ ω) P

The process shifted by t₀ is pre-Brownian.

theorem ProbabilityTheory.IsPreBrownianVec.indepFun_shift {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Fintype ι] {B : NNReal → Ω → EuclideanSpace ℝ ι} (hB : IsPreBrownianVec B P) [MeasureTheory.IsProbabilityMeasure P] (hBm : ∀ (t : NNReal), Measurable (B t)) (t₀ : NNReal) : IndepFun (B t₀) (fun (ω : Ω) (t : NNReal) => B (t₀ + t) ω - B t₀ ω) P

★ The weak Markov property: the process shifted by t₀ is independent of B t₀.

theorem ProbabilityTheory.IsBrownianVec.of_coord {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Fintype ι] {B : NNReal → Ω → EuclideanSpace ℝ ι} (hcoord : ∀ (i : ι), IsBrownianReal (fun (t : NNReal) (ω : Ω) => (B t ω).ofLp i) P) (hind : iIndepFun (fun (i : ι) (ω : Ω) (t : NNReal) => (B t ω).ofLp i) P) : IsBrownianVec B P

Jointly independent real Brownian coordinates form a Brownian motion in ℝᵈ.