Actual adaptive backward-kernel KL error propagation
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.AdaptiveKLError.adaptive_center_kl_error · theorem · Teaching coverage
Mathematical statement
Let mu be a probability measure on a finite-dimensional real inner-product Borel space E,b≥0,a>0. Construct Markov kernels T,H:E to E and B:E times E to E times E. Every T(u) is mu tilted by -b*norm(x-u)^2/2, and H(u) is its actual Gaussian smoothing at standard-deviation sqrt(a). Every B(u,y) retains u and draws from T(u) tilted by -norm(x-y)^2/(2a), equivalently from mu tilted at precision b+a^-1 and center (b+a^-1)^-1*(b*u+a^-1*y). For every probability center law nu, B composed with nu compProd H equals nu compProd T. The same T,H,B satisfy for every probability center law nu, every probability input law P on E times E and every Markov kernel L on E times E: s to actual ENNReal KL(L(s),B(s)) is measurable, and actual KL(L composed with P,nu compProd T) is at most KL(P,nu compProd H) plus the nonnegative integral of KL(L(s),B(s)) against P. All KL terms and the integral may be infinite.
Lean statement · adaptive_center_kl_error
Construct ideal random-center kernels and prove measurable actual conditional KL plus an extended-valued output error bound for every actual probability input and Markov approximation.
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 adaptive_center_kl_error {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(μ : Measure E) [IsProbabilityMeasure μ] (b a : ℝ) (hb : 0 ≤ b) (ha : 0 < a) :
∃ (T H : Kernel E E) (B : Kernel (E × E) (E × E)),
IsMarkovKernel T ∧ IsMarkovKernel H ∧ IsMarkovKernel B ∧
(∀ u, T u = μ.tilted (fun x => -(b/2)*‖x-u‖^2)) ∧
(∀ u, H u = GaussianSmoothing.gaussianSmoothing (T u) (Real.sqrt a)) ∧
(∀ u y, B (u,y) = Measure.map (Prod.mk u)
((T u).tilted (fun x => -‖x-y‖^2/(2*a)))) ∧
(∀ u y, B (u,y) = Measure.map (Prod.mk u)
(μ.tilted (fun x => -((b+a⁻¹)/2)*
‖x-(b+a⁻¹)⁻¹ • (b • u+a⁻¹ • y)‖^2))) ∧
(∀ (ν : Measure E), IsProbabilityMeasure ν → B ∘ₘ (ν ⊗ₘ H) = ν ⊗ₘ T) ∧
∀ (ν : Measure E), IsProbabilityMeasure ν →
∀ (P : Measure (E × E)), IsProbabilityMeasure P →
∀ (L : Kernel (E × E) (E × E)), IsMarkovKernel L →
Measurable (fun s => klDiv (L s) (B s)) ∧
klDiv (L ∘ₘ P) (ν ⊗ₘ T) ≤ klDiv P (ν ⊗ₘ H) + ∫⁻ s, klDiv (L s) (B s) ∂PProof roadmap
- 1Construct the same ideal joint target and backward kernel
Use the proved measurable random-center recovery theorem. It supplies actual T,H,B, both normalized backward fibers and recovery for every center law. None of these conclusions is introduced as an extra assumption.
- 2Prove that actual conditional KL is measurable
Kernel Radon-Nikodym derivatives are jointly measurable and agree fiberwise almost everywhere with measure RN derivatives. Express KL on the measurable AC set using the nonnegative klFun integral and set it to infinity on the complement. Kernel integration and measurable case distinction prove the desired measurable function.
- 3Identify the joint RN derivative and conditional entropy integral
When the joint law is absolutely continuous, its fibers are almost everywhere absolutely continuous. The actual compProd-withDensity identity identifies its RN derivative with the kernel RN derivative. Tonelli for the nonnegative klFun gives the integral formula, even if that integral is infinite.
- 4Prove the non-AC and infinite branches
If the joint law is not absolutely continuous, its KL is infinite. If the fiber-KL integral were finite, fiber KL would be finite almost everywhere, hence fiber AC almost everywhere, implying joint AC and a contradiction. Thus the same exact formula holds without an AC or finite-integral premise.
- 5Use the actual joint chain rule and output projection
The chain rule separates input divergence from conditional joint divergence. The proved integral identity gives the latter under P. Projecting to the output can only decrease KL. The integration weight is the actual input P, not the ideal input Q.
- 6Substitute actual ideal recovery
Take Q=nu compProd H and K=B from the single earlier construction. Its actual recovery identifies BQ with nu compProd T. The general bound now gives the claimed error for the supplied actual input and approximate kernel; no algorithmic accuracy is inferred.
Full assumptions and notation
All objects and hypotheses
- Finite-dimensional real inner-product Borel space including dimension zero; arbitrary probability base mu; b≥0,a>0.
- T,H,B are constructed before every center law nu, input P and approximate Markov L; fiber formulas are everywhere.
- P is any actual probability joint input law. Its divergence from the ideal nu compProd H is explicitly charged.
- L is an actual measurable Markov kernel. It need not retain the center; relative conditional KL may then be infinite.
- No AC, finite KL, LLR integrability or separately assumed fiber-KL measurability. General probability-base joint semantics explicitly extend the source setting.
Mathematical proof
1. Construct the same ideal joint target and backward kernel
Use the proved measurable random-center recovery theorem. It supplies actual T,H,B, both normalized backward fibers and recovery for every center law. None of these conclusions is introduced as an extra assumption.
Corresponding Lean step
AdaptiveCenterRGO.adaptive_center_recovery; retain all fibers and hrec.
2. Prove that actual conditional KL is measurable
Kernel Radon-Nikodym derivatives are jointly measurable and agree fiberwise almost everywhere with measure RN derivatives. Express KL on the measurable AC set using the nonnegative klFun integral and set it to infinity on the complement. Kernel integration and measurable case distinction prove the desired measurable function.
Corresponding Lean step
Local measurable_fiber_kl; Kernel.measurable_rnDeriv; measurableSet_absolutelyContinuous; klDiv_eq_lintegral_klFun.
3. Identify the joint RN derivative and conditional entropy integral
When the joint law is absolutely continuous, its fibers are almost everywhere absolutely continuous. The actual compProd-withDensity identity identifies its RN derivative with the kernel RN derivative. Tonelli for the nonnegative klFun gives the integral formula, even if that integral is infinite.
Corresponding Lean step
Local conditional_kl_integral AC branch; kernel_of_compProd; compProd_withDensity; rnDeriv_withDensity; lintegral_compProd.
4. Prove the non-AC and infinite branches
If the joint law is not absolutely continuous, its KL is infinite. If the fiber-KL integral were finite, fiber KL would be finite almost everywhere, hence fiber AC almost everywhere, implying joint AC and a contradiction. Thus the same exact formula holds without an AC or finite-integral premise.
Corresponding Lean step
Local conditional_kl_integral non-AC branch; ae_lt_top; klDiv_ne_top_iff; AbsolutelyContinuous.compProd_right.
5. Use the actual joint chain rule and output projection
The chain rule separates input divergence from conditional joint divergence. The proved integral identity gives the latter under P. Projecting to the output can only decrease KL. The integration weight is the actual input P, not the ideal input Q.
Corresponding Lean step
Local composed_kl_bound; klDiv_compProd_eq_add; conditional_kl_integral; klDiv_map_le; snd_compProd.
6. Substitute actual ideal recovery
Take Q=nu compProd H and K=B from the single earlier construction. Its actual recovery identifies BQ with nu compProd T. The general bound now gives the claimed error for the supplied actual input and approximate kernel; no algorithmic accuracy is inferred.
Corresponding Lean step
composed_kl_bound P (ν ⊗ₘ H) L B; rewrite hrec ν hν.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · adaptive_center_kl_error
Measurable kernel RN, nonnegative KL integrals, both AC branches, joint chain rule, output projection and actual ideal recovery.
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 adaptive_center_kl_error {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(μ : Measure E) [IsProbabilityMeasure μ] (b a : ℝ) (hb : 0 ≤ b) (ha : 0 < a) :
∃ (T H : Kernel E E) (B : Kernel (E × E) (E × E)),
IsMarkovKernel T ∧ IsMarkovKernel H ∧ IsMarkovKernel B ∧
(∀ u, T u = μ.tilted (fun x => -(b/2)*‖x-u‖^2)) ∧
(∀ u, H u = GaussianSmoothing.gaussianSmoothing (T u) (Real.sqrt a)) ∧
(∀ u y, B (u,y) = Measure.map (Prod.mk u)
((T u).tilted (fun x => -‖x-y‖^2/(2*a)))) ∧
(∀ u y, B (u,y) = Measure.map (Prod.mk u)
(μ.tilted (fun x => -((b+a⁻¹)/2)*
‖x-(b+a⁻¹)⁻¹ • (b • u+a⁻¹ • y)‖^2))) ∧
(∀ (ν : Measure E), IsProbabilityMeasure ν → B ∘ₘ (ν ⊗ₘ H) = ν ⊗ₘ T) ∧
∀ (ν : Measure E), IsProbabilityMeasure ν →
∀ (P : Measure (E × E)), IsProbabilityMeasure P →
∀ (L : Kernel (E × E) (E × E)), IsMarkovKernel L →
Measurable (fun s => klDiv (L s) (B s)) ∧
klDiv (L ∘ₘ P) (ν ⊗ₘ T) ≤ klDiv P (ν ⊗ₘ H) + ∫⁻ s, klDiv (L s) (B s) ∂P := by
have measurable_fiber_kl (L K : Kernel (E × E) (E × E)) [IsMarkovKernel L] [IsMarkovKernel K] :
Measurable (fun x => klDiv (L x) (K x)) := by
classical
have hf : Measurable (fun p : (E × E) × (E × E) =>
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 : (E × E)) : 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 (μ : Measure (E × E)) [IsProbabilityMeasure μ]
(L K : Kernel (E × E) (E × E)) [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 (P Q : Measure (E × E)) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
(L K : Kernel (E × E) (E × E)) [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]
obtain ⟨T,H,B,hT,hH,hB,hTf,hHf,hBf,hUpd,hrec⟩ :=
AdaptiveCenterRGO.adaptive_center_recovery μ b a hb ha
let := hT
let := hH
let := hB
refine ⟨T,H,B,hT,hH,hB,hTf,hHf,hBf,hUpd,hrec,?_⟩
intro ν hν P hP L hL
let := hν
let := hP
let := hL
refine ⟨measurable_fiber_kl L B,?_⟩
have h := composed_kl_bound P (ν ⊗ₘ H) L B
rw [hrec ν hν] at h
exact h
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.AdaptiveKLErrorSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Theorem6.5 A1 propagates recursive sampler errors for concrete Euclidean Gibbs targets. | Arbitrary probability base on finite-dimensional inner-product Borel space, fixed b>=0,a>0. | generalization | Expanded joint-kernel entropy calculus does not need density, curvature or moments. |
| The proof applies a chain rule and data processing to approximate backward kernels. | Actual ENNReal KL and measurable fiber KL, with conditional integral formula proved including non-AC and infinite cases. | source-implicit | No conditional entropy formula, AC, finite KL or LLR integrability is assumed. |
| Recursive error is averaged over the approximate forward input. | Bound charges KL(P,nu compProd H) plus integral KL(L(s),B(s)) against actual P. | same | The integration weight is P, not the ideal forward law; divergence direction is actual output relative to ideal target. |
| Ideal RGO recovery supplies the comparison target. | Construct one T,H,B before all nu,P,L with everywhere fibers and full retained-center joint recovery. | source-implicit | Existing proved construction supplies recovery; it is not an extra premise. Arbitrary L need not preserve center and may have infinite conditional KL. |
| The full recursive algorithm requires implementable kernels, quantitative bounds and query costs. | An error inequality for any supplied actual Markov approximation. | API-limitation | No concrete recursive L, history-uniform accuracy, A2 proxy selection, Wp sampler guarantee, terminal or cost result. |
Fixed probability base, precision and variance. The supplied actual approximate Markov kernel need not retain the center or satisfy a finite error bound. Its conditional KL is charged under the actual input law. No concrete recursive program, uniform history accuracy, measurable proxy, Wp sampler guarantee, terminal implementation or expected query cost is proved.
Encoder–denoiser: accepted · domain-mismatch
Detected semantic differences
- domains: General probability base abstracts source Gibbs. — No potential, curvature, density or positive-dimension premise.
- assumptions: Non-AC and infinite-KL cases without finite-error hypotheses. — Both AC branches proved; L need not retain center and P need not have first marginal nu. Terms may be infinite.
- conclusion: Conditional error integrated against actual P; input mismatch separately charged. — Actual P-weighted integral from proved conditional identity, chain rule and output projection.
- quantifiers: One ideal family precedes all nu,P,L and supplies full joint recovery. — Existential witness precedes comparison inputs; no all-parameter/history joint selection.
- scopes: Arbitrary Markov approximation is not a constructed accurate recursive sampler. — No numerical accuracy, concrete recursive kernel, termination or costs inferred.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
Scope and omitted-condition boundaries
- Fixed probability base, precision and variance. The supplied actual approximate Markov kernel need not retain the center or satisfy a finite error bound. Its conditional KL is charged under the actual input law. No concrete recursive program, uniform history accuracy, measurable proxy, Wp sampler guarantee, terminal implementation or expected query cost is proved.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- ProbabilityTheory.Kernel.measurable_rnDeriv
- ProbabilityTheory.Kernel.measurableSet_absolutelyContinuous
- MeasureTheory.Measure.compProd_withDensity
- InformationTheory.klDiv_eq_lintegral_klFun
- InformationTheory.klDiv_compProd_eq_add
- InformationTheory.klDiv_map_le
Mathematical sources
- SPHMC v1 Theorem 6.5 A1 recursive error propagation — Expanded actual joint-kernel entropy calculus used by the backward induction; not a completed recursive sampler.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.