AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOKLError

- The actual finite RGO output KL is bounded by accumulated observation error under its own state laws plus the terminal residual, including infinite values.

theorem finite_rgo_kl_error (μ : Measure E) [IsProbabilityMeasure μ]
    (a : PS → ℝ) (ha : Measurable a) (ha0 : ∀ s, 0 < a s) (threshold : ℝ≥0) :
    let F : PS × E → PS := 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 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))) ∧
      ∀ (Q L : Kernel PS E), IsMarkovKernel Q → IsMarkovKernel L →
      ∃ (P : Kernel PS PS) (R : ℕ → Kernel PS 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)))) ∧
        let e : PS → ℝ≥0∞ := fun s => if threshold ≤ s.1 then 0 else klDiv (Q s) (H s)
        let t : PS → ℝ≥0∞ := fun s => klDiv (L s) (T s)
        Measurable e ∧ Measurable t ∧
        ∀ n s, klDiv (R n s) (T s) ≤
          (∑ j ∈ Finset.range n, ∫⁻ x, e x ∂(P^j) s) + ∫⁻ x, t x ∂(P^n) s := by
  classical
  have measurable_fiber_kl {A B : Type u} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace.CountableOrCountablyGenerated A B] (L K : Kernel A B) [IsMarkovKernel L] [IsMarkovKernel K] :
      Measurable (fun x => klDiv (L x) (K x)) := by
    classical
    have hf : Measurable (fun p : A × B =>
        ENNReal.ofReal (klFun ((Kernel.rnDeriv L K p.1 p.2).toReal))) := by
      exact ENNReal.measurable_ofReal.comp
        (continuous_klFun.measurable.comp (Kernel.measurable_rnDeriv L K).ennreal_toReal)
    have heq (x : A) : klDiv (L x) (K x) =
        if L x ≪ K x then ∫⁻ y, ENNReal.ofReal (klFun ((Kernel.rnDeriv L K x y).toReal)) ∂K x
        else ∞ := by
      rw [klDiv_eq_lintegral_klFun]
      split_ifs
      · apply lintegral_congr_ae
        filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := L) (η := K) (a := x)] with y hy
        rw [hy]
      · rfl
    simp_rw [heq]
    exact Measurable.ite (Kernel.measurableSet_absolutelyContinuous L K)
      hf.lintegral_kernel_prod_right' measurable_const
  have conditional_kl_integral {A B : Type u} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace.CountableOrCountablyGenerated A B] (μ : Measure A) [IsProbabilityMeasure μ]
      (L K : Kernel A B) [IsMarkovKernel L] [IsMarkovKernel K] :
      klDiv (μ ⊗ₘ L) (μ ⊗ₘ K) = ∫⁻ x, klDiv (L x) (K x) ∂μ := by
-- Source excerpt truncated; follow the exact source link.

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

Excerpt truncated; the exact source link is authoritative.