One truncation proxy for every Gaussian time and order

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

Complete source statement (Samplinglib restatement)

Let P,Q be probability measures on a finite-dimensional real inner-product Borel space. Let real p>=2,r>=0 and 0<delta<1. Suppose the actual infimum over couplings of the pth displacement integral is at most ofReal(r^p). There exist one probability proxy Pdag and one probability coupling Gamma of Pdag,Q such that every measurable event B satisfies |P.real B-Pdag.real B|<=delta and norm(x-y)<=r delta^(-1/p) Gamma-a.e. For this same Pdag and Gamma, every tau>0 and real q>1 satisfy: Htau Pdag is absolutely continuous with respect to Htau Q; its actual ENNReal RN qth-power integral is at most ofReal exp(q(q-1)r^2/(2tau delta^(2/p))); the real RN qth power is integrable under Htau Q, its integral has the same exponential bound, and its logarithm divided by q-1 is at most q r^2/(2tau delta^(2/p)). Htau is the existing actual GaussianSmoothing operator with scale sqrt(tau).

Uniform actual proxy bound

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

One truncation proxy for every Gaussian time and order

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProxyReverseTransport.proxy_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. Let real p≥2,r≥0 and 0<delta<1. Suppose the actual infimum over couplings of the pth displacement integral is at most ofReal(r^p). There exist one probability proxy Pdag and one probability coupling Gamma of Pdag,Q such that every measurable event B satisfies |P.real B-Pdag.real B|≤delta and norm(x-y)≤r delta^(-1/p) Gamma-a.e. For this same Pdag and Gamma, every tau>0 and real q>1 satisfy: Htau Pdag is absolutely continuous with respect to Htau Q; its actual ENNReal RN qth-power integral is at most ofReal exp(q(q-1)r^2/(2tau delta^(2/p))); the real RN qth power is integrable under Htau Q, its integral has the same exponential bound, and its logarithm divided by q-1 is at most q r^2/(2tau delta^(2/p)). Htau is the existing actual GaussianSmoothing operator with scale sqrt(tau).

\[\exists P^\dagger,\Gamma\in\Pi(P^\dagger,Q):\quad\sup_B|P(B)-P^\dagger(B)|\le\delta,\qquad\forall\tau>0,\ q>1,\quad\frac{\log\int(dH_\tau P^\dagger/dH_\tau Q)^q\,dH_\tau Q}{q-1}\le\frac{qr^2}{2\tau\delta^{2/p}}.\]

Lean statement · proxy_reverse_transport

There exist a single actual proxy and coupling with eventwise TV/displacement and all-time/all-order Gaussian RN moment/log bounds.

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 proxy_reverse_transport {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (P Q : Measure E) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
    (p r δ : ℝ) (hp : 2 ≤ p) (hr : 0 ≤ r) (hδ : 0 < δ) (hδ1 : δ < 1)
    (hcost : Transport.transportCost (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^p)) P Q ≤ ENNReal.ofReal (r^p)) :
    ∃ Pdag : Measure E, ∃ Γ : Measure (E × E),
      IsProbabilityMeasure Pdag ∧ IsProbabilityMeasure Γ ∧ Transport.IsCoupling Γ Pdag Q ∧
      (∀ B, MeasurableSet B → |P.real B-Pdag.real B| ≤ δ) ∧
      (∀ᵐ z ∂Γ, ‖z.1-z.2‖ ≤ r*δ^(-1/p)) ∧
      ∀ τ : ℝ, 0 < τ → ∀ q : ℝ, 1 < q →
        let H := fun μ : Measure E => GaussianSmoothing.gaussianSmoothing μ (Real.sqrt τ)
        H Pdag ≪ H Q ∧
          (∫⁻ z, ((H Pdag).rnDeriv (H Q) z)^q ∂H Q) ≤
            ENNReal.ofReal (Real.exp (q*(q-1)*r^2/(2*τ*δ^(2/p)))) ∧
          Integrable (fun z => ((H Pdag).rnDeriv (H Q) z).toReal^q) (H Q) ∧
          (∫ z, ((H Pdag).rnDeriv (H Q) z).toReal^q ∂H Q) ≤
            Real.exp (q*(q-1)*r^2/(2*τ*δ^(2/p))) ∧
          Real.log (∫ z, ((H Pdag).rnDeriv (H Q) z).toReal^q ∂H Q)/(q-1) ≤
            q*r^2/(2*τ*δ^(2/p))

