ASTIS mathematical exposition

Actual finite recursive RGO KL error accumulation

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOKLError.finite_rgo_kl_error · theorem · Teaching coverage

Statement

Let E be a finite-dimensional real inner-product space with its Borel measurable structure, and mu any probability measure. States are s=(b,u,k,h) in NNReal times E times Nat times E^Nat. Let a(s)>0 be measurable and theta a fixed nonnegative precision threshold. Define F(s,y) by b_new=b+1/a(s), u_new=(b*u+y/a(s))/(b+1/a(s)), count k+1 and history with y prepended. There exist Markov kernels T,H, constructed before all actual kernels, with T(s) the normalized tilt of mu by -b*norm(x-u)^2/2 and H(s) its Gaussian smoothing with standard deviation sqrt(a(s)). For every Markov observation kernel Q and terminal kernel L there exist Markov P and R_n: P(s)=dirac s if theta<=b and otherwise the pushforward of Q(s) under F(s,.); R_0=L; R_(n+1)(s)=L(s) if stopped and otherwise the bind of Q(s) with y mapped to R_n(F(s,y)). Define e(s)=0 if stopped and KL(Q(s)||H(s)) otherwise, and t(s)=KL(L(s)||T(s)). Both e and t are measurable. For every n and initial s, KL(R_n(s)||T(s)) is at most the sum over j<n of the integral of e under P^j(s), plus the integral of t under P^n(s).

\[\operatorname{KL}(R_n(s)\Vert T(s))\le\sum_{j=0}^{n-1}\int e(x)\,P^j(s)(dx)+\int t(x)\,P^n(s)(dx).\]

All objects and hypotheses

E is finite-dimensional over the reals with its Borel measurable structure; zero dimension is permitted. mu is a probability measure.
a is measurable and strictly positive at every state. theta is fixed and nonnegative. Initial precision can be zero or already stopped.
Q and L are measurable Markov kernels on the complete precision-center-count-history state. No probability density or moment assumption is added.
T,H are constructed before arbitrary Q,L. F, P and all R_n have their displayed actual program semantics.
No finite KL, absolute continuity, assumed error measurability, common observation-error budget or terminal-error bound is a premise.

Mathematical proof

1. Prove measurable fiber KL, including singular fibers

Use the jointly measurable kernel Radon-Nikodym derivative and the nonnegative KL integrand z log z+1-z. Fiber KL equals its integral where absolute continuity holds and infinity elsewhere. The absolute-continuity set is measurable; kernel integration and a measurable case split establish fiber KL measurability without a finite-divergence premise.

\[s\mapsto\operatorname{KL}(L(s)\Vert K(s))\quad\text{is measurable}.\]

Corresponding Lean step

Local measurable_fiber_kl; Kernel.measurable_rnDeriv, Kernel.measurableSet_absolutelyContinuous, klDiv_eq_lintegral_klFun.

2. Derive the conditional KL identity in extended reals

If the two joint measures with common first marginal are absolutely continuous, identify the joint density with the fiber kernel density and use nonnegative Fubini integration. If they are not, the joint KL is infinite. Were the integral of fiber KL finite, fiber KL would be finite almost everywhere, hence the fiber laws absolutely continuous almost everywhere; this would imply joint absolute continuity, a contradiction.

\[\operatorname{KL}(\nu\otimes L\Vert\nu\otimes K)=\int\operatorname{KL}(L(x)\Vert K(x))\,\nu(dx).\]

Corresponding Lean step

Local conditional_kl_integral; compProd_withDensity, rnDeriv_withDensity, lintegral_compProd and AbsolutelyContinuous.compProd_right.

3. Obtain the one-step output comparison

Apply data processing to the output projection of the two joint laws. Then apply the KL chain rule and the conditional identity. The conditional output error is integrated against the first actual input law, not the ideal law. The calculation involves no subtraction and remains valid when either term is infinite.

\[\operatorname{KL}(L\nu\Vert K\xi)\le\operatorname{KL}(\nu\Vert\xi)+\int\operatorname{KL}(L(x)\Vert K(x))\,\nu(dx).\]

Corresponding Lean step

Local composed_kl_bound; klDiv_map_le, klDiv_compProd_eq_add and conditional_kl_integral.

4. Construct the actual program and derive ideal consistency

