Samplinglib · shared mathematical prerequisite

Pairing a relative score with transport displacement

The analytic estimate behind the Cauchy–Schwarz step in Chewi’s proximal-sampling argument; first variation remains a separate theorem.

Theorem 1. Integrability of the score–displacement pairing

Statement

Let \(\gamma\) be a coupling of \(\mu,\nu\) on a finite-dimensional Euclidean space. Assume the two marginal squared norms are integrable. For \(\mu,\pi\) in the smooth finite score domain, put \(\ell=\log(d\mu/d\pi)\) using the selected RN representative and \(s=\nabla\ell\). Then the following scalar function is integrable under the coupling. Optimality is not required.

\[(x,y)\longmapsto\langle s(x),y-x\rangle\ \in L^1(\gamma).\]

\(\mu\ll\pi\); the selected \(\ell\) is differentiable \(\mu\)-almost everywhere; \(\|s\|^2\in L^1(\mu)\).
\((\mathrm{pr}_1)_\#\gamma=\mu,\ (\mathrm{pr}_2)_\#\gamma=\nu\), and \(\|x\|^2\) is integrable under both marginals. Probability and sigma-finiteness are not assumed.

Lean statement · integrable_pairing_of_isCoupling

hgamma contains the two marginal identities. hscore is a structure packaging absolute continuity, genuine almost-everywhere differentiability and finite squared-score energy. hmu and hnu are second-moment hypotheses. Integrable is the conclusion to prove; it is not supplied as a premise.

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 integrable_pairing_of_isCoupling
    (hgamma : Transport.IsCoupling gamma mu nu)
    (hscore : SmoothFiniteScoreDomain mu pi)
    (hmu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) mu)
    (hnu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) nu) :
    Integrable (fun z =>
      ⟪gradient (RNLogRatio.logRatio mu pi) z.1, z.2 - z.1⟫) gamma

Exact module and namespace context

Mathematical proof

We obtain two L² functions on the coupling space and dominate their inner product by the integrable product of their norms.

1. Pull score energy through the first marginal

The total gradient is measurable by an existing ASTIS result. Composition with the first projection is therefore strongly measurable almost everywhere. The marginal identity transports its squared integral exactly; it does not require independence of the coordinates.

\[\int \|s(x)\|^2\,d\gamma(x,y)=\int\|s(x)\|^2\,d\mu(x)=I(\mu\mid\pi).\]

How this step appears in Lean

memLp_score_and_displacement uses measurable_gradient and measurePreserving_fst_of_isCoupling; memLp_two_iff_integrable_sq_norm turns measurability plus integrable squared norm into MemLp at exponent 2.

2. Obtain displacement energy from marginal moments

The displacement is continuous. Its squared norm is dominated by the sum of the two marginal squared norms, so it is integrable. This is an existing ASTIS coupling lemma, reused rather than re-proved in this packet.

\[\|y-x\|^2\leq 2\|x\|^2+2\|y\|^2,\qquad \int\|y-x\|^2\,d\gamma<\infty.\]

How this step appears in Lean

integrable_norm_sub_sq_of_isCoupling supplies the integrable cost. norm_sub_rev reconciles x − y with y − x.

3. Justify the pairing integral before estimating it

The product of the two norm functions is integrable by the \(L^2\)-product theorem. Pointwise Cauchy–Schwarz dominates the scalar pairing by that product, while measurability is preserved by the inner product. Thus the displayed integral is a genuine integrable pairing, not merely the value of a totalized integral.

\[|\langle s(x),y-x\rangle|\leq\|s(x)\|\,\|y-x\|,\qquad \langle s(x),y-x\rangle\in L^1(\gamma).\]

How this step appears in Lean

hs.norm.integrable_mul hd.norm produces the dominating integrable product; Integrable.mono' with hs.1.inner hd.1 proves integrable_pairing_of_isCoupling.

Lean proof · integrable_pairing_of_isCoupling

obtain unpacks the two L² facts from the private helper. MemLp.integrable_mul proves integrability of the product of the norms. Integrable.mono' transfers integrability to the measurable inner product using its pointwise norm bound.