Exact module and namespace context

Proof roadmap

1Use the true transport budget to construct a truncation
Call the existing truncation theorem once. It attains the actual infimum cost, constructs T(x,y)=x inside the radius r delta^(-1/p) and y outside, and supplies the actual probability, marginal, TV and displacement conclusions. No optimizer or finite coupling moment is added as a premise.
2Fix both witnesses before choosing any heat time or order
Set Pdag=gamma.map T and Gamma=gamma.map((x,y) to (T(x,y),y)). These are probability measures, Gamma has actual Pdag,Q marginals, and the eventwise TV and a.e. displacement bounds already hold. Introduce tau and q only after supplying these existential witnesses.
3Apply actual Gaussian mixture reverse transport
For arbitrary tau>0,q>1, the threshold t is nonnegative. Apply the admitted GaussianMixture theorem to the fixed Gamma and Pdag,Q. This provides actual absolute continuity, finite ENNReal RN power bound, real-power integrability, exponential moment bound and normalized logarithm.
4Normalize the exact truncation radius
Since delta>0, real-power multiplication and negation give (delta^(-1/p))^2=(delta^(2/p))^(-1). Multiplying by r^2 gives t^2=r^2/delta^(2/p), valid also for r=0.
5Retain the full joint guarantee with exact constants
Substitute the same radius identity into both the exponential and normalized logarithm bounds. Keep all five smoothing conclusions alongside the previously fixed probability, coupling and TV/displacement facts. No use of TV to transport an unbounded cost is involved.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real inner-product Borel E, including zero dimension; P,Q probability measures.
Real p≥2 inherited from the source Lemma6.2 proof route. Lemma6.3(ii) does not independently restate this range; the formal statement makes it explicit.
r≥0 and0<delta<1, including zero radius. The genuine infimum p-displacement transportCost(P,Q)≤ofReal(r^p) is the input, not a supplied optimal coupling or proxy.
Finite marginal p-moments are not assumed or concluded; this raw-budget theorem is an explicit generalization of the source Pp presentation. Its relation to a full Wp metric API remains separate.
The same proxy and coupling precede all tau>0,q>1. Their independence from tau is justified by the actual truncation construction, strengthening the source fixed-time presentation.

Mathematical proof

1. Use the true transport budget to construct a truncation

Call the existing truncation theorem once. It attains the actual infimum cost, constructs T(x,y)=x inside the radius r delta^(-1/p) and y outside, and supplies the actual probability, marginal, TV and displacement conclusions. No optimizer or finite coupling moment is added as a premise.

\[t=r\delta^{-1/p},\qquad T(x,y)=\begin{cases}x,&\|x-y\|\le t,\\y,&\|x-y\|>t.\end{cases}\]

Corresponding Lean step

One call to Truncation.truncated_proxy with the actual hcost, p≥2 and delta/r conditions.

2. Fix both witnesses before choosing any heat time or order

Set Pdag=gamma.map T and Gamma=gamma.map((x,y) to (T(x,y),y)). These are probability measures, Gamma has actual Pdag,Q marginals, and the eventwise TV and a.e. displacement bounds already hold. Introduce tau and q only after supplying these existential witnesses.

