Uniform-grid error quantities for vector Itô formula
DefinitionKLSModular_LevyStochCalc_Brownian_VectorItoFormulaVendored from the LevyStochCalc library at https://github.com/cgarryZA/LevyStochCalc, commit 984dbf0b790031eac05d56fe5a84b65e15e1e932. vectorItoGridResidue nR dR C T is the explicit residual expression proportional to the second-derivative oscillation scale, while vectorItoGridError nR dR B C T A K K₂ x is the explicit real-valued error bound as a function of mesh parameter , with terms for Taylor, drift, martingale, and quadratic-variation contributions. The definitions contain no assertion that these quantities converge or bound an error; those are separate declarations in the source module.
Original module imports
import LevyStochCalc.Brownian.VectorItoFormulaDecomp
import LevyStochCalc.Brownian.VectorItoQuadVarRiemann
import LevyStochCalc.Brownian.VectorItoMartingaleRiemann
import LevyStochCalc.Brownian.ItoFormulaScalar
Original declaration excerpt
Shown in the original module context.
noncomputable def vectorItoGridResidue (nR dR C T : ℝ) : ℝ :=
nR * (2 * (dR ^ 2 * (C ^ 2 * T))) + 1 / 2 * (nR ^ 2 * (dR * C ^ 2 * T))
Module navigation
Direct project imports: LevyStochCalc/Brownian/VectorItoFormulaDecomp, LevyStochCalc/Brownian/VectorItoQuadVarRiemann, LevyStochCalc/Brownian/VectorItoMartingaleRiemann, LevyStochCalc/Brownian/ItoFormulaScalar.
Theorems in source order:
Project result: The KLS conjecture.
Original module · LevyStochCalc.Brownian.VectorItoFormula · Frozen source 408915f.
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_VectorItoFormulaDecomp
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_VectorItoQuadVarRiemann
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_VectorItoMartingaleRiemann
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoFormulaScalar
/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/VectorItoFormula.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
namespace LevyStochCalc
namespace Brownian
namespace Ito
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal Topology
universe u
/-- The residue of the uniform-grid error that the oscillation scale `A` of the second derivative
leaves behind as the mesh vanishes, per unit of `A`. -/
noncomputable def vectorItoGridResidue (nR dR C T : ℝ) : ℝ :=
nR * (2 * (dR ^ 2 * (C ^ 2 * T))) + 1 / 2 * (nR ^ 2 * (dR * C ^ 2 * T))
/-- The `L¹` error of the uniform-grid approximation in Itô's formula for a vector Itô process,
as a function of the mesh. The four summands are the Taylor remainder, the drift Riemann sums,
the martingale Riemann sums and the weighted quadratic variations; `A` and `K` are the two
constants of the affine oscillation bound `A + K‖z − w‖` on the second derivative. -/
noncomputable def vectorItoGridError (nR dR B C T A K K₂ : ℝ) (x : ℝ) : ℝ :=
(A * (nR * (2 * (B ^ 2 * (T * x)) + 2 * (dR ^ 2 * (C ^ 2 * T))))
+ K * (nR ^ 2 * (nR * (4 * (B ^ 3 * T * x ^ 2
+ dR ^ 2 * (dR * ((C ^ 2 + (6 + gaussianFourthMoment) * C ^ 4) / 2
* (T * Real.sqrt x))))))))
+ nR * (K₂ * B * (T * (nR * (B * x + dR * (C * Real.sqrt x)))))
+ nR * dR * Real.sqrt (C ^ 2 * (K₂ ^ 2
* (T * (nR * (2 * (B * x) ^ 2 + 2 * (dR ^ 2 * (C ^ 2 * x)))))))
+ 1 / 2 * (nR ^ 2 * (K₂ * B ^ 2 * T * x
+ 2 * (K₂ * B * dR * C * T * Real.sqrt x)
+ dR * Real.sqrt (K₂ ^ 2 * (3 * ((2 * (6 + gaussianFourthMoment) + 2) * (2 * C) ^ 4))
* (T * x))
+ dR ^ 2 * Real.sqrt (K₂ ^ 2 * ((6 + gaussianFourthMoment) * (C ^ 4 + C ^ 4) / 2)
* (T * x))
+ (A * (dR * C ^ 2) * T
+ K * (dR * C ^ 2) * (T * (nR * (B * x + dR * (C * Real.sqrt x)))))))
end Ito
end Brownian
end LevyStochCalc