Invoke FiniteRGOProgram for the explicit update and threshold. Before choosing Q,L, also instantiate the same construction with Q=H,L=T. Its exact ideal recovery at depth one and its actual recursion show that binding H(s) with T(F(s,y)) equals T(s) on continuing states. This consistency is proved from the parent construction, not included as an assumption.

\[\int T(F(s,y))\,H(s)(dy)=T(s)\qquad(b(s)<\theta).\]

Corresponding Lean step

FiniteRGOProgram.finite_rgo_program; hprog H T, hRIrec 0, hRIideal and hRIzero; main hcons.

5. Establish the recurrence under the actual transition

On a continuing state, apply the one-step output comparison to Q(s), H(s) and the output kernels pulled back through F(s,.). Replace the ideal bind with T(s). Push the conditional error integral through F to express it under actual P(s). On a stopped state P(s) is a point mass and every R_n(s)=L(s), so the same inequality holds with e(s)=0 and the terminal error unchanged.

\[f_{n+1}(s)\le e(s)+\int f_n(x)\,P(s)(dx),\quad f_n(s)=\operatorname{KL}(R_n(s)\Vert T(s)).\]

Corresponding Lean step

Main stopped and continuing branches; Kernel.comap, actual hrec/hstop/hPf, hcons and lintegral_map.

6. Expand the recurrence into actual visited-law errors

Start with f_0=t. Induct on the finite cap, substitute the prior bound under P, and distribute the integral over the finite nonnegative sum. Kernel composition converts the nested j-step integral into the (j+1)-step actual law. Reindexing gives precisely the displayed sum plus the terminal residual. The zero-depth identity uses the point-mass kernel, so no terminal term is lost at n=0.

\[f_n(s)\le\sum_{j<n}(P^j e)(s)+(P^n t)(s).\]

Corresponding Lean step

Local kernel_error_sum; lintegral_mono, lintegral_finsetSum, Kernel.lintegral_comp, pow_succ and Finset.sum_range_succ'.

Lean statement · finite_rgo_kl_error

Actual finite recursive RGO KL is bounded by actual state-law observation errors and the terminal residual.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

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

Exact module and namespace context

Lean proof · finite_rgo_kl_error

