Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Gaussian KL reverse transport from the actual quadratic transport budget

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang; ASTIS expanded proof, no author endorsement implied.

arXiv:2609.06906v1 · Lemma6.3(i), actual quadratic-budget Gaussian KL reverse transport · faithful paraphrase

Complete source statement (Samplinglib restatement)

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.

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

Actual Gaussian KL reverse transport

\[\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}.\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Gaussian KL reverse transport from the actual quadratic transport budget

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianKL.gaussian_kl_reverse_transport · theorem · Teaching coverage

Read this first

Mathematical 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}.\]
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.

Download module (.lean)
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

Proof roadmap

  1. 1Attain 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.

  2. 2Identify 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.

  3. 3Use 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.

  4. 4Prove 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.

  5. 5Calculate 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.

  6. 6Identify 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.

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

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

Download module (.lean)
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

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Lemma6.3(i) states Gaussian KL reverse transport for Euclidean P2 probabilities using W2.Finite-dimensional real inner-product Borel probabilities including zero dimension, with actual infimum quadratic-cost budget and no marginal moments.generalizationThe proof uses only finite coupling displacement moment, which does not imply marginal second moments; full W2 API identification remains separate.
Positive heat time with exact coefficient 1/(2tau).tau>0,nonnegative radius r and actual ENNReal KL <=ofReal(r^2/(2tau)).sameActual noise scale sqrt(tau), forward KL direction and exact joint LLR formula preserve normalization.
The standard Gaussian regularization inequality is invoked in the A1 stage of Theorem6.5.Expanded optimal coupling, joint likelihood, proved LLR integrability, exact output marginals and KL data processing.source-implicitNo Gaussian KL contract, optimizer, target integrability or exponential displacement moment is assumed.
Full recursive sampling main results also require actual conditional kernels and costs.This actual probability-measure Gaussian KL prerequisite only.API-limitationRecursive kernels, full Wasserstein API, sampler error and query-cost statements are not claimed.

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.

Encoder–denoiser: accepted · domain-mismatch

Detected semantic differences

  • domains: Explicit finite-dimensional generalization includes zero dimension. — No positive dimension or division by dimension.
  • assumptions: Raw displacement-cost budget generalizes marginal P2; no marginal moment inference. — Optimum and displacement integrability derived; marginal moments neither used nor concluded.
  • conclusion: Radius r^2 budget, not a full W2 metric API identity. — Disclosed radius budget; actual divergence, not totalized toReal. Full W2 identity separate.
  • scopes: Joint likelihood and KL projection elaborate the source short joint-convexity argument without Gaussian KL or exponential-moment premises. — Recursive kernels, sampler errors and query costs excluded.

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
  • 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.
Sources, dependencies, and reuse

Source and reuse

Samplinglib 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

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

Which proof obligations and prerequisites are covered?

  • Independently verified prerequisite Actual ENNReal Gaussian KL bound from the true quadratic transport infimum