AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOProgram

- Construct finite threshold-absorbed RGO execution, identify its terminal-output marginal with recursive evaluation, and derive ideal recovery for every finite cap.

theorem finite_rgo_program (μ : Measure E) [IsProbabilityMeasure μ]
    (a : ProgramState E → ℝ) (ha : Measurable a) (ha0 : ∀ s, 0 < a s)
    (threshold : ℝ≥0) :
    let F : ProgramState E × E → ProgramState E := fun p =>
      (⟨(p.1.1 : ℝ)+(a p.1)⁻¹, add_nonneg p.1.1.coe_nonneg (le_of_lt (inv_pos.mpr (ha0 p.1)))⟩,
       ((p.1.1 : ℝ)+(a p.1)⁻¹)⁻¹ • ((p.1.1 : ℝ) • p.1.2.1+(a p.1)⁻¹ • p.2),
       p.1.2.2.1+1, fun n => Nat.casesOn n p.2 p.1.2.2.2)
    ∃ (T H : Kernel (ProgramState E) 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))) ∧
      ∀ (Q L : Kernel (ProgramState E) E), IsMarkovKernel Q → IsMarkovKernel L →
      ∃ (P : Kernel (ProgramState E) (ProgramState E)) (R : ℕ → Kernel (ProgramState E) E),
        IsMarkovKernel P ∧ (∀ n, IsMarkovKernel (R n)) ∧
        (∀ 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)))) ∧
        (∀ n s, threshold ≤ s.1 → R n s = L s) ∧
        (∀ n : ℕ,
          let κ : (k : ℕ) → Kernel (Π _ : Iic k, ProgramState E) (ProgramState E) := fun k =>
            P.comap (fun h => h ⟨k, mem_Iic.mpr le_rfl⟩) (by fun_prop)
          L ∘ₖ (((Kernel.partialTraj (X := fun _ => ProgramState E) κ 0 n).map
            (fun h => h ⟨n, mem_Iic.mpr le_rfl⟩)).comap
            (fun (s : ProgramState E) (_ : Iic 0) => s) (by fun_prop)) = R n) ∧
        (Q = H → L = T → ∀ n, R n = T) := by
  classical
  have endpoint_path (C : Kernel (ProgramState E) (ProgramState E)) [IsMarkovKernel C] (n : ℕ) :
      let κ : (k : ℕ) → Kernel (Π _ : Iic k, (ProgramState E)) (ProgramState E) := fun k =>
        C.comap (fun h => h ⟨k, mem_Iic.mpr le_rfl⟩) (by fun_prop)
      ((Kernel.partialTraj (X := fun _ => (ProgramState E)) κ 0 n).map (fun h => h ⟨n, mem_Iic.mpr le_rfl⟩)).comap
        (fun (s : (ProgramState E)) (_ : Iic 0) => s) (by fun_prop) = C ^ n := by
    intro κ
    have hκ : ∀ k, IsMarkovKernel (κ k) := fun k => by dsimp [κ]; infer_instance
    let := hκ
    have hm (n : ℕ) : (Kernel.partialTraj (X := fun _ => (ProgramState E)) κ 0 n).map (fun h => h ⟨n, mem_Iic.mpr le_rfl⟩) =
        (C ^ n) ∘ₖ Kernel.deterministic (fun h : Π _ : Iic 0, (ProgramState E) => h ⟨0, mem_Iic.mpr le_rfl⟩)
          (by fun_prop) := by
      induction n with
      | zero =>
        rw [Kernel.partialTraj_self, Kernel.id_map (by fun_prop), pow_zero]
        exact (Kernel.id_comp _).symm
      | succ n ih =>
        rw [Kernel.partialTraj_succ_eq_comp (Nat.zero_le n), Kernel.map_comp,
          Kernel.map_partialTraj_succ_self]
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/FiniteRGOProgram.lean:40published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.