theorem integrable_pairing_of_isCoupling
    (hgamma : Transport.IsCoupling gamma mu nu)
    (hscore : SmoothFiniteScoreDomain mu pi)
    (hmu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) mu)
    (hnu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) nu) :
    Integrable (fun z =>
      ⟪gradient (RNLogRatio.logRatio mu pi) z.1, z.2 - z.1⟫) gamma := by
  obtain ⟨hs, hd⟩ := memLp_score_and_displacement hgamma hscore hmu hnu
  exact (hs.norm.integrable_mul hd.norm).mono' (hs.1.inner hd.1)
    (Filter.Eventually.of_forall fun _ => norm_inner_le_norm _ _)

/-- For an optimal coupling, the absolute canonical score/displacement pairing
is bounded by the square root of canonical Fisher information times the
actual Wasserstein distance. The moment hypotheses give integrable cost;
the optimal real/ENNReal cost identity rules out an infinite W2 cost before
its real representation is used. -/

Exact module and namespace context

Lean proof · memLp_score_and_displacement

Supporting proof called by the result above.

private theorem memLp_score_and_displacement
    (hgamma : Transport.IsCoupling gamma mu nu)
    (hscore : SmoothFiniteScoreDomain mu pi)
    (hmu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) mu)
    (hnu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) nu) :
    MemLp (fun z => gradient (RNLogRatio.logRatio mu pi) z.1) 2 gamma ∧
      MemLp (fun z => z.2 - z.1) 2 gamma := by
  have hscoreM : AEStronglyMeasurable
      (fun z => gradient (RNLogRatio.logRatio mu pi) z.1) gamma :=
    ((Analysis.MeasurableGradient.measurable_gradient _).comp measurable_fst).aestronglyMeasurable
  have hfst := CouplingQuadraticIntegrability.measurePreserving_fst_of_isCoupling hgamma
  constructor
  · exact (memLp_two_iff_integrable_sq_norm hscoreM).mpr
      (hfst.integrable_comp_of_integrable hscore.scoreSq_integrable)
  · apply (memLp_two_iff_integrable_sq_norm (by fun_prop)).mpr
    simpa only [norm_sub_rev] using
      CouplingQuadraticIntegrability.integrable_norm_sub_sq_of_isCoupling hgamma hmu hnu

/-- The canonical relative score paired with displacement is integrable under
any coupling of finite-second-moment marginals. Optimality is not needed. -/

Exact module and namespace context

Theorem 2. The optimal-coupling Fisher estimate

Statement

Under Theorem 1’s hypotheses, assume in addition that \(\gamma\) is quadratic-optimal. With \(I(\mu\mid\pi)=\int\|s\|^2\,d\mu\), the pairing is bounded by the square root of the score energy times the Wasserstein distance.

\[\left|\int \langle s(x),y-x\rangle\,d\gamma(x,y)\right|\leq \sqrt{I(\mu\mid\pi)}\,W_2(\mu,\nu),\qquad I(\mu\mid\pi)=\int\|s(x)\|^2\,d\mu(x).\]

All hypotheses of Theorem 1 remain in force. Quadratic optimality identifies \(\int\|y-x\|^2\,d\gamma\) with the actual optimal cost.
The distance in Lean is extended nonnegative. Finite moments imply finite cost before its real representation is used.

Lean statement · abs_integral_pairing_le_sqrt_information_mul_wasserstein

IsQuadraticOptimalCoupling includes the coupling equations plus optimality. Real.sqrt applies to the guarded finite Fisher information. The suffix toReal translates a finite extended distance to a real value; it is not permission to interpret an infinite distance as zero.

theorem abs_integral_pairing_le_sqrt_information_mul_wasserstein
    (hgamma : DisplacementInterpolation.IsQuadraticOptimalCoupling gamma mu nu)
    (hscore : SmoothFiniteScoreDomain mu pi)
    (hmu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) mu)
    (hnu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) nu) :
    |∫ z, ⟪gradient (RNLogRatio.logRatio mu pi) z.1, z.2 - z.1⟫ ∂gamma| ≤
      Real.sqrt (information mu pi hscore) *
        (WassersteinSpace.wassersteinDistance mu nu).toReal

Exact module and namespace context

Mathematical proof

The preceding proof provides pairing integrability, displacement L² integrability and the first-marginal score identity. Apply Hölder and identify the optimal cost.

1. Apply the existing Hölder inequality

