AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoFormulaAlgebra

- The `j`-th state-space column of a finite diffusion matrix.

noncomputable def diffusionColumn
    {iota kappa : Type*} [Fintype iota]
    (sigma : iota → kappa → ℝ) (j : kappa) : EuclideanSpace ℝ iota :=
  WithLp.toLp 2 (fun i => sigma i j)

/-- First-order deterministic drift contribution in Itô's formula. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:31published source at 7bcd37294df1

- First-order deterministic drift contribution in Itô's formula.

def driftGradientTerm
    {iota : Type*} [Fintype iota]
    (f : EuclideanSpace ℝ iota → ℝ)
    (x b : EuclideanSpace ℝ iota) : ℝ :=
  inner ℝ (gradient f x) b

/-- Brownian-coordinate coefficient of the stochastic first-order term. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:37published source at 7bcd37294df1

- Brownian-coordinate coefficient of the stochastic first-order term.

def diffusionGradientCoefficient
    {iota kappa : Type*} [Fintype iota]
    (f : EuclideanSpace ℝ iota → ℝ)
    (x : EuclideanSpace ℝ iota)
    (sigma : iota → kappa → ℝ) (j : kappa) : ℝ :=
  inner ℝ (gradient f x) (diffusionColumn sigma j)

/-- Second Fréchet derivative evaluated twice in the same direction. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:44published source at 7bcd37294df1

- Second Fréchet derivative evaluated twice in the same direction.

def secondDerivativeQuadraticForm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : E → ℝ) (x v : E) : ℝ :=
  fderiv ℝ (fderiv ℝ f) x v v

/-- The second-order diffusion/Hessian contraction in column form.

For a `d x N` coefficient matrix this is
`sum_j D^2 f(x)[sigma_j, sigma_j]`, hence the finite-dimensional form of
`<nabla^2 f(x), sigma sigma^T>`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:52published source at 7bcd37294df1

- The second-order diffusion/Hessian contraction in column form. For a `d x N` coefficient matrix this is `sum_j D^2 f(x)[sigma_j, sigma_j]`, hence the finite-dimensional form of `<nabla^2 f(x), sigma sigma^T>`.

def diffusionHessianContraction
    {iota kappa : Type*} [Fintype iota] [Fintype kappa]
    (f : EuclideanSpace ℝ iota → ℝ)
    (x : EuclideanSpace ℝ iota)
    (sigma : iota → kappa → ℝ) : ℝ :=
  ∑ j, secondDerivativeQuadraticForm f x (diffusionColumn sigma j)

/-- The deterministic finite-variation coefficient in the source Itô formula. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:62published source at 7bcd37294df1

- The deterministic finite-variation coefficient in the source Itô formula.

def itoDriftCorrection
    {iota kappa : Type*} [Fintype iota] [Fintype kappa]
    (f : EuclideanSpace ℝ iota → ℝ)
    (x b : EuclideanSpace ℝ iota)
    (sigma : iota → kappa → ℝ) : ℝ :=
  driftGradientTerm f x b +
    (1 / 2 : ℝ) * diffusionHessianContraction f x sigma

/-- The drift-gradient contraction is the Fréchet derivative applied to the
drift whenever `f` is differentiable at the point. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:70published source at 7bcd37294df1

- The drift-gradient contraction is the Fréchet derivative applied to the drift whenever `f` is differentiable at the point.

theorem driftGradientTerm_eq_fderiv
    {iota : Type*} [Fintype iota]
    {f : EuclideanSpace ℝ iota → ℝ}
    {x b : EuclideanSpace ℝ iota}
    (hf : DifferentiableAt ℝ f x) :
    driftGradientTerm f x b = fderiv ℝ f x b := by
  exact
    (Analysis.Calculus.Gradient.fderiv_apply_eq_inner_gradient_of_differentiableAt
      hf).symm

/-- Each stochastic first-order coefficient is the Fréchet derivative in the
corresponding diffusion-column direction. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:80published source at 7bcd37294df1

- Each stochastic first-order coefficient is the Fréchet derivative in the corresponding diffusion-column direction.

