AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOBackward

- One actual backward kernel with every-point precision update, target recovery and all quadratic-budget KL guarantees for its actual smoothed-input outputs.

theorem rgo_backward_recovery {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsProbabilityMeasure μ] (b a : ℝ) (hb : 0 ≤ b) (ha : 0 < a) (u : E) :
    let ρ := μ.tilted (fun x => -(b/2)*‖x-u‖^2)
    IsProbabilityMeasure ρ ∧ ∃ K : Kernel E E, IsMarkovKernel K ∧
      (∀ y, K y = ρ.tilted (fun x => -‖x-y‖^2/(2*a))) ∧
      (∀ y, K y = μ.tilted (fun x => -((b+a⁻¹)/2)*
        ‖x-(b+a⁻¹)⁻¹ • (b • u+a⁻¹ • y)‖^2)) ∧
      K ∘ₘ GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt a) = ρ ∧
      ∀ (ν : Measure E), IsProbabilityMeasure ν → ∀ r : ℝ, 0 ≤ r →
        Transport.transportCost (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^2)) ν ρ ≤
          ENNReal.ofReal (r^2) →
        InformationTheory.klDiv (K ∘ₘ GaussianSmoothing.gaussianSmoothing ν (Real.sqrt a)) ρ ≤
          ENNReal.ofReal (r^2/(2*a)) := by
  have backward_core (μ : Measure E) [IsProbabilityMeasure μ] (a : ℝ) (ha : 0 < a) :
      ∃ K : Kernel E E, IsMarkovKernel K ∧
        (∀ y, K y = μ.tilted (fun x => -‖x-y‖^2/(2*a))) ∧
        K ∘ₘ GaussianSmoothing.gaussianSmoothing μ (Real.sqrt a) = μ := by
    obtain ⟨K, hK, hfiber, hcond⟩ := GaussianConditionalKernel.exists_tilted_isCondKernel μ ha
    let := hK
    let J := Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt a • p.2))
      (μ.prod (stdGaussian E))
    have hfst : J.fst = μ := by
      dsimp [J]
      rw [Measure.fst_map_prodMk (by fun_prop)]
      exact Measure.fst_prod
    have hsnd : J.snd = GaussianSmoothing.gaussianSmoothing μ (Real.sqrt a) := by
      dsimp [J]
      rw [Measure.snd_map_prodMk measurable_fst]
      unfold GaussianSmoothing.gaussianSmoothing CommonNoiseContraction.addNoise
        GaussianSmoothing.scaledStdGaussian
      have hp := Measure.map_prod_map μ (stdGaussian E) measurable_id
        (show Measurable (fun z : E => Real.sqrt a • z) by fun_prop)
      rw [Measure.map_id] at hp
      rw [hp, Measure.map_map (by fun_prop) (by fun_prop)]
      rfl
    have : IsProbabilityMeasure J := Measure.isProbabilityMeasure_map (by fun_prop)
    have hd : (J.map Prod.swap).fst ⊗ₘ K = J.map Prod.swap := hcond.disintegrate
    have heq := congrArg Measure.snd hd
    rw [Measure.snd_compProd, Measure.fst_map_swap, Measure.snd_map_swap, hfst, hsnd] at heq
    exact ⟨K, hK, hfiber, heq⟩
  dsimp only
  let ρ := μ.tilted (fun x => -(b/2)*‖x-u‖^2)
  have hi : Integrable (fun x => Real.exp (-(b/2)*‖x-u‖^2)) μ := by
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/RGOBackward.lean:29published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.