Measurable fiber KL, extended-real conditional KL, output projection, derived ideal consistency and finite actual-kernel recurrence expansion.

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
    classical
    by_cases hac : μ ⊗ₘ L ≪ μ ⊗ₘ K
    · have hfiber := hac.kernel_of_compProd
      have hwd : (μ ⊗ₘ K).withDensity (fun p => Kernel.rnDeriv L K p.1 p.2) = μ ⊗ₘ L := by
        rw [← Measure.compProd_withDensity (Kernel.measurable_rnDeriv L K)]
        apply Measure.compProd_congr
        filter_upwards [hfiber] with x hx
        exact Kernel.withDensity_rnDeriv_eq hx
      have hrn : (μ ⊗ₘ L).rnDeriv (μ ⊗ₘ K) =ᵐ[μ ⊗ₘ K]
          (fun p => Kernel.rnDeriv L K p.1 p.2) := by
        rw [← hwd]
        exact Measure.rnDeriv_withDensity _ (Kernel.measurable_rnDeriv L K)
      rw [klDiv_eq_lintegral_klFun_of_ac hac]
      calc
        _ = ∫⁻ p, ENNReal.ofReal (klFun ((Kernel.rnDeriv L K p.1 p.2).toReal)) ∂(μ ⊗ₘ K) := by
          apply lintegral_congr_ae
          filter_upwards [hrn] with p hp
          rw [hp]
        _ = ∫⁻ x, ∫⁻ y, ENNReal.ofReal (klFun ((Kernel.rnDeriv L K x y).toReal)) ∂K x ∂μ := by
          apply Measure.lintegral_compProd
          exact ENNReal.measurable_ofReal.comp
            (continuous_klFun.measurable.comp (Kernel.measurable_rnDeriv L K).ennreal_toReal)
        _ = _ := by
          apply lintegral_congr_ae
          filter_upwards [hfiber] with x hx
          rw [klDiv_eq_lintegral_klFun_of_ac hx]
          apply lintegral_congr_ae
          filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := L) (η := K) (a := x)] with y hy
          rw [hy]
    · rw [klDiv_of_not_ac hac]
      symm
      by_contra hfinite
      have hf := ae_lt_top (measurable_fiber_kl L K) hfinite
      apply hac
      apply Measure.AbsolutelyContinuous.compProd_right
      filter_upwards [hf] with x hx
      exact (klDiv_ne_top_iff.mp hx.ne).1
  have composed_kl_bound {A B : Type u} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace.CountableOrCountablyGenerated A B] (P Q : Measure A) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
      (L K : Kernel A B) [IsMarkovKernel L] [IsMarkovKernel K] :
      klDiv (L ∘ₘ P) (K ∘ₘ Q) ≤ klDiv P Q + ∫⁻ x, klDiv (L x) (K x) ∂P := by
    calc
      klDiv (L ∘ₘ P) (K ∘ₘ Q) = klDiv (P ⊗ₘ L).snd (Q ⊗ₘ K).snd := by
        rw [Measure.snd_compProd, Measure.snd_compProd]
      _ ≤ klDiv (P ⊗ₘ L) (Q ⊗ₘ K) := klDiv_map_le _ _ measurable_snd
      _ = _ := by rw [klDiv_compProd_eq_add, conditional_kl_integral]
  have kernel_error_sum {A : Type u} [MeasurableSpace A] (P : Kernel A A) [IsMarkovKernel P]
      (e t : A → ℝ≥0∞) (he : Measurable e) (ht : Measurable t)
      (f : ℕ → A → ℝ≥0∞) (hzero : ∀ s, f 0 s ≤ t s)
      (hstep : ∀ n s, f (n+1) s ≤ e s + ∫⁻ x, f n x ∂P s) :
      ∀ n s, f n s ≤ (∑ j ∈ Finset.range n, ∫⁻ x, e x ∂(P^j) s) + ∫⁻ x, t x ∂(P^n) s := by
    have hp (n : ℕ) : IsMarkovKernel (P^n) := by
      induction n with
      | zero => change IsMarkovKernel Kernel.id; infer_instance
      | succ n ih =>
        let := ih
        rw [pow_succ]
        change IsMarkovKernel ((P^n) ∘ₖ P)
        infer_instance
    let := hp
    have hi (n : ℕ) : Measurable (fun s => ∫⁻ x, e x ∂(P^n) s) := he.lintegral_kernel
    intro n
    induction n with
    | zero =>
      intro s
      simp only [Finset.range_zero,Finset.sum_empty,zero_add,pow_zero]
      change f 0 s ≤ ∫⁻ x, t x ∂Measure.dirac s
      simpa only [lintegral_dirac' s ht] using hzero s
    | succ n ih =>
      intro s
      calc
        f (n+1) s ≤ e s + ∫⁻ x, f n x ∂P s := hstep n s
        _ ≤ e s + ∫⁻ x, (∑ j ∈ Finset.range n, ∫⁻ y, e y ∂(P^j) x) +
            ∫⁻ y, t y ∂(P^n) x ∂P s := add_le_add le_rfl (lintegral_mono ih)
        _ = _ := by
          rw [lintegral_add_left (Finset.measurable_sum _ (fun j _ => hi j))]
          rw [lintegral_finsetSum _ (fun j _ => hi j)]
          have hei (j : ℕ) : (∫⁻ x, ∫⁻ y, e y ∂(P^j) x ∂P s) = ∫⁻ y, e y ∂(P^(j+1)) s := by
            rw [pow_succ]
            exact (Kernel.lintegral_comp (P^j) P s he).symm
          have hti : (∫⁻ x, ∫⁻ y, t y ∂(P^n) x ∂P s) = ∫⁻ y, t y ∂(P^(n+1)) s := by
            rw [pow_succ]
            exact (Kernel.lintegral_comp (P^n) P s ht).symm
          simp_rw [hei]
          rw [hti,Finset.sum_range_succ']
          simp only [pow_zero]
          rw [show (1 : Kernel A A) s = Measure.dirac s from rfl,lintegral_dirac' s he]
          change e s + ((∑ j ∈ Finset.range n, ∫⁻ x, e x ∂(P^(j+1)) s) + _) =
            ((∑ j ∈ Finset.range n, ∫⁻ x, e x ∂(P^(j+1)) s) + e s) + _
          ac_rfl
  intro F
  have hF : Measurable F := by
    apply Measurable.prodMk
    · exact Measurable.subtype_mk (by fun_prop)
    · apply Measurable.prodMk
      · fun_prop
      · apply Measurable.prodMk
        · fun_prop
        · apply measurable_pi_lambda
          intro n
          cases n <;> fun_prop
  obtain ⟨T,H,hT,hH,hTf,hHf,hprog⟩ :=
    AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOProgram.finite_rgo_program μ a ha ha0 threshold
  let := hT
  let := hH
  obtain ⟨PI,RI,hPI,hRI,hPIf,hRIzero,hRIrec,hRIstop,hRIpath,hRIideal⟩ := hprog H T hH hT
  have hcons (s : PS) (hs : ¬threshold ≤ s.1) :
      (H s).bind (fun y => T (F (s,y))) = T s := by
    have hh := hRIrec 0 s
    rw [hRIideal rfl rfl 1,hRIzero,if_neg hs] at hh
    exact hh.symm
  refine ⟨T,H,hT,hH,hTf,hHf,?_⟩
  intro Q L hQ hL
  let := hQ
  let := hL
  obtain ⟨P,R,hP,hR,hPf,hzero,hrec,hstop,hpath,hideal⟩ := hprog Q L hQ hL
  let := hP
  refine ⟨P,R,hP,hR,hPf,hzero,hrec,?_⟩
  intro e t
  have he : Measurable e := Measurable.ite
    (measurableSet_le measurable_const measurable_fst) measurable_const (measurable_fiber_kl Q H)
  have ht : Measurable t := measurable_fiber_kl L T
  refine ⟨he,ht,?_⟩
  apply kernel_error_sum P e t he ht (fun n s => klDiv (R n s) (T s))
  · intro s
    rw [hzero]
  · intro n s
    let := hR n
    by_cases hs : threshold ≤ s.1
    · rw [hstop (n+1) s hs,show e s = 0 from if_pos hs,hPf,if_pos hs,
        lintegral_dirac' s (measurable_fiber_kl (R n) T),hstop n s hs,zero_add]
    · have hFs : Measurable (fun y : E => F (s,y)) := hF.comp measurable_prodMk_left
      let LR : Kernel E E := (R n).comap (fun y => F (s,y)) hFs
      let KT : Kernel E E := T.comap (fun y => F (s,y)) hFs
      have hLR : IsMarkovKernel LR := by dsimp [LR]; infer_instance
      have hKT : IsMarkovKernel KT := by dsimp [KT]; infer_instance
      let := hLR
      let := hKT
      have hc := composed_kl_bound (Q s) (H s) LR KT
      change klDiv ((Q s).bind (fun y => R n (F (s,y)))) ((H s).bind (fun y => T (F (s,y)))) ≤
        klDiv (Q s) (H s) + ∫⁻ y, klDiv (R n (F (s,y))) (T (F (s,y))) ∂Q s at hc
      rw [hcons s hs] at hc
      rw [hrec,if_neg hs,show e s = klDiv (Q s) (H s) from if_neg hs,hPf,if_neg hs,
        lintegral_map (measurable_fiber_kl (R n) T) hFs]
      exact hc


end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOKLError

Exact module and namespace context

Scope and omitted-condition boundaries

This proves the error-transfer dependency for the actual finite recursive program. Arbitrary supplied Markov Q and L are not identified with the paper smoothed sampler or FORS. No stage accuracy, adequate stopping cap, initialization validity, or expected query-cost bound is asserted. The terminal residual is retained, including on stopped states. All KL values and budgets are extended nonnegative reals. The source A1 Wasserstein accuracy and equation (6.5) still need an actual observation-kernel instantiation.

Source and reuse

ASTIS parents called

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOProgram.finite_rgo_program

Mathlib API called (external library)

ProbabilityTheory.Kernel.measurable_rnDeriv
InformationTheory.klDiv_compProd_eq_add
InformationTheory.klDiv_map_le
MeasureTheory.lintegral_finsetSum
ProbabilityTheory.Kernel.lintegral_comp

Mathematical sources

SPHMC v1 Theorem 6.5 A1 recursive error argument and equation (6.5) — Finite recursive error transfer; numerical stage budgets and concrete sampler guarantees remain separate.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.