AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianRGOErrorBudget

- Source-scaled Wasserstein accuracy implies an actual Gaussian observation KL budget and its finite recursive accumulation, with terminal error retained.

theorem gaussian_rgo_error_budget (μ : Measure E) [IsProbabilityMeasure μ]
    (β κ η τ : PS → ℝ) (hβm : Measurable β) (_hκm : Measurable κ)
    (hηm : Measurable η) (hτm : Measurable τ)
    (hβ : ∀ s, 0 < β s) (hκ : ∀ s, 0 < κ s) (hη : ∀ s, 0 ≤ η s) (hτ : ∀ s, 0 < τ s)
    (threshold : ℝ≥0) (J : ℕ) (Δ : ℝ) (_hΔ : 0 ≤ Δ) :
    let a := fun s => (η s+τ s)/β s
    ∃ (T H : Kernel PS E), IsMarkovKernel T ∧ IsMarkovKernel H ∧
      (∀ s, T s = μ.tilted (fun x => -((s.1:ℝ)/2)*‖x-s.2.1‖^2)) ∧
      (∀ s, H s = GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (a s))) ∧
      ∀ (M L : Kernel PS E), IsMarkovKernel M → IsMarkovKernel L →
      (∀ s, ¬threshold ≤ s.1 → WassersteinSpace.wassersteinDistance (M s)
        (GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (η s/β s)))^2 ≤
        ENNReal.ofReal (κ s*(2*τ s*Δ^2/(κ s*((J:ℝ)+1)))/β s)) →
      ∃ (F : PS × E → PS) (Q : Kernel PS E) (P : Kernel PS PS) (R : ℕ → Kernel PS E),
        (∀ s y, ((F (s,y)).1:ℝ) = (s.1:ℝ)+(a s)⁻¹ ∧
          (F (s,y)).2 = (((s.1:ℝ)+(a s)⁻¹)⁻¹ • ((s.1:ℝ) • s.2.1+(a s)⁻¹ • y),
            s.2.2.1+1,fun n => Nat.casesOn n y s.2.2.2)) ∧
        IsMarkovKernel Q ∧ IsMarkovKernel P ∧ (∀ n, IsMarkovKernel (R n)) ∧
        (∀ s, Q s = GaussianSmoothing.gaussianSmoothing (M s) (Real.sqrt (τ s/β s))) ∧
        (∀ s, P s = if threshold ≤ s.1 then Measure.dirac s else (Q s).map (fun y => F (s,y))) ∧
        R 0 = L ∧
        (∀ n s, R (n+1) s = if threshold ≤ s.1 then L s else (Q s).bind (fun y => R n (F (s,y)))) ∧
        (∀ s, ¬threshold ≤ s.1 → klDiv (Q s) (H s) ≤ ENNReal.ofReal (Δ^2/((J:ℝ)+1))) ∧
        ∀ n s, klDiv (R n s) (T s) ≤
          (n:ℝ≥0∞)*ENNReal.ofReal (Δ^2/((J:ℝ)+1)) + ∫⁻ x, klDiv (L x) (T x) ∂(P^n) s := by
  classical
  have gaussian_kernel {S : Type u} [MeasurableSpace S] (M : Kernel S E) [IsMarkovKernel M]
      (v : S → ℝ) (hv : Measurable v) :
      ∃ Q : Kernel S E, IsMarkovKernel Q ∧
        ∀ s, Q s = GaussianSmoothing.gaussianSmoothing (M s) (Real.sqrt (v s)) := by
    let N : Kernel S E :=
      ((Kernel.deterministic (id : S → S) measurable_id) ×ₖ Kernel.const S (stdGaussian E)).map
        (fun p : S × E => Real.sqrt (v p.1) • p.2)
    have hN : IsMarkovKernel N := by
      dsimp only [N]
      exact Kernel.IsMarkovKernel.map _ (by fun_prop)
    let := hN
    have hNf (s : S) : N s = GaussianSmoothing.scaledStdGaussian (E := E) (Real.sqrt (v s)) := by
      dsimp only [N]
      rw [Kernel.map_apply _ (by fun_prop), Kernel.prod_apply, Kernel.deterministic_apply,
        Kernel.const_apply, Measure.dirac_prod, Measure.map_map (by fun_prop) (by fun_prop)]
      rfl
    let Q := (M ×ₖ N).map (fun p : E × E => p.1+p.2)
    have hQ : IsMarkovKernel Q := by
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/GaussianRGOErrorBudget.lean:36published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.