Actual adaptive backward-kernel KL error propagation
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.AdaptiveKLError.adaptive_center_kl_error · theorem · Teaching coverage
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.
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 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) ∂PLean 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.AdaptiveKLErrorScope 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.
Source and reuse
ASTIS 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.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.