3.2 · Book p. 100 · PDF p. 112
Change of Measure in Path Space
Builds change of measure on path space and Girsanov's theorem, including the likelihood-ratio and martingale conditions.
Open this section in the canonical August 9 source ↗Section 3.2
A change in drift can be represented by an exponential likelihood ratio.
Girsanov's theorem compares two path laws with the same diffusion coefficient by exponentiating a stochastic integral of their drift difference. A martingale condition is what promotes the local exponential to a genuine change of probability measure.
Why is this valid?
A full result requires adapted drift differences, a stochastic integral, a martingale criterion, and identification of the changed path law.
Source assumptions
- controlled drift change
Formal assumptions
- finite-dimensional Gaussian cylinder at the compiled layer
- path-space martingale hypotheses still missing
View Lean formalization
ASTIS currently owns finite Gaussian cylinder identities. The path-space theorem remains a separate red boundary.
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Girsanov.finiteGaussianGirsanovCylinderIntegral
theorem finiteGaussianGirsanovCylinderIntegral
{ι : Type*} [Fintype ι] (h : ι → ℝ) {F : EuclideanSpace ℝ ι → ℝ}
(hF : Measurable F) :
∫ z : EuclideanSpace ℝ ι, F z ∂finiteShiftedGaussianPathMeasure h =
∫ z : EuclideanSpace ℝ ι,
finiteGaussianGirsanovWeight h z * F z
∂stdGaussian (EuclideanSpace ℝ ι) := by
simpa [finiteShiftedGaussianPathMeasure, finiteGaussianGirsanovWeight] using
_root_.AutoSamplingTheory.TechnicalLemmas.Gaussian.stdGaussian_shift_integral_map_toLp
(ι := ι) h hF
/-- Measure-level finite-dimensional cylindrical Girsanov density identity. -/Imports
- AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributions.Gaussian
Local dependencies
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
- continuous-time comparison
- LMC and ULMC discretization