First move the absolute value inside the integral, then dominate the inner product and apply Hölder with conjugate exponents 2 and 2. No first-variation or convexity assumption enters this calculation.

\[\begin{aligned}\left|\int\langle s(x),y-x\rangle\,d\gamma\right|&\leq\int\|s(x)\|\,\|y-x\|\,d\gamma\\&\leq\left(\int\|s(x)\|^2\,d\gamma\right)^{1/2}\left(\int\|y-x\|^2\,d\gamma\right)^{1/2}.\end{aligned}\]

How this step appears in Lean

The calc block follows norm_integral_le_integral_norm, integral_mono, and integral_mul_norm_le_Lp_mul_Lq with Real.HolderConjugate.two_two.

2. Identify the optimal cost, with finiteness retained

For an optimal coupling, the existing real/extended quadratic-cost bridge identifies the second factor. The moment bound guarantees finite transport cost before converting the extended distance to a real number. Substitute both energy identities and take the square root of a nonnegative square.

\[\int\|y-x\|^2\,d\gamma=W_2(\mu,\nu)^2,\qquad \sqrt{W_2(\mu,\nu)^2}=W_2(\mu,\nu).\]

How this step appears in Lean

hdispEq invokes integral_norm_sq_eq_wassersteinDistance_sq_toReal_of_optimal. The final rewrite uses Real.sqrt_sq ENNReal.toReal_nonneg. The focused test separately checks that the actual extended W₂ is not infinity.

Lean proof · abs_integral_pairing_le_sqrt_information_mul_wasserstein

The calc block is the displayed inequality chain. hscoreEq pulls back through the first marginal; hdispEq identifies the cost. The final rw substitutes these equalities and Real.sqrt_sq removes the square using nonnegativity.

theorem abs_integral_pairing_le_sqrt_information_mul_wasserstein
    (hgamma : DisplacementInterpolation.IsQuadraticOptimalCoupling gamma mu nu)
    (hscore : SmoothFiniteScoreDomain mu pi)
    (hmu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) mu)
    (hnu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) nu) :
    |∫ z, ⟪gradient (RNLogRatio.logRatio mu pi) z.1, z.2 - z.1⟫ ∂gamma| ≤
      Real.sqrt (information mu pi hscore) *
        (WassersteinSpace.wassersteinDistance mu nu).toReal := by
  let score := fun z : State (ι := ι) × State (ι := ι) =>
    gradient (RNLogRatio.logRatio mu pi) z.1
  let disp := fun z : State (ι := ι) × State (ι := ι) => z.2 - z.1
  obtain ⟨hscoreL, hdispL⟩ := memLp_score_and_displacement hgamma.1 hscore hmu hnu
  have hprod : Integrable (fun z => ‖score z‖ * ‖disp z‖) gamma :=
    hscoreL.norm.integrable_mul hdispL.norm
  have hpair := integrable_pairing_of_isCoupling hgamma.1 hscore hmu hnu
  have hcs := integral_mul_norm_le_Lp_mul_Lq (f := score) (g := disp)
    Real.HolderConjugate.two_two
    (by simpa using hscoreL) (by simpa using hdispL)
  have hscoreEq : (∫ z, ‖score z‖ ^ 2 ∂gamma) = information mu pi hscore := by
    rw [information_eq_integral_scoreSq]
    have hm : Measurable (scoreSq mu pi) :=
      (Analysis.MeasurableGradient.measurable_gradient _).norm.pow_const 2
    have hmap : gamma.map Prod.fst = mu := hgamma.1.1
    simpa only [hmap, score, scoreSq] using
      (integral_map (μ := gamma) measurable_fst.aemeasurable hm.aestronglyMeasurable).symm
  have hcost := CouplingQuadraticIntegrability.integrable_norm_sub_sq_of_isCoupling
    hgamma.1 hmu hnu
  have hdispEq : (∫ z, ‖disp z‖ ^ 2 ∂gamma) =
      (WassersteinSpace.wassersteinDistance mu nu).toReal ^ 2 := by
    simpa only [disp, norm_sub_rev, ENNReal.toReal_pow] using
      DisplacementRealQuadraticCost.integral_norm_sq_eq_wassersteinDistance_sq_toReal_of_optimal
        hgamma hcost
  change |∫ z, ⟪score z, disp z⟫ ∂gamma| ≤ _
  calc
    |∫ z, ⟪score z, disp z⟫ ∂gamma| ≤ ∫ z, ‖⟪score z, disp z⟫‖ ∂gamma := by
      simpa only [Real.norm_eq_abs] using
        (norm_integral_le_integral_norm (fun z => ⟪score z, disp z⟫) (μ := gamma))
    _ ≤ ∫ z, ‖score z‖ * ‖disp z‖ ∂gamma :=
      integral_mono hpair.norm hprod (fun _ => norm_inner_le_norm _ _)
    _ ≤ Real.sqrt (∫ z, ‖score z‖ ^ 2 ∂gamma) *
        Real.sqrt (∫ z, ‖disp z‖ ^ 2 ∂gamma) := by
      simpa only [Real.sqrt_eq_rpow, Real.rpow_two] using hcs
    _ = _ := by
      rw [hscoreEq, hdispEq, Real.sqrt_sq ENNReal.toReal_nonneg]

