AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.VectorBrownianFiltration

- Chewi's arbitrary finite-family independent-increment clause implies Mathlib's consecutive-grid `HasIndepIncrements` predicate.

theorem IsStandardBrownianMotion.hasIndepIncrements
    {B : ℝ≥0 → Omega → E} {mu : Measure Omega}
    (hB : IsStandardBrownianMotion B mu) :
    HasIndepIncrements B mu := by
  intro n t ht
  apply hB.2.1 n
      (fun i : Fin n => t i.castSucc)
      (fun i : Fin n => t i.succ)
  · intro i
    apply ht
    apply Fin.le_iff_val_le_val.mpr
    simp only [Fin.val_castSucc, Fin.val_succ]
    omega
  · intro i j hij
    rcases lt_or_gt_of_ne hij with hijlt | hjilt
    · apply Set.Ioc_disjoint_Ioc_of_le
      apply ht
      apply Fin.le_iff_val_le_val.mpr
      simp only [Fin.val_succ, Fin.val_castSucc]
      have hijval : i.val < j.val := hijlt
      omega
    · apply (Set.Ioc_disjoint_Ioc_of_le ?_).symm
      apply ht
      apply Fin.le_iff_val_le_val.mpr
      simp only [Fin.val_succ, Fin.val_castSucc]
      have hjival : j.val < i.val := hjilt
      omega

/-- Every continuous linear projection of a Chewi-standard vector Brownian
motion has Mathlib independent increments.  All projections still come from
the same vector process. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/VectorBrownianFiltration.lean:35published source at 77184245109a

- Every continuous linear projection of a Chewi-standard vector Brownian motion has Mathlib independent increments. All projections still come from the same vector process.

theorem IsStandardBrownianMotion.projected_hasIndepIncrements
    {B : ℝ≥0 → Omega → E} {mu : Measure Omega}
    (hB : IsStandardBrownianMotion B mu) (ell : StrongDual ℝ E) :
    HasIndepIncrements (fun t omega => ell (B t omega)) mu :=
  hB.hasIndepIncrements.map ell

/-- Source-level Brownian-filtration contract for a vector process.

The process itself is Chewi-standard.  Adaptedness and independence of each
future *vector* increment from the whole past filtration are added explicitly;
these are exactly the filtration hypotheses needed to derive the scalar
coordinate contracts consumed by stochastic integration. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/VectorBrownianFiltration.lean:66published source at 77184245109a

- Source-level Brownian-filtration contract for a vector process. The process itself is Chewi-standard. Adaptedness and independence of each future *vector* increment from the whole past filtration are added explicitly; these are exactly the filtration hypotheses needed to derive the scalar coordinate contracts consumed by stochastic integration.

structure IsStandardBrownianMotionWithFiltration
    {Omega E : Type*} [MeasurableSpace Omega]
    [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [MeasurableSpace E] [BorelSpace E]
    (B : ℝ≥0 → Omega → E) (filtration : Filtration ℝ≥0 (inferInstance : MeasurableSpace Omega))
    (mu : Measure Omega) : Prop where
  isStandard : IsStandardBrownianMotion B mu
  stronglyAdapted : StronglyAdapted filtration B
  incrementIndependent : ∀ s t, s ≤ t →
    Indep (filtration s)
      (MeasurableSpace.comap (fun omega => B t omega - B s omega) (borel E)) mu

end BrownianMotion
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/VectorBrownianFiltration.lean:78published source at 77184245109a