AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedRGODepth

- With the source variance schedule and fixed initial-state threshold, the actual absorbed RGO program reaches the terminal set by the explicit logarithmic stage bound. Its output law at that initial state is unchanged by any further cap extension.

theorem stopped_rgo_depth (μ : Measure E) [IsProbabilityMeasure μ]
    (η : PS → ℝ) (hηm : Measurable η) (κ c q Δ γ C : ℝ)
    (hκ : 1 ≤ κ) (hc : 0 < c) (hc1 : c < 1/4)
    (hη : ∀ s, 0 < η s ∧ η s ≤ c) (hd : 0 < Module.finrank ℝ E) (hq : 2 ≤ q)
    (hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1/2) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hC : 8 ≤ C)
    (s0 : PS) (Q Lterm : Kernel PS E) [IsMarkovKernel Q] [IsMarkovKernel Lterm] :
    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 L := q+Real.log (K s0.1*Module.finrank ℝ E*q/Δ)
    let B := γ/(Real.sqrt (Module.finrank ℝ E*L)+L)
    let J := Nat.ceil (C*Real.log (Real.exp 1*K s0.1/B))
    ∃ (F : PS × E → PS) (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 P ∧ (∀ n, IsMarkovKernel (R n)) ∧
      (∀ s, P s = if B⁻¹ ≤ (s.1 : ℝ) then Measure.dirac s else
        (Q s).map (fun y => F (s,y))) ∧
      (∀ n, R n = Lterm ∘ₖ (P^n)) ∧
      0 < B ∧ (P^J) s0 {s | B⁻¹ ≤ (s.1 : ℝ)} = 1 ∧
      (∀ m, R (J+m) s0 = R J s0) ∧
      (J : ℝ) ≤ (3*C+(C/2)*Real.log (1/γ))*L := by
  classical
  let statePath (G : PS × E → PS) (s : PS) (ys : ℕ → E) : ℕ → PS :=
    Nat.rec s (fun n x => G (x,ys n))
  have statePath_shift (G : (PS) × E → (PS)) (n : ℕ) (s : (PS)) (ys : ℕ → E) :
      statePath G s ys (n+1) = statePath G (G (s,ys 0)) (fun k => ys (k+1)) n := by
    induction n with
    | zero => rfl
    | succ n ih =>
      change G (statePath G s ys (n+1),ys (n+1)) =
        G (statePath G (G (s,ys 0)) (fun k => ys (k+1)) n,ys (n+1))
      rw [ih]
  have path_endpoint_mass (G : (PS) × E → (PS)) (hG : Measurable G)
      (Q : Kernel (PS) E) [IsMarkovKernel Q] (P : Kernel (PS) (PS)) [IsMarkovKernel P]
      (hP : ∀ s, P s = (Q s).map (fun y => G (s,y)))
      (D : Set (PS)) (hD : MeasurableSet D) (n : ℕ) (s : (PS))
      (hpaths : ∀ ys : ℕ → E, statePath G s ys n ∈ D) [Nonempty E] :
      (P^n) s D = 1 := by
    have hp (k : ℕ) : IsMarkovKernel (P^k) := by
      induction k with
      | zero => change IsMarkovKernel Kernel.id; infer_instance
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/StoppedRGODepth.lean:37published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.