\[P^\dagger=T_\#\gamma,\quad\Gamma=(T,\operatorname{snd})_\#\gamma,\quad\exists P^\dagger,\Gamma\ \forall\tau>0\ \forall q>1.\]

Corresponding Lean step

The refine witness tuple is completed before intro tau hTau q hq; hTV compares P with that same Pdag.

3. Apply actual Gaussian mixture reverse transport

For arbitrary tau>0,q>1, the threshold t is nonnegative. Apply the admitted GaussianMixture theorem to the fixed Gamma and Pdag,Q. This provides actual absolute continuity, finite ENNReal RN power bound, real-power integrability, exponential moment bound and normalized logarithm.

\[\int(dH_\tau P^\dagger/dH_\tau Q)^q\,dH_\tau Q\le e^{q(q-1)t^2/(2\tau)}.\]

Corresponding Lean step

GaussianMixture.bounded_displacement_reverse_transport consumes the actual fixed coupling, with its probability facts already available.

4. Normalize the exact truncation radius

Since delta>0, real-power multiplication and negation give (delta^(-1/p))^2=(delta^(2/p))^(-1). Multiplying by r^2 gives t^2=r^2/delta^(2/p), valid also for r=0.

\[(r\delta^{-1/p})^2=\frac{r^2}{\delta^{2/p}}.\]

Corresponding Lean step

Real.rpow_natCast, rpow_mul and rpow_neg, followed by exact multiplication/division algebra. No division by r.

5. Retain the full joint guarantee with exact constants

Substitute the same radius identity into both the exponential and normalized logarithm bounds. Keep all five smoothing conclusions alongside the previously fixed probability, coupling and TV/displacement facts. No use of TV to transport an unbounded cost is involved.

\[\frac{q(q-1)t^2}{2\tau}=\frac{q(q-1)r^2}{2\tau\delta^{2/p}},\qquad\frac{qt^2}{2\tau}=\frac{qr^2}{2\tau\delta^{2/p}}.\]

Corresponding Lean step

hc1 and hc2 rewrite the entire conjunction from the actual mixture theorem; no new divergence or sampler-cost assumption.

Lean verification

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

Lean proof · proxy_reverse_transport

One actual truncation witness followed by actual Gaussian mixture reverse transport and exact positive-base exponent normalization.

Download module (.lean)

theorem proxy_reverse_transport {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (P Q : Measure E) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
    (p r δ : ℝ) (hp : 2 ≤ p) (hr : 0 ≤ r) (hδ : 0 < δ) (hδ1 : δ < 1)
    (hcost : Transport.transportCost (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^p)) P Q ≤ ENNReal.ofReal (r^p)) :
    ∃ Pdag : Measure E, ∃ Γ : Measure (E × E),
      IsProbabilityMeasure Pdag ∧ IsProbabilityMeasure Γ ∧ Transport.IsCoupling Γ Pdag Q ∧
      (∀ B, MeasurableSet B → |P.real B-Pdag.real B| ≤ δ) ∧
      (∀ᵐ z ∂Γ, ‖z.1-z.2‖ ≤ r*δ^(-1/p)) ∧
      ∀ τ : ℝ, 0 < τ → ∀ q : ℝ, 1 < q →
        let H := fun μ : Measure E => GaussianSmoothing.gaussianSmoothing μ (Real.sqrt τ)
        H Pdag ≪ H Q ∧
          (∫⁻ z, ((H Pdag).rnDeriv (H Q) z)^q ∂H Q) ≤
            ENNReal.ofReal (Real.exp (q*(q-1)*r^2/(2*τ*δ^(2/p)))) ∧
          Integrable (fun z => ((H Pdag).rnDeriv (H Q) z).toReal^q) (H Q) ∧
          (∫ z, ((H Pdag).rnDeriv (H Q) z).toReal^q ∂H Q) ≤
            Real.exp (q*(q-1)*r^2/(2*τ*δ^(2/p))) ∧
          Real.log (∫ z, ((H Pdag).rnDeriv (H Q) z).toReal^q ∂H Q)/(q-1) ≤
            q*r^2/(2*τ*δ^(2/p)) := by
  obtain ⟨γ,hγ,hcouple,hopt,hT,hPdag,hΓ,hΓcouple,hdisp,hTV⟩ :=
    Truncation.truncated_proxy P Q p r δ hp hr hδ hδ1 hcost
  let T := fun z : E × E => if ‖z.1-z.2‖ ≤ r*δ^(-1/p) then z.1 else z.2
  refine ⟨γ.map T,γ.map (fun z => (T z,z.2)),hPdag,hΓ,hΓcouple,hTV,hdisp,?_⟩
  intro τ hτ q hq
  let : IsProbabilityMeasure (γ.map T) := hPdag
  have ht : 0 ≤ r*δ^(-1/p) := mul_nonneg hr (Real.rpow_nonneg hδ.le _)
  have h := GaussianMixture.bounded_displacement_reverse_transport
    (γ.map T) Q (γ.map (fun z => (T z,z.2))) hΓcouple τ q (r*δ^(-1/p)) hτ hq ht hdisp
  have he : (r*δ^(-1/p))^2 = r^2 / δ^(2/p) := by
    rw [mul_pow]
    have hd : (δ^(-1/p))^2 = (δ^(2/p))⁻¹ := by
      rw [← Real.rpow_natCast,← Real.rpow_mul hδ.le]
      change δ^((-1/p)*(2 : ℝ)) = (δ^(2/p))⁻¹
      have hex : (-1/p)*(2 : ℝ) = -(2/p) := by ring
      rw [hex,Real.rpow_neg hδ.le]
    rw [hd]
    exact (div_eq_mul_inv _ _).symm
  have hc1 : q*(q-1)*(r*δ^(-1/p))^2/(2*τ) = q*(q-1)*r^2/(2*τ*δ^(2/p)) := by
    rw [he]
    ring
  have hc2 : q*(r*δ^(-1/p))^2/(2*τ) = q*r^2/(2*τ*δ^(2/p)) := by
    rw [he]
    ring
  dsimp only at h ⊢
  simpa only [hc1,hc2] using h

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProxyReverseTransport

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Lemma6.3(ii) uses P,Q in Pp and invokes Lemma6.2, which assumes p>=2; the former does not separately restate that range.	Explicit p>=2 and actual infimum displacement-cost budget, without marginal p-moment assumptions.	generalization	Retains the invoked proof route; finite coupling cost does not imply marginal moments. Full Wp API identification is separate.
The source states the bound at fixed heat time and uniformly over q>1.	One actual proxy and coupling precede every tau>0 and q>1.	generalization	The actual truncation construction is independent of both parameters.
Euclidean probability measures, TV proxy, and Renyi reverse-transport bound.	Finite-dimensional real inner-product Borel spaces including zero dimension; eventwise TV and actual RN integral/log certificate.	API-limitation	Explicit budget-form generalization; full Wasserstein/Renyi metric interfaces, recursive warmness and sampler costs are not claimed.
Exact q r^2/(2 tau delta^(2/p)) normalized logarithm bound.	Same coefficient, RN direction, denominator law, plus proved real-power integrability and finite ENNReal bound.	same	Actual truncation and Gaussian mixture theorems with exact positive-base exponent algebra.

Actual infimum p-cost budget and eventwise TV/RN-log certificate for the Lemma6.2 to6.3(ii) route. One proxy is fixed before all tau,q. Full Wp/Renyi API identification, marginal moment conclusions, recursive warmness and actual sampler/error/query-cost results remain separate.

Encoder–denoiser: accepted · domain-mismatch

Detected semantic differences

domains: Explicit finite-dimensional generalization including zero dimension. — No positive-dimension requirement or division by dimension.
assumptions: Raw displacement budget drops marginal Pp; finite cost does not imply marginal moments. — Disclosed budget generalization; truncation obtains optimizer; no marginal moments inferred.
assumptions: p>=2 inherited from Lemma6.2, not restated in Lemma6.3(ii). — Disclosed budget generalization; truncation obtains optimizer; no marginal moments inferred.
quantifiers: Uniform positive heat times supported by same truncation. — One truncation and existential tuple before intro tau,q; construction independent of both.
scopes: Budget/RN-log certificate does not establish full Wasserstein/Renyi APIs. — Full metric/divergence APIs, recursive warmness and sampler/error/cost remain separate.

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 infimum p-cost budget and eventwise TV/RN-log certificate for the Lemma6.2 to6.3(ii) route. One proxy is fixed before all tau,q. Full Wp/Renyi API identification, marginal moment conclusions, recursive warmness and actual sampler/error/query-cost results remain separate.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Real.rpow_mul
Real.rpow_neg
MeasureTheory.Measure.map

Mathematical sources

Chen, Chewi, Lu and Zhang, SPHMC v1 Lemmas6.2 and6.3(ii) — Actual-budget composition of truncation and Gaussian reverse transport. The p>=2 condition comes from invoked Lemma6.2; Lemma6.3(ii) does not separately repeat it.

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

One truncation proxy for every Gaussian time and order

Complete source statement (Samplinglib restatement)

Uniform actual proxy bound

Read the formalized proofs

One truncation proxy for every Gaussian time and order

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Use the true transport budget to construct a truncation

2. Fix both witnesses before choosing any heat time or order

3. Apply actual Gaussian mixture reverse transport

4. Normalize the exact truncation radius

5. Retain the full joint guarantee with exact constants

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?