Analysis of LMC via Girsanov's Theorem

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