AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.AdaptiveCenterRGO

- Construct globally measurable target, Gaussian forward and center-retaining backward kernels before every probability center law, with exact joint recovery. The general probability base explicitly abstracts the source Gibbs setting.

theorem adaptive_center_recovery (μ : Measure E) [IsProbabilityMeasure μ] (b a : ℝ)
    (hb : 0 ≤ b) (ha : 0 < a) :
    ∃ (T H : Kernel E E) (B : Kernel (E × E) (E × E)),
      IsMarkovKernel T ∧ IsMarkovKernel H ∧ IsMarkovKernel B ∧
      (∀ u, T u = μ.tilted (fun x => -(b/2)*‖x-u‖^2)) ∧
      (∀ u, H u = GaussianSmoothing.gaussianSmoothing (T u) (Real.sqrt a)) ∧
      (∀ u y, B (u,y) = Measure.map (Prod.mk u)
        ((T u).tilted (fun x => -‖x-y‖^2/(2*a)))) ∧
      (∀ u y, B (u,y) = Measure.map (Prod.mk u)
        (μ.tilted (fun x => -((b+a⁻¹)/2)*
          ‖x-(b+a⁻¹)⁻¹ • (b • u+a⁻¹ • y)‖^2))) ∧
      ∀ (ν : Measure E), IsProbabilityMeasure ν → B ∘ₘ (ν ⊗ₘ H) = ν ⊗ₘ T := by
  have precisionKernel (μ : Measure E) [IsProbabilityMeasure μ] (q : ℝ) (hq : 0 < q) :
      ∃ T : Kernel E E, IsMarkovKernel T ∧
        ∀ u, T u = μ.tilted (fun x => -(q/2)*‖x-u‖^2) := by
    obtain ⟨T,hT,hfiber,_⟩ := GaussianConditionalKernel.exists_tilted_isCondKernel μ (inv_pos.mpr hq)
    refine ⟨T,hT,?_⟩
    intro u
    rw [hfiber]
    congr 1
    funext x
    field_simp
  
  have targetKernel (μ : Measure E) [IsProbabilityMeasure μ] (b : ℝ) (hb : 0 ≤ b) :
      ∃ T : Kernel E E, IsMarkovKernel T ∧
        ∀ u, T u = μ.tilted (fun x => -(b/2)*‖x-u‖^2) := by
    by_cases hb0 : b = 0
    · subst b
      refine ⟨Kernel.const E μ,inferInstance,?_⟩
      intro u
      simp
    · exact precisionKernel μ b (lt_of_le_of_ne hb (Ne.symm hb0))
  
  have globalKernels (μ : Measure E) [IsProbabilityMeasure μ] (b a : ℝ)
      (hb : 0 ≤ b) (ha : 0 < a) :
      ∃ (T H : Kernel E E) (K : Kernel (E × E) E) (B : Kernel (E × E) (E × E)),
        IsMarkovKernel T ∧ IsMarkovKernel H ∧ IsMarkovKernel K ∧ IsMarkovKernel B ∧
        (∀ u, T u = μ.tilted (fun x => -(b/2)*‖x-u‖^2)) ∧
        (∀ u, H u = GaussianSmoothing.gaussianSmoothing (T u) (Real.sqrt a)) ∧
        (∀ u y, K (u,y) = (T u).tilted (fun x => -‖x-y‖^2/(2*a))) ∧
        (∀ u y, K (u,y) = μ.tilted (fun x => -((b+a⁻¹)/2)*
          ‖x-(b+a⁻¹)⁻¹ • (b • u+a⁻¹ • y)‖^2)) ∧
        ∀ u y, B (u,y) = Measure.map (Prod.mk u) (K (u,y)) := by
    obtain ⟨T,hT,hTf⟩ := targetKernel μ b hb
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/AdaptiveCenterRGO.lean:26published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.