6.2 · Book p. 178 · PDF p. 190
Analysis of LMC via Girsanov's Theorem
Compares LMC and Langevin path laws by Girsanov's theorem and converts the result to a Rényi terminal bound.
Open this section in the canonical August 9 source ↗Section 6.2
Continuous interpolation and change of measure convert local numerical error into sampling error.
An interpolation agrees with the discrete chain at grid times while freezing part of the drift between updates. Comparing this process with the target diffusion reduces the global law error to an integrated local drift mismatch.
Why is this valid?
Prove adaptedness, moment bounds, integrated drift error, absolute continuity of path laws, and the terminal-time data-processing step independently.
Source assumptions
- smooth drift
- stable step size
Formal assumptions
- moment and path-law hypotheses not yet fully formalized
View Lean formalization
The website exposes the compiled divergence and Girsanov leaves, while the full stochastic interpolation chain remains red.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Girsanov.finiteGaussianGirsanovCylinderMeasure_eq_withDensity
theorem finiteGaussianGirsanovCylinderMeasure_eq_withDensity
{ι : Type*} [Fintype ι] (h : ι → ℝ) :
finiteShiftedGaussianPathMeasure h =
(stdGaussian (EuclideanSpace ℝ ι)).withDensity
(fun z => ENNReal.ofReal (finiteGaussianGirsanovWeight h z)) := by
classical
let μ0 : Measure (ι → ℝ) :=
Measure.pi (fun _ : ι => gaussianReal 0 (1 : NNReal))
let coordDensity : (ι → ℝ) → ℝ≥0∞ :=
fun x => ENNReal.ofReal
(Real.exp ((∑ i, h i * x i) - (∑ i, (h i) ^ 2) / 2))
let e : (ι → ℝ) ≃ᵐ EuclideanSpace ℝ ι :=
MeasurableEquiv.toLp 2 (ι → ℝ)
have hProduct :
Measure.pi (fun i : ι => gaussianReal (h i) (1 : NNReal)) =
μ0.withDensity coordDensity := by
simpa [μ0, coordDensity] using
(_root_.AutoSamplingTheory.TechnicalLemmas.Gaussian.pi_gaussianReal_withDensity_exp_shift h).symm
have hMapDensity :
(μ0.withDensity coordDensity).map e =
(μ0.map e).withDensity (fun z => coordDensity (e.symm z)) :=
AutoSamplingTheory.TechnicalLemmas.Measure.RadonNikodym.measurableEquiv_map_withDensity
e μ0 (by fun_prop)
have hStd : μ0.map e = stdGaussian (EuclideanSpace ℝ ι) := by
simpa [μ0, e, MeasurableEquiv.coe_toLp] using
ProbabilityTheory.map_pi_eq_stdGaussian (ι := ι)
have hDensityEq :
(fun z : EuclideanSpace ℝ ι => coordDensity (e.symm z)) =
fun z => ENNReal.ofReal (finiteGaussianGirsanovWeight h z) := by
funext z
have hInner :
inner ℝ (WithLp.toLp 2 h : EuclideanSpace ℝ ι) z =
∑ i, h i * (WithLp.ofLp z) i := by
simpa using
_root_.AutoSamplingTheory.TechnicalLemmas.Gaussian.inner_toLp_toLp_eq_sum_mul
h (WithLp.ofLp z)
have hNorm :
‖(WithLp.toLp 2 h : EuclideanSpace ℝ ι)‖ ^ 2 =
∑ i, (h i) ^ 2 :=
_root_.AutoSamplingTheory.TechnicalLemmas.Gaussian.norm_sq_toLp_eq_sum_sq h
simp [coordDensity, finiteGaussianGirsanovWeight, e, hInner, hNorm]
calc
finiteShiftedGaussianPathMeasure h
= (μ0.withDensity coordDensity).map e := by
simpa [finiteShiftedGaussianPathMeasure, e, μ0,
MeasurableEquiv.coe_toLp] using congrArg (fun ν => ν.map e) hProduct
_ = (μ0.map e).withDensity (fun z => coordDensity (e.symm z)) := hMapDensity
_ = (stdGaussian (EuclideanSpace ℝ ι)).withDensity
(fun z => ENNReal.ofReal (finiteGaussianGirsanovWeight h z)) := by
rw [hDensityEq, hStd]
/-- The finite-dimensional Girsanov weight has unit mass under the centered
`stdGaussian` cylinder. -/Imports
- AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributions.Gaussian
Local dependencies
Downstream consumers
- LMC complexity
- ULMC complexity