theorem diffusionGradientCoefficient_eq_fderiv
    {iota kappa : Type*} [Fintype iota]
    {f : EuclideanSpace ℝ iota → ℝ}
    {x : EuclideanSpace ℝ iota}
    {sigma : iota → kappa → ℝ} {j : kappa}
    (hf : DifferentiableAt ℝ f x) :
    diffusionGradientCoefficient f x sigma j =
      fderiv ℝ f x (diffusionColumn sigma j) := by
  exact
    (Analysis.Calculus.Gradient.fderiv_apply_eq_inner_gradient_of_differentiableAt
      hf).symm

/-- Coordinate expansion of the first-order drift contraction. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:92published source at 7bcd37294df1

- Coordinate expansion of the first-order drift contraction.

theorem driftGradientTerm_eq_sum
    {iota : Type*} [Fintype iota]
    (f : EuclideanSpace ℝ iota → ℝ)
    (x b : EuclideanSpace ℝ iota) :
    driftGradientTerm f x b =
      ∑ i, (gradient f x) i * b i := by
  exact
    Geometry.EuclideanSpaceCoordinates.euclideanSpace_inner_eq_sum_mul
      (gradient f x) b

/-- Coordinate expansion of the Brownian-coordinate stochastic coefficient. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:105published source at 7bcd37294df1

- Coordinate expansion of the Brownian-coordinate stochastic coefficient.

theorem diffusionGradientCoefficient_eq_sum
    {iota kappa : Type*} [Fintype iota]
    (f : EuclideanSpace ℝ iota → ℝ)
    (x : EuclideanSpace ℝ iota)
    (sigma : iota → kappa → ℝ) (j : kappa) :
    diffusionGradientCoefficient f x sigma j =
      ∑ i, (gradient f x) i * sigma i j := by
  rw [diffusionGradientCoefficient]
  rw [Geometry.EuclideanSpaceCoordinates.euclideanSpace_inner_eq_sum_mul]
  rfl

/-- If a supplied Hessian representative is the derivative of `fderiv f` at
`x`, the quadratic form uses that representative literally.  This is the local
bridge used later to turn a `C^2` source function into the Hessian contraction
without assuming a bounded Hessian in the final theorem. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:116published source at 7bcd37294df1

- If a supplied Hessian representative is the derivative of `fderiv f` at `x`, the quadratic form uses that representative literally. This is the local bridge used later to turn a `C^2` source function into the Hessian contraction without assuming a bounded Hessian in the final theorem.

theorem secondDerivativeQuadraticForm_eq_of_hasFDerivAt
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {f : E → ℝ} {x v : E}
    {H : E →L[ℝ] (E →L[ℝ] ℝ)}
    (hH : HasFDerivAt (fderiv ℝ f) H x) :
    secondDerivativeQuadraticForm f x v = H v v := by
  unfold secondDerivativeQuadraticForm
  rw [hH.fderiv]

/-- Rewrite the full diffusion/Hessian contraction using a supplied Hessian
representative at the point. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:131published source at 7bcd37294df1

- Rewrite the full diffusion/Hessian contraction using a supplied Hessian representative at the point.

theorem diffusionHessianContraction_eq_of_hasFDerivAt
    {iota kappa : Type*} [Fintype iota] [Fintype kappa]
    {f : EuclideanSpace ℝ iota → ℝ}
    {x : EuclideanSpace ℝ iota}
    {sigma : iota → kappa → ℝ}
    {H : EuclideanSpace ℝ iota →L[ℝ]
      (EuclideanSpace ℝ iota →L[ℝ] ℝ)}
    (hH : HasFDerivAt (fderiv ℝ f) H x) :
    diffusionHessianContraction f x sigma =
      ∑ j, H (diffusionColumn sigma j) (diffusionColumn sigma j) := by
  unfold diffusionHessianContraction
  apply Finset.sum_congr rfl
  intro j _
  exact secondDerivativeQuadraticForm_eq_of_hasFDerivAt hH

end ItoFormulaAlgebra
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean:142published source at 7bcd37294df1