end

end AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalFisherTransportPairing

Exact module and namespace context

What is still not proved by this result

This is not Theorem 8.4.1. Source certification is withheld: the smooth score of the source has not been identified with the selected RN representative’s classical total gradient. Almost-everywhere equality alone does not imply equality of classical gradients.
Specializing to probability laws, setting \(\nu=\pi\), constructing the source’s optimal graph coupling and identifying its expectation are still source adapters.
Finite entropy, a genuine KL first variation, endpoint one-sided versus two-sided differentiation, convexity, heat-flow domains and the proximal convergence theorem are not supplied.
The test removes an assumed Cauchy–Schwarz bound from an existing geodesic interface; the first variation and path/law adapters remain test hypotheses. Totalized klDiv.toReal is not evidence of finite entropy.

Proof dependencies

Declarations and reuse: ASTIS versus Mathlib

Results proved here by ASTIS

Existing ASTIS declarations reused

Mathlib results called, not re-proved here

MeasureTheory.memLp_two_iff_integrable_sq_norm — L² criterion
MeasureTheory.integral_mul_norm_le_Lp_mul_Lq — Hölder inequality; not a new ASTIS theorem
MeasureTheory.integral_map — Marginal change of variables

Focused tests · exact source

import AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalFisherTransportPairing
import AutoSamplingTheory.TechnicalLemmas.InformationTheory.GeodesicFisherTransport

open MeasureTheory
open scoped RealInnerProductSpace ENNReal
open AutoSamplingTheory.TechnicalLemmas
open InformationTheory InformationTheory.CanonicalRelativeFisher
open InformationTheory.CanonicalFisherTransportPairing
open Measure

noncomputable section

variable {ι : Type*} [Fintype ι]
  {mu pi nu : Measure (State (ι := ι))}
  {gamma : Measure (State (ι := ι) × State (ι := ι))}

-- Integrability is independently exercised for a non-optimal coupling.
example (hgamma : Transport.IsCoupling gamma mu nu)
    (hscore : SmoothFiniteScoreDomain mu pi)
    (hmu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) mu)
    (hnu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) nu) :
    Integrable (fun z =>
      ⟪gradient (RNLogRatio.logRatio mu pi) z.1, z.2 - z.1⟫) gamma :=
  integrable_pairing_of_isCoupling hgamma hscore hmu hnu

-- Finite optimal real cost rules out infinity before toReal is interpreted.
-- This check has no score, probability or sigma-finiteness assumption.
example (hgamma : DisplacementInterpolation.IsQuadraticOptimalCoupling gamma mu nu)
    (hmu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) mu)
    (hnu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) nu) :
    WassersteinSpace.wassersteinDistance mu nu ≠ ∞ := by
  have hcost := CouplingQuadraticIntegrability.integrable_norm_sub_sq_of_isCoupling
    hgamma.1 hmu hnu
  have heq :=
    DisplacementRealQuadraticCost.ofReal_integral_norm_sq_eq_wassersteinDistance_sq_of_optimal
      hgamma hcost
  intro hinfinite
  simp [hinfinite] at heq

