AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TwoNoiseRGO

- Actual two-noise target recovery and added-time KL control, using one Markov kernel chosen before every proposal law and radius.

theorem two_noise_rgo {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsProbabilityMeasure μ] (b η τ : ℝ)
    (hb : 0 ≤ b) (hη : 0 ≤ η) (hτ : 0 < τ) (u : E) :
    let ρ := μ.tilted (fun x => -(b/2)*‖x-u‖^2)
    IsProbabilityMeasure ρ ∧
      GaussianSmoothing.gaussianSmoothing (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η))
        (Real.sqrt τ) = GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt (η+τ)) ∧
      ∃ K : Kernel E E, IsMarkovKernel K ∧
        (∀ y, K y = ρ.tilted (fun x => -‖x-y‖^2/(2*(η+τ)))) ∧
        K ∘ₘ GaussianSmoothing.gaussianSmoothing
          (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η)) (Real.sqrt τ) = ρ ∧
        ∀ (ν : Measure E), IsProbabilityMeasure ν → ∀ r : ℝ, 0 ≤ r →
          WassersteinSpace.wassersteinDistance ν
            (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt η)) ≤ ENNReal.ofReal r →
          InformationTheory.klDiv (K ∘ₘ GaussianSmoothing.gaussianSmoothing ν (Real.sqrt τ)) ρ ≤
            ENNReal.ofReal (r^2/(2*τ)) := by
  have heat_semigroup (μ : Measure E) [IsProbabilityMeasure μ] (η τ : ℝ) (hη : 0 ≤ η) (hτ : 0 ≤ τ) :
      GaussianSmoothing.gaussianSmoothing (GaussianSmoothing.gaussianSmoothing μ (Real.sqrt η))
        (Real.sqrt τ) = GaussianSmoothing.gaussianSmoothing μ (Real.sqrt (η+τ)) := by
    have hc (a : ℝ) (ha : 0 ≤ a) (t : E) :
        charFun (GaussianSmoothing.scaledStdGaussian (E := E) (Real.sqrt a)) t =
          Complex.exp (-(a : ℂ) * (‖t‖ : ℂ)^2 / 2) := by
      unfold GaussianSmoothing.scaledStdGaussian
      rw [charFun_map_smul, charFun_stdGaussian]
      simp only [norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg a),
        Complex.ofReal_mul, mul_pow]
      rw [← Complex.ofReal_pow, Real.sq_sqrt ha]
      congr 1
      ring
    have hs (ν : Measure E) [IsProbabilityMeasure ν] (s : ℝ) :
        IsProbabilityMeasure (GaussianSmoothing.gaussianSmoothing ν s) := by
      unfold GaussianSmoothing.gaussianSmoothing CommonNoiseContraction.addNoise
      exact Measure.isProbabilityMeasure_map (by fun_prop)
    let := hs μ (Real.sqrt η)
    let := hs (GaussianSmoothing.gaussianSmoothing μ (Real.sqrt η)) (Real.sqrt τ)
    let := hs μ (Real.sqrt (η+τ))
    apply Measure.ext_of_charFun
    funext t
    change charFun ((μ ∗ GaussianSmoothing.scaledStdGaussian (Real.sqrt η)) ∗
        GaussianSmoothing.scaledStdGaussian (Real.sqrt τ)) t =
      charFun (μ ∗ GaussianSmoothing.scaledStdGaussian (Real.sqrt (η+τ))) t
    rw [charFun_conv, charFun_conv, charFun_conv, hc η hη, hc τ hτ, hc (η+τ) (add_nonneg hη hτ)]
    rw [mul_assoc, ← Complex.exp_add]
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/TwoNoiseRGO.lean:28published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.