Gaussian KL reverse transport from the actual quadratic transport budget
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianKL.gaussian_kl_reverse_transport · theorem · Teaching coverage
Statement
Let P,Q be probability measures on a finite-dimensional real inner-product Borel space E, including dimension zero. Let r>=0 and tau>0. Suppose the actual infimum over couplings gamma of the extended nonnegative integral of ofReal(norm(x-y)^2) is at most ofReal(r^2). Then the actual extended-nonnegative InformationTheory.klDiv of GaussianSmoothing P sqrt(tau) relative to GaussianSmoothing Q sqrt(tau) is at most ofReal(r^2/(2tau)). GaussianSmoothing is the product-noise addition pushforward with centered identity-covariance standard Gaussian, scaled by sqrt(tau). No marginal second moments, optimizer, Gaussian KL formula or target LLR integrability are assumed.
All objects and hypotheses
- Finite-dimensional real inner-product Borel E, including zero dimension; P,Q probability measures.
- r>=0 and tau>0. Zero radius is included; nonnegative radius is retained for its geometric meaning although the algebra uses only r^2.
- The actual extended nonnegative infimum quadratic displacement transportCost(P,Q)<=ofReal(r^2) is the input; no optimizer or supplied coupling premise.
- Source Lemma6.3(i) uses Euclidean marginal P2 membership and W2. The proved raw-cost formulation and finite-dimensional inner-product domain are explicit generalizations; finite displacement cost does not imply marginal moments.
- InformationTheory.klDiv is the actual ENNReal divergence, with absolute continuity and LLR integrability proved before using its real integral formula. No exponential displacement moment is required.
Mathematical proof
1. Attain the genuine quadratic transport cost
Apply the existing optimal-coupling theorem to the continuous nonnegative cost norm(x-y)^2. Its actual optimum equals the infimum in the hypothesis. The finite budget yields integrability of the squared displacement and the real expectation bound; no individual marginal moment is inferred.
Corresponding Lean step
OptimalContinuousCost.exists_optimal_coupling; hfinite, hI and hbudget convert only the finite nonnegative integral.
2. Identify the joint Gaussian likelihood as a measure equality
On the actual product gamma times standard Gaussian, retain c=(x,y) and map the noise to x+sqrt(tau)Z or y+sqrt(tau)Z, defining joint probability laws A,B. Nonnegative integral extensionality and the known fixed-center Gaussian likelihood give A=B.withDensity L. The likelihood is jointly measurable; no fiber a.e. identity is promoted to a pointwise joint identity.
Corresponding Lean step
jointLikelihood expands the product integral and applies translated_gaussian_likelihood for each retained c.
3. Use the likelihood under the correct joint law
The withDensity equality gives A absolutely continuous with respect to B and RN=L B-a.e. Transfer that equality to A-a.e. using absolute continuity. Under A, z=x+sqrt(tau)Z, so the log likelihood has a positive quadratic term and a centered inner-product term.
Corresponding Lean step
hrn then hac.ae_eq yields hlog; llrAlgebra proves the exact A-parameterized identity.
4. Prove absolute integrability before taking expectations
The bound norm(d)<=1+norm(d)^2 gives displacement integrability. Product integrability of the inner product follows from abs(inner(d,Z))<=norm(d)norm(Z) and the Gaussian first moment. Fubini and the continuous linear inner-product functional then give zero expectation, using the actual product measure and Gaussian zero mean.
Corresponding Lean step
crossMoment uses Integrable.op_fst_snd, integral_prod, continuous-linear-map integral interchange and integral_id_stdGaussian.
5. Calculate the actual joint KL divergence
Both terms of the pulled-back LLR are integrable. Transfer integrability through the measurable map and the A-a.e. LLR identity. Apply the actual klDiv formula; the probability mass corrections cancel, leaving the quadratic displacement expectation divided by 2tau.
Corresponding Lean step
jointKL proves Integrable(llr A B) A before klDiv_of_ac_of_integrable; all real integral manipulations are justified.
6. Identify both actual output marginals
Project each retained-parameter joint law to its output coordinate. Composition of pushforwards and the product-map identity show that the marginals are the existing GaussianSmoothing operators applied to the actual coupling marginals P,Q.
Corresponding Lean step
gaussianMarginal uses Measure.map_prod_map and Measure.map_map; hAP,hBQ use hcouple.1 and hcouple.2.
7. Apply KL data processing and the finite budget
Apply the existing actual KL data-processing inequality to the same output projection for A and B. Substitute the exact joint KL and actual marginal identities, then divide the proved budget by positive 2tau and use ENNReal.ofReal monotonicity.
Corresponding Lean step
InformationTheory.klDiv_map_le followed by hj, hAP, hBQ and hbudget. No totalized-toReal shortcut, Renyi limit, or TV-to-cost transfer.
Lean statement · gaussian_kl_reverse_transport
Actual ENNReal KL of Gaussian smoothing is bounded by r^2/(2tau) from the true quadratic transport budget.
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 gaussian_kl_reverse_transport {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(P Q : Measure E) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
(r τ : ℝ) (_hr : 0 ≤ r) (hτ : 0 < τ)
(hcost : Transport.transportCost (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^2)) P Q ≤
ENNReal.ofReal (r^2)) :
InformationTheory.klDiv (GaussianSmoothing.gaussianSmoothing P (Real.sqrt τ))
(GaussianSmoothing.gaussianSmoothing Q (Real.sqrt τ)) ≤ ENNReal.ofReal (r^2/(2*τ))Lean proof · gaussian_kl_reverse_transport
Actual optimal coupling, joint Gaussian likelihood and integrable LLR formula, followed by exact marginal identification and KL data processing.
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 gaussian_kl_reverse_transport {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(P Q : Measure E) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
(r τ : ℝ) (_hr : 0 ≤ r) (hτ : 0 < τ)
(hcost : Transport.transportCost (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^2)) P Q ≤
ENNReal.ofReal (r^2)) :
InformationTheory.klDiv (GaussianSmoothing.gaussianSmoothing P (Real.sqrt τ))
(GaussianSmoothing.gaussianSmoothing Q (Real.sqrt τ)) ≤ ENNReal.ofReal (r^2/(2*τ)) := by
have crossMoment (γ : Measure (E × E)) [IsProbabilityMeasure γ]
(h2 : Integrable (fun c : E × E => ‖c.1-c.2‖^2) γ) :
Integrable (fun z : (E × E) × E => inner ℝ (z.1.1-z.1.2) z.2)
(γ.prod (stdGaussian E)) ∧
(∫ z : (E × E) × E, inner ℝ (z.1.1-z.1.2) z.2 ∂γ.prod (stdGaussian E)) = 0 := by
have hd : Integrable (fun c : E × E => c.1-c.2) γ := by
apply Integrable.mono' ((integrable_const (1 : ℝ)).add h2) (by fun_prop)
filter_upwards [] with c
change ‖c.1-c.2‖ ≤ 1 + ‖c.1-c.2‖^2
have hn := norm_nonneg (c.1-c.2)
nlinarith [sq_nonneg (‖c.1-c.2‖-1)]
have hz : Integrable (fun z : E => z) (stdGaussian E) := IsGaussian.integrable_id
have hi : Integrable (fun z : (E × E) × E => inner ℝ (z.1.1-z.1.2) z.2)
(γ.prod (stdGaussian E)) :=
hd.op_fst_snd (by fun_prop) ⟨1, by intro x y; simpa using abs_real_inner_le_norm x y⟩ hz
refine ⟨hi, ?_⟩
rw [integral_prod _ hi]
have hm (c : E × E) : (∫ z : E, inner ℝ (c.1-c.2) z ∂stdGaussian E) = 0 := by
change (∫ z : E, (innerSL ℝ (c.1-c.2)) z ∂stdGaussian E) = 0
rw [(innerSL ℝ (c.1-c.2)).integral_comp_comm hz]
simp [integral_id_stdGaussian]
simp_rw [hm]
simp
have jointLikelihood (γ : Measure (E × E)) [IsProbabilityMeasure γ]
(a b : E × E → E) (ha : Measurable a) (hb : Measurable b)
(τ : ℝ) (hτ : 0 < τ) :
let A := (γ.prod (stdGaussian E)).map (fun w => (w.1,a w.1+Real.sqrt τ • w.2))
let B := (γ.prod (stdGaussian E)).map (fun w => (w.1,b w.1+Real.sqrt τ • w.2))
let L := fun w : (E × E) × E => ENNReal.ofReal (Real.exp
(inner ℝ (a w.1-b w.1) (w.2-b w.1)/τ-‖a w.1-b w.1‖^2/(2*τ)))
Measurable L ∧ A = B.withDensity L := by
dsimp only
let L := fun w : (E × E) × E => ENNReal.ofReal (Real.exp
(inner ℝ (a w.1-b w.1) (w.2-b w.1)/τ-‖a w.1-b w.1‖^2/(2*τ)))
have hL : Measurable L := by unfold L; fun_prop
refine ⟨hL, ?_⟩
apply Measure.ext_of_lintegral
intro f hf
rw [lintegral_map hf (by fun_prop),lintegral_prod _ (by fun_prop),
lintegral_withDensity_eq_lintegral_mul _ hL hf,
lintegral_map (hL.mul hf) (by fun_prop),lintegral_prod _ (by fun_prop)]
apply lintegral_congr
intro c
change (∫⁻ z, f (c,a c+Real.sqrt τ • z) ∂stdGaussian E) =
∫⁻ z, L (c,b c+Real.sqrt τ • z) * f (c,b c+Real.sqrt τ • z) ∂stdGaussian E
have hf' : Measurable (fun z : E => f (c,z)) := hf.comp (measurable_const.prodMk measurable_id)
have hLc : Measurable (fun z : E => L (c,z)) := hL.comp (measurable_const.prodMk measurable_id)
have hlaw := (GaussianLikelihood.translated_gaussian_likelihood (a c) (b c) τ hτ).2.1
dsimp only at hlaw
calc
_ = ∫⁻ z, f (c,z) ∂(stdGaussian E).map (fun z => a c+Real.sqrt τ • z) :=
(lintegral_map hf' (by fun_prop)).symm
_ = ∫⁻ z, L (c,z)*f (c,z) ∂(stdGaussian E).map (fun z => b c+Real.sqrt τ • z) := by
rw [hlaw,lintegral_withDensity_eq_lintegral_mul _ (by fun_prop) hf']
rfl
_ = _ := lintegral_map (show Measurable (fun z => L (c,z)*f (c,z)) from hLc.mul hf') (by fun_prop)
have llrAlgebra (x y z : E) (τ : ℝ) (hτ : 0 < τ) :
inner ℝ (x-y) (x+Real.sqrt τ • z-y)/τ-‖x-y‖^2/(2*τ) =
‖x-y‖^2/(2*τ)+inner ℝ (x-y) z/Real.sqrt τ := by
have hs : Real.sqrt τ ≠ 0 := (Real.sqrt_pos.mpr hτ).ne'
rw [show x+Real.sqrt τ • z-y = (x-y)+Real.sqrt τ • z by abel,
inner_add_right,real_inner_smul_right,real_inner_self_eq_norm_sq]
have ht : τ = (Real.sqrt τ)^2 := (Real.sq_sqrt hτ.le).symm
rw [ht]
rw [Real.sqrt_sq (Real.sqrt_nonneg τ)]
field_simp
ring
have jointKL (γ : Measure (E × E)) [IsProbabilityMeasure γ]
(h2 : Integrable (fun c : E × E => ‖c.1-c.2‖^2) γ)
(τ : ℝ) (hτ : 0 < τ) :
let A := (γ.prod (stdGaussian E)).map (fun w => (w.1,w.1.1+Real.sqrt τ • w.2))
let B := (γ.prod (stdGaussian E)).map (fun w => (w.1,w.1.2+Real.sqrt τ • w.2))
InformationTheory.klDiv A B = ENNReal.ofReal ((∫ c, ‖c.1-c.2‖^2 ∂γ)/(2*τ)) := by
let F := fun w : (E × E) × E => (w.1,w.1.1+Real.sqrt τ • w.2)
let G := fun w : (E × E) × E => (w.1,w.1.2+Real.sqrt τ • w.2)
let A := (γ.prod (stdGaussian E)).map F
let B := (γ.prod (stdGaussian E)).map G
let ℓ := fun w : (E × E) × E => inner ℝ (w.1.1-w.1.2) (w.2-w.1.2)/τ-‖w.1.1-w.1.2‖^2/(2*τ)
let L := fun w => ENNReal.ofReal (Real.exp (ℓ w))
have hF : Measurable F := by unfold F; fun_prop
have hG : Measurable G := by unfold G; fun_prop
have hℓ : Measurable ℓ := by unfold ℓ; fun_prop
have hL : Measurable L := by unfold L; fun_prop
have hA : IsProbabilityMeasure A := Measure.isProbabilityMeasure_map hF.aemeasurable
have hB : IsProbabilityMeasure B := Measure.isProbabilityMeasure_map hG.aemeasurable
let := hA
let := hB
have hab : A = B.withDensity L :=
(jointLikelihood γ Prod.fst Prod.snd measurable_fst measurable_snd τ hτ).2
have hac : A ≪ B := by rw [hab]; exact withDensity_absolutelyContinuous _ _
have hrn : A.rnDeriv B =ᵐ[B] L := by rw [hab]; exact Measure.rnDeriv_withDensity _ hL
have hlog : llr A B =ᵐ[A] ℓ := by
filter_upwards [hac.ae_eq hrn] with w hw
simp only [llr,hw,L,ENNReal.toReal_ofReal (Real.exp_pos _).le,Real.log_exp]
have hpull : (fun w => ℓ (F w)) = fun w : (E × E) × E =>
‖w.1.1-w.1.2‖^2/(2*τ)+inner ℝ (w.1.1-w.1.2) w.2/Real.sqrt τ := by
funext w
exact llrAlgebra w.1.1 w.1.2 w.2 τ hτ
obtain ⟨hc,hcz⟩ := crossMoment γ h2
have hip : Integrable (fun w => ℓ (F w)) (γ.prod (stdGaussian E)) := by
rw [hpull]
exact ((h2.comp_fst (stdGaussian E)).div_const _).add (hc.div_const _)
have hiℓ : Integrable ℓ A := (integrable_map_measure hℓ.aestronglyMeasurable hF.aemeasurable).mpr hip
have hillr : Integrable (llr A B) A := hiℓ.congr hlog.symm
have hfstint : (∫ w : (E × E) × E, ‖w.1.1-w.1.2‖^2 ∂γ.prod (stdGaussian E)) =
∫ c : E × E, ‖c.1-c.2‖^2 ∂γ := by
simpa using (integral_fun_fst (μ := γ) (ν := stdGaussian E) (fun c : E × E => ‖c.1-c.2‖^2))
have hint : (∫ w, ℓ w ∂A) = (∫ c, ‖c.1-c.2‖^2 ∂γ)/(2*τ) := by
rw [show A = (γ.prod (stdGaussian E)).map F from rfl,
integral_map hF.aemeasurable hℓ.aestronglyMeasurable]
change (∫ w, (fun w => ℓ (F w)) w ∂γ.prod (stdGaussian E)) = _
rw [hpull,integral_add ((h2.comp_fst _).div_const _) (hc.div_const _),
integral_div,integral_div,hcz]
rw [hfstint]
simp
change InformationTheory.klDiv A B = _
rw [InformationTheory.klDiv_of_ac_of_integrable hac hillr,integral_congr_ae hlog,hint]
simp
have gaussianMarginal (γ : Measure (E × E)) [IsProbabilityMeasure γ]
(a : E × E → E) (ha : Measurable a) (τ : ℝ) :
((γ.prod (stdGaussian E)).map (fun w => (w.1,a w.1+Real.sqrt τ • w.2))).map Prod.snd =
GaussianSmoothing.gaussianSmoothing (γ.map a) (Real.sqrt τ) := by
have hprob : IsProbabilityMeasure (γ.map a) := Measure.isProbabilityMeasure_map ha.aemeasurable
let := hprob
have smoothing_law (μ : Measure E) [IsProbabilityMeasure μ] :
GaussianSmoothing.gaussianSmoothing μ (Real.sqrt τ) =
(μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt τ • p.2) := by
unfold GaussianSmoothing.gaussianSmoothing CommonNoiseContraction.addNoise
GaussianSmoothing.scaledStdGaussian
have hp := Measure.map_prod_map μ (stdGaussian E) measurable_id
(by fun_prop : Measurable (fun z : E => Real.sqrt τ • z))
simp only [Measure.map_id] at hp
rw [hp,Measure.map_map (by fun_prop) (by fun_prop)]
rfl
rw [smoothing_law,Measure.map_map measurable_snd (by fun_prop)]
have hp := Measure.map_prod_map γ (stdGaussian E) ha measurable_id
simp only [Measure.map_id] at hp
rw [hp,Measure.map_map (by fun_prop) (by fun_prop)]
rfl
have hn (z : E × E) : 0 ≤ ‖z.1-z.2‖^2 := sq_nonneg _
let c : E × E → ℝ≥0 := fun z => ⟨‖z.1-z.2‖^2,hn z⟩
have hf : Continuous (fun z : E × E => ‖z.1-z.2‖^2) := by fun_prop
have hc : Continuous c := hf.subtype_mk _
obtain ⟨γ,hprob,hcouple,hopt⟩ := OptimalContinuousCost.exists_optimal_coupling P Q c hc
let : IsProbabilityMeasure γ := hprob
have heq : (fun z => (c z : ℝ≥0∞)) = (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^2)) := by
funext z
exact (ENNReal.ofReal_eq_coe_nnreal (hn z)).symm
rw [heq] at hopt
have hfinite : (∫⁻ z, ENNReal.ofReal (‖z.1-z.2‖^2) ∂γ) ≠ ∞ :=
ne_of_lt (lt_of_le_of_lt (hopt.le.trans hcost) ENNReal.ofReal_lt_top)
have hnon : 0 ≤ᵐ[γ] (fun z : E × E => ‖z.1-z.2‖^2) := Filter.Eventually.of_forall hn
have hI := (lintegral_ofReal_ne_top_iff_integrable hf.aestronglyMeasurable hnon).mp hfinite
have hbudget : (∫ z, ‖z.1-z.2‖^2 ∂γ) ≤ r^2 := by
rw [integral_eq_lintegral_of_nonneg_ae hnon hf.aestronglyMeasurable]
have hh := ENNReal.toReal_mono ENNReal.ofReal_ne_top (hopt.le.trans hcost)
simpa [ENNReal.toReal_ofReal (sq_nonneg r)] using hh
let A := (γ.prod (stdGaussian E)).map (fun w => (w.1,w.1.1+Real.sqrt τ • w.2))
let B := (γ.prod (stdGaussian E)).map (fun w => (w.1,w.1.2+Real.sqrt τ • w.2))
have hA : IsProbabilityMeasure A := Measure.isProbabilityMeasure_map (by fun_prop)
have hB : IsProbabilityMeasure B := Measure.isProbabilityMeasure_map (by fun_prop)
let := hA
let := hB
have hfst : γ.map Prod.fst = P := hcouple.1
have hsnd : γ.map Prod.snd = Q := hcouple.2
have hAP : A.map Prod.snd = GaussianSmoothing.gaussianSmoothing P (Real.sqrt τ) := by
have hh := gaussianMarginal γ Prod.fst measurable_fst τ
rw [hfst] at hh
exact hh
have hBQ : B.map Prod.snd = GaussianSmoothing.gaussianSmoothing Q (Real.sqrt τ) := by
have hh := gaussianMarginal γ Prod.snd measurable_snd τ
rw [hsnd] at hh
exact hh
have hd := InformationTheory.klDiv_map_le A B measurable_snd
have hj : InformationTheory.klDiv A B = ENNReal.ofReal ((∫ c, ‖c.1-c.2‖^2 ∂γ)/(2*τ)) :=
jointKL γ hI τ hτ
rw [hAP,hBQ,hj] at hd
exact hd.trans (ENNReal.ofReal_le_ofReal (div_le_div_of_nonneg_right hbudget (by positivity)))
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianKLScope and omitted-condition boundaries
- Actual ENNReal KL Gaussian reverse transport from a genuine quadratic transport-cost budget. Explicit generalization of Euclidean marginal-P2/W2 presentation; no marginal moments inferred. Full W2 API identification, recursive kernels, sampler errors and query costs remain separate.
Source and reuse
ASTIS parents called
AutoSamplingTheory.TechnicalLemmas.Measure.OptimalContinuousCost.exists_optimal_couplingAutoSamplingTheory.TechnicalLemmas.Measure.GaussianLikelihood.translated_gaussian_likelihood
Mathlib API called (external library)
- InformationTheory.klDiv_map_le
- InformationTheory.klDiv_of_ac_of_integrable
- MeasureTheory.Integrable.op_fst_snd
- ProbabilityTheory.integral_id_stdGaussian
Mathematical sources
- Chen, Chewi, Lu and Zhang, SPHMC v1 Lemma6.3(i) — Expanded actual-budget Gaussian regularization inequality used by Theorem6.5 A1; not a proof of the full recursive algorithm.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.