ASTIS mathematical exposition

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.

\[\inf_{\gamma\in\Pi(P,Q)}\int\|x-y\|^2\,d\gamma\le r^2\quad\Longrightarrow\quad\operatorname{KL}(H_\tau P\|H_\tau Q)\le\frac{r^2}{2\tau}.\]

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.

\[\exists\gamma\in\Pi(P,Q):\quad\int\|x-y\|^2d\gamma=\inf_{\rho\in\Pi(P,Q)}\int\|x-y\|^2d\rho\le r^2.\]

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.

\[L(c,z)=\exp\left(\frac{\langle x-y,z-y\rangle}{\tau}-\frac{\|x-y\|^2}{2\tau}\right),\qquad A=L\,B.\]

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.

\[\log L(c,x+\sqrt\tau Z)=\frac{\|x-y\|^2}{2\tau}+\frac{\langle x-y,Z\rangle}{\sqrt\tau}.\]

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.

\[\mathbb E_{\gamma\otimes G}|\langle x-y,Z\rangle|<\infty,\qquad\mathbb E_{\gamma\otimes G}\langle x-y,Z\rangle=0.\]

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.

\[\operatorname{KL}(A\|B)=\frac1{2\tau}\int\|x-y\|^2d\gamma.\]

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.

\[(\operatorname{snd})_\#A=H_\tau P,\qquad(\operatorname{snd})_\#B=H_\tau 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.

\[\operatorname{KL}(H_\tau P\|H_\tau Q)\le\operatorname{KL}(A\|B)\le\frac{r^2}{2\tau}.\]

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*τ))

Exact module and namespace context

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.

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.GaussianKL

Exact module and namespace context

Scope 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

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.