-- Genuine consumer: the pairing is the actual gamma integral and FI/W2 are
-- the existing measure-level definitions. No hcs or equivalent bound is an input.
-- RED BOUNDARY: KL convexity, an ambient metric/law representation, and the
-- first variation of the actual KL path remain supplied. In particular the
-- HasDerivAt input is two-sided; this test does not manufacture the source's
-- endpoint first variation, finite entropy near zero, or a Wasserstein metric.
example [SigmaFinite pi] {M : Type*} [MetricSpace M]
    (law : M → Measure (State (ι := ι)))
    {isGeodesic : (ℝ → M) → Prop} {path : ℝ → M}
    (hgamma : DisplacementInterpolation.IsQuadraticOptimalCoupling gamma mu pi)
    (hscore : SmoothFiniteScoreDomain mu pi)
    (hmu : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) mu)
    (hpi : Integrable (fun x : State (ι := ι) => ‖x‖ ^ 2) pi)
    (hconvex : Geometry.GeodesicConvexity.IsAlphaGeodesicallyConvex isGeodesic
      (fun x => (_root_.InformationTheory.klDiv (law x) pi).toReal) 0)
    (hpath : isGeodesic path)
    (hlaw : ∀ t, law (path t) = DisplacementInterpolation.displacementInterpolation gamma t)
    (hdist : dist (path 0) (path 1) =
      (WassersteinSpace.wassersteinDistance mu pi).toReal)
    (hderiv : HasDerivAt
      (fun t => (_root_.InformationTheory.klDiv
        (DisplacementInterpolation.displacementInterpolation gamma t) pi).toReal)
      (∫ z, ⟪gradient (RNLogRatio.logRatio mu pi) z.1, z.2 - z.1⟫ ∂gamma) 0) :
    (_root_.InformationTheory.klDiv mu pi).toReal ^ 2 ≤
      information mu pi hscore * (WassersteinSpace.wassersteinDistance mu pi).toReal ^ 2 := by
  have hstart : law (path 0) = mu :=
    (hlaw 0).trans (DisplacementInterpolation.displacementInterpolation_zero hgamma.1)
  have hend : law (path 1) = pi :=
    (hlaw 1).trans (DisplacementInterpolation.displacementInterpolation_one hgamma.1)
  have hactual : (fun t => (_root_.InformationTheory.klDiv (law (path t)) pi).toReal) =
      (fun t => (_root_.InformationTheory.klDiv
        (DisplacementInterpolation.displacementInterpolation gamma t) pi).toReal) := by
    funext t
    rw [hlaw t]
  have hcs : -(∫ z, ⟪gradient (RNLogRatio.logRatio mu pi) z.1, z.2 - z.1⟫ ∂gamma) ≤
      Real.sqrt (information mu pi hscore) * dist (path 0) (path 1) := by
    rw [hdist]
    exact (neg_le_abs _).trans
      (abs_integral_pairing_le_sqrt_information_mul_wasserstein hgamma hscore hmu hpi)
  have hresult := GeodesicFisherTransport.sq_le_fisher_mul_dist_sq_of_geodesic_first_order
    hconvex hpath (hactual ▸ hderiv)
    (by simp [hend]) ENNReal.toReal_nonneg (information_nonneg mu pi hscore) hcs
  simpa only [hstart, hdist] using hresult

#check integrable_pairing_of_isCoupling
#check abs_integral_pairing_le_sqrt_information_mul_wasserstein
#print axioms integrable_pairing_of_isCoupling
#print axioms abs_integral_pairing_le_sqrt_information_mul_wasserstein

end

Source and evidence

This is original ASTIS exposition of a shared prerequisite, not a quotation or a replacement statement for a numbered source theorem. Expository coverage does not change formal completion.

Current checkout compilation not certified

Frontier Cell: proved_locally
Source comparison: rejected / domain-mismatch / needs-revision
Registry membership: 0 of 2 displayed results; repository Registry total: 438. Compilation and Registry admission are separate.

Source correspondence and exact audit records

Sinho Chewi, Log-Concave Sampling, August 9, 2026, proof of Theorem 8.4.1, printed p.221 / PDF p.233 — Motivation for the Cauchy–Schwarz step only; this is an ASTIS supplementary general-coupling derivation.

The immutable canonical edition is used. The independent source audit records domain-mismatch / needs-revision; this does not refute the compiled conditional inequality and must not be hidden by a green compilation badge.

Frontier Cell record · Independent source audit