AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedGaussianRGOError

- Align the actual Gaussian error program with the stopped program, retain its terminal-set residual, and derive stopped output accuracy from terminal-only KL.

theorem stopped_gaussian_rgo_error (μ : Measure E) [IsProbabilityMeasure μ]
    (η : PS → ℝ) (hηm : Measurable η) (κ c Δ γ C : ℝ)
    (hκ : 1 ≤ κ) (hc : 0 < c) (hc1 : c < 1/4)
    (hη : ∀ s, 0 < η s ∧ η s ≤ c) (hd : 0 < Module.finrank ℝ E)
    (hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1/2) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hC : 8 ≤ C) (s0 : PS) :
    let K := fun r : ℝ => (1+r)/(κ⁻¹+r)
    let τ := fun r : ℝ => if 2 ≤ K r then K r else c
    let a := fun s : PS => (η s+τ s.1)/(1+s.1)
    let ell := 2+Real.log (K s0.1*Module.finrank ℝ E*2/Δ)
    let B := γ/(Real.sqrt (Module.finrank ℝ E*ell)+ell)
    let J := Nat.ceil (C*Real.log (Real.exp 1*K s0.1/B))
    let D : Set PS := {s | B⁻¹ ≤ (s.1:ℝ)}
    ∃ 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, s ∉ D → WassersteinSpace.wassersteinDistance (M s)
        (GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (η s/(1+s.1))))^2 ≤
        ENNReal.ofReal (K s.1*(2*τ s.1*Δ^2/(K s.1*((J:ℝ)+1)))/(1+s.1))) →
      ∃ (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.1/(1+s.1)))) ∧
        (∀ s, P s = if s ∈ D then Measure.dirac s else (Q s).map (fun y => F (s,y))) ∧
        (∀ n, R n = L ∘ₖ (P^n)) ∧
        0 < B ∧ (P^J) s0 D = 1 ∧
        (∀ m, R (J+m) s0 = R J s0) ∧
        klDiv (R J s0) (T s0) ≤ (J:ℝ≥0∞)*ENNReal.ofReal (Δ^2/((J:ℝ)+1)) +
          ∫⁻ x in D, klDiv (L x) (T x) ∂(P^J) s0 ∧
        ((∀ s ∈ D, klDiv (L s) (T s) ≤ ENNReal.ofReal (Δ^2/((J:ℝ)+1))) →
          ∀ m, klDiv (R (J+m) s0) (T s0) ≤ ENNReal.ofReal (Δ^2)) := by
  classical
  have recursive_output_powers (Q L : Kernel (PS) E) [IsMarkovKernel Q] [IsMarkovKernel L]
      (F : (PS) × E → (PS)) (hF : Measurable F) (D : Set (PS)) [DecidablePred (· ∈ D)]
      (P : Kernel (PS) (PS)) (R : ℕ → Kernel (PS) E)
      (hPf : ∀ s, P s = if s ∈ D then Measure.dirac s else (Q s).map (fun y => F (s,y)))
      (hzero : R 0 = L)
      (hrec : ∀ n s, R (n+1) s = if s ∈ D then L s else (Q s).bind (fun y => R n (F (s,y)))) :
      ∀ n, R n = L ∘ₖ (P^n) := by
    have hstop (n : ℕ) (s : (PS)) (hs : s ∈ D) : R n s = L s := by
      cases n with
      | zero => rw [hzero]
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/StoppedGaussianRGOError.lean:38published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.