An IsDiffusion process starts at its deterministic vector initial state
ProvedFeynmanKac.diffusion_initial_aebrownian-motiondiffusionfeynman-kacinitial-condition
Any genuine IsDiffusion solution starts at its prescribed vector initial state, almost surely. The proof projects the IsDiffusion witness to its underlying IsVectorItoVersion and invokes the accepted zero-time vector Itô-version theorem. It is reusable for clock-augmented Feynman–Kac diffusions and other Brownian SDEs, and assumes no PDE or Feynman–Kac conclusion.
Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_Existence import Theorems.Thm_LevyStochCalc_Brownian_Ito_version_ae_eq_zero_readable open MeasureTheory open LevyStochCalc.Brownian open LevyStochCalc.Brownian.Multidim open FunctionalInequalities.Probability.Diffusion
Formal statement
theorem FeynmanKac.diffusion_initial_ae
{Ω : Type*} [MeasurableSpace Ω]
{P : Measure Ω} [IsProbabilityMeasure P]
{N d : ℕ} {W : MultidimBrownianMotion P d}
{ℱ : Filtration ℝ ‹MeasurableSpace Ω›}
{hW : ∀ k, IsBrownianFiltration (W.W k) ℱ}
{b : (Fin N → ℝ) → Fin N → ℝ}
{σ : (Fin N → ℝ) → Fin d → Fin N → ℝ}
{x₀ : Fin N → ℝ} {Y : ℝ → Ω → Fin N → ℝ}
(h : IsDiffusion W ℱ hW b σ x₀ Y) :
(fun ω => Y 0 ω) =ᵐ[P] (fun _ => x₀) := by sorrySource
Accepted Prove2Me theorem https://prove2.me/theorems/ee3afebe-ae0f-4c3f-aa5d-fab65a71b613
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.