ASTIS mathematical exposition

One truncation proxy for every Gaussian time and order

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProxyReverseTransport.proxy_reverse_transport · theorem · Teaching coverage

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

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

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

Lean proof · proxy_reverse_transport

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

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

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.

Source and reuse

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

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