Samplinglib mathematical lesson

Actual Gaussian numerical kernel: integrated law and source transport contraction

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualKernelTransport.source_kernel_transport_contraction · theorem · Teaching coverage

Read this first

Mathematical statement

Construct a Markov K whose law at every z is Gamma.map(zeta → Phi(z,zeta)). For all probability mu,nu, K composed with each input equals the actual pushforward Phi#(input×Gamma), and W_M²(Kmu,Knu)≤(1-h/(65536kappa))² W_M²(mu,nu). This is the actual deterministic exact-gradient Gaussian numerical kernel, not an arbitrary supplied contracting kernel and not an invariant-target theorem.

\[K(z)=\Phi_z{}_{\#}\Gamma,\quad K\mu=\Phi_\#(\mu\otimes\Gamma),\quad W_{2,M_\kappa}^2(K\mu,K\nu)\le\left(1-\frac{h}{65536\kappa}\right)^2W_{2,M_\kappa}^2(\mu,\nu).\]

Lean statement · source_kernel_transport_contraction

Exact randomized law/actual Phi and Markov semantics, canonical raw source cost.

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 source_kernel_transport_contraction {f : E → ℝ} {κ h : ℝ} {J : ℕ}
    (hκ : 1 ≤ κ) (hf : ContDiff ℝ 2 f)
    (hH : ∀ z v, (1 / (2 * κ)) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) z v) v ∧
      (fderiv ℝ (fderiv ℝ f) z v) v ≤ ‖v‖ ^ 2)
    (hJ : 2 ≤ J) (hh : 0 < h) :
    let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
    let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
    let Λ := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Icc 0 h)
    let ω := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
    let b := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
    let c := fun j : Fin J => ∫ s in 0..h, (h-s)*(ell j).eval s
    h * Λ ≤ 1/(65536*κ) →
    let a := Real.exp (-h / 2)
    let sigma := Real.sqrt (1 - Real.exp (-h))
    let P0 := fun (z ζ : E × E) => a • z.2 + sigma • ζ.1
    let Y0 := fun (z ζ : E × E) j => z.1 + t j • P0 z ζ
    let Y1 := fun (z ζ : E × E) i => Y0 z ζ i - ∑ j, ω i j • gradient f (Y0 z ζ j)
    let Φ := fun w : (E × E) × (E × E) =>
      (w.1.1 + h • P0 w.1 w.2 - ∑ j, c j • gradient f (Y1 w.1 w.2 j),
        a • (P0 w.1 w.2 - ∑ j, b j • gradient f (Y1 w.1 w.2 j)) + sigma • w.2.2)
    let Γ := (stdGaussian E).prod (stdGaussian E)
    ∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
      (∀ z, K z = Γ.map (fun ζ => Φ (z,ζ))) ∧
      ∀ (μ ν : Measure (E × E)), IsProbabilityMeasure μ → IsProbabilityMeasure ν →
        K ∘ₘ μ = (μ.prod Γ).map Φ ∧ K ∘ₘ ν = (ν.prod Γ).map Φ ∧
        phaseWassersteinSq κ (K ∘ₘ μ) (K ∘ₘ ν) ≤
          ENNReal.ofReal ((1-h/(65536*κ))^2) * phaseWassersteinSq κ μ ν

Exact module and namespace context

Proof roadmap

1Recover actual joint measurability
The genuine source quadrature constructor gives Lambda≥1. The actual step condition gives h≤1 and h²Lambda≤1. Reuse FirstOrderDifference for exactly the same coefficients/potential/Phi; its jointly measurable actual numerical map is the needed random-map producer.
2Build the Markov kernel and prove both laws
Use (id times const Gamma).map Phi. Markovness follows from actual independent probability refreshes and measurable Phi. At each z, dirac×Gamma followed by map composition gives Gamma.map(Phi_z). For any probability input, the map-composition and constant-kernel product identities yield Kmu=Phi#(mu×Gamma). These identities justify the actual kernel semantics before applying a law-level inequality.
3Square the actual source norm contraction
The existing ActualContraction theorem proves the source Q norm contraction for every input and common noise, using the actual numerical phase. Delta=1-h/(65536kappa) is strictly positive. The unchanged Q lower comparison gives nonnegative Q for all phase displacements. Square the genuine sqrt inequality and reuse the squared sqrt identity, then apply ofReal multiplication. This proves the measurable extended pointwise cost bound with A=ofReal(delta²); it is not a public supplied premise of this consumer.
4Consume the shared genuine coupling lift
The source cost is measurable by its exact Q formula. A is positive and finite. Apply the shared randomized-map transport theorem to the actual Phi, actual Gaussian product law and arbitrary input probabilities, then rewrite both actual kernel laws. No optimizer, finite transport premise, invariant measure or selection of the state-dependent H/R is introduced.

Full assumptions and notation

All objects and hypotheses

E is a complete finite-dimensional real inner-product Borel space, including zero dimension. kappa≥1, f:E→R is globally C2 and its actual nested second derivative satisfies (2kappa)^-1||v||²≤D²f(z)[v,v]≤||v||² for every z,v. Producing the actual source f=V_eta remains open.
J≥2,h>0; t_j=h(1-cos(j*pi/(J-1)))/2, cardinal ell_j, and omega_ij=integral_0^t_i(t_i-s)ell_j(s)ds, b_j=integral_0^h ell_j(s)ds,c_j=integral_0^h(h-s)ell_j(s)ds are the actual coefficients. Lambda=sup_[0,h] sum_j |ell_j| and actual hLambda≤1/(65536kappa).
a=exp(-h/2),sigma=sqrt(1-exp(-h)); P0=a p+sigma zeta0, Y0_j=x+t_jP0, Y1_i=Y0_i-sum_j omega_ij gradient f(Y0_j), Phi=(x+hP0-sum_j c_j gradient f(Y1_j),a(P0-sum_j b_j gradient f(Y1_j))+sigma zeta1). Gamma=standard Gaussian E product standard Gaussian E, with independent refresh vectors.
Both input laws mu,nu are arbitrary probability laws on phase space; their source quadratic transport may be infinite. Q_kappa(x,p)=((2kappa)^-1+1/2)||x||²+inner(x,p)+||p||², c_kappa(z,zprime)=ofReal Q_kappa(z-zprime), and W_M²=T_c_kappa. Source Q is retained, not the ordinary product max norm.

Mathematical proof

1. Recover actual joint measurability

The genuine source quadrature constructor gives Lambda≥1. The actual step condition gives h≤1 and h²Lambda≤1. Reuse FirstOrderDifference for exactly the same coefficients/potential/Phi; its jointly measurable actual numerical map is the needed random-map producer.

\[\Lambda_J\ge1,\quad h\le1,\quad h^2\Lambda_J\le1,\quad\Phi\text{ jointly measurable}.\]

Corresponding Lean step

hcoeff; hLambda; hs; hfirst.1; hΦ

2. Build the Markov kernel and prove both laws

Use (id times const Gamma).map Phi. Markovness follows from actual independent probability refreshes and measurable Phi. At each z, dirac×Gamma followed by map composition gives Gamma.map(Phi_z). For any probability input, the map-composition and constant-kernel product identities yield Kmu=Phi#(mu×Gamma). These identities justify the actual kernel semantics before applying a law-level inequality.

\[K=(\mathrm{id}\times\mathrm{const}\,\Gamma).\mathrm{map}\,\Phi,\qquad K\mu=\Phi_\#(\mu\otimes\Gamma).\]

Corresponding Lean step

K; hK; Kernel.map_apply; Kernel.prod_apply; Measure.dirac_prod; hlaw; Measure.map_comp; Measure.compProd_eq_comp_prod; Measure.compProd_const

3. Square the actual source norm contraction

The existing ActualContraction theorem proves the source Q norm contraction for every input and common noise, using the actual numerical phase. Delta=1-h/(65536kappa) is strictly positive. The unchanged Q lower comparison gives nonnegative Q for all phase displacements. Square the genuine sqrt inequality and reuse the squared sqrt identity, then apply ofReal multiplication. This proves the measurable extended pointwise cost bound with A=ofReal(delta²); it is not a public supplied premise of this consumer.

\[c_\kappa(\Phi_z(\zeta),\Phi_{z\prime}(\zeta))\le\delta^2c_\kappa(z,z\prime),\qquad\delta>0.\]

Corresponding Lean step

hδ; nonnegQ; ActualContraction.source_synchronous_contraction; hcon; hsq; Real.sq_sqrt; ENNReal.ofReal_mul

4. Consume the shared genuine coupling lift

The source cost is measurable by its exact Q formula. A is positive and finite. Apply the shared randomized-map transport theorem to the actual Phi, actual Gaussian product law and arbitrary input probabilities, then rewrite both actual kernel laws. No optimizer, finite transport premise, invariant measure or selection of the state-dependent H/R is introduced.

\[W_{2,M_\kappa}^2(K\mu,K\nu)\le\delta^2W_{2,M_\kappa}^2(\mu,\nu).\]

Corresponding Lean step

hc; transportCost_randomized_map_le; hlaw

Lean verification

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

Lean proof · source_kernel_transport_contraction

Genuine synchronous coupling / actual kernel-law producer, measurable nonnegative integrals and positive finite scaled raw infimum.

Download module (.lean)

theorem source_kernel_transport_contraction {f : E → ℝ} {κ h : ℝ} {J : ℕ}
    (hκ : 1 ≤ κ) (hf : ContDiff ℝ 2 f)
    (hH : ∀ z v, (1 / (2 * κ)) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) z v) v ∧
      (fderiv ℝ (fderiv ℝ f) z v) v ≤ ‖v‖ ^ 2)
    (hJ : 2 ≤ J) (hh : 0 < h) :
    let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
    let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
    let Λ := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Icc 0 h)
    let ω := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
    let b := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
    let c := fun j : Fin J => ∫ s in 0..h, (h-s)*(ell j).eval s
    h * Λ ≤ 1/(65536*κ) →
    let a := Real.exp (-h / 2)
    let sigma := Real.sqrt (1 - Real.exp (-h))
    let P0 := fun (z ζ : E × E) => a • z.2 + sigma • ζ.1
    let Y0 := fun (z ζ : E × E) j => z.1 + t j • P0 z ζ
    let Y1 := fun (z ζ : E × E) i => Y0 z ζ i - ∑ j, ω i j • gradient f (Y0 z ζ j)
    let Φ := fun w : (E × E) × (E × E) =>
      (w.1.1 + h • P0 w.1 w.2 - ∑ j, c j • gradient f (Y1 w.1 w.2 j),
        a • (P0 w.1 w.2 - ∑ j, b j • gradient f (Y1 w.1 w.2 j)) + sigma • w.2.2)
    let Γ := (stdGaussian E).prod (stdGaussian E)
    ∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
      (∀ z, K z = Γ.map (fun ζ => Φ (z,ζ))) ∧
      ∀ (μ ν : Measure (E × E)), IsProbabilityMeasure μ → IsProbabilityMeasure ν →
        K ∘ₘ μ = (μ.prod Γ).map Φ ∧ K ∘ₘ ν = (ν.prod Γ).map Φ ∧
        phaseWassersteinSq κ (K ∘ₘ μ) (K ∘ₘ ν) ≤
          ENNReal.ofReal ((1-h/(65536*κ))^2) * phaseWassersteinSq κ μ ν := by
  classical
  dsimp only
  let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
  let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
  let Λ := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Icc 0 h)
  let ω := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
  let b := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
  let c := fun j : Fin J => ∫ s in 0..h, (h-s)*(ell j).eval s
  intro hstep
  change h*Λ ≤ 1/(65536*κ) at hstep
  have hcoeff := TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficients hJ hh
  rcases hcoeff with ⟨_,_,_,_,_,hΛ,_,_⟩
  change 1 ≤ Λ at hΛ
  have hk : 0 < κ := lt_of_lt_of_le zero_lt_one hκ
  have hi : 1/(65536*κ) ≤ (1:ℝ) := (div_le_one (by positivity)).mpr (by linarith)
  have hh1 : h ≤ 1 := by nlinarith
  have hs : h^2*Λ ≤ 1 := by
    have hm := mul_le_mul_of_nonneg_left (hstep.trans hi) (le_of_lt hh)
    nlinarith
  let a := Real.exp (-h / 2)
  let sigma := Real.sqrt (1 - Real.exp (-h))
  let P0 := fun (z ζ : E × E) => a • z.2 + sigma • ζ.1
  let Y0 := fun (z ζ : E × E) j => z.1 + t j • P0 z ζ
  let Y1 := fun (z ζ : E × E) i => Y0 z ζ i - ∑ j, ω i j • gradient f (Y0 z ζ j)
  let Φ := fun w : (E × E) × (E × E) =>
    (w.1.1 + h • P0 w.1 w.2 - ∑ j, c j • gradient f (Y1 w.1 w.2 j),
      a • (P0 w.1 w.2 - ∑ j, b j • gradient f (Y1 w.1 w.2 j)) + sigma • w.2.2)
  let Γ := (stdGaussian E).prod (stdGaussian E)
  have hfirst := FirstOrderDifference.source_first_order_difference hκ hf hH hJ hh hs
  have hΦ : Measurable Φ := hfirst.1
  let K := (Kernel.id ×ₖ Kernel.const (E × E) Γ).map Φ
  have hK : IsMarkovKernel K := Kernel.IsMarkovKernel.map _ hΦ
  refine ⟨K,hK,?_,?_⟩
  · intro z
    dsimp only [K]
    rw [Kernel.map_apply _ hΦ, Kernel.prod_apply, Kernel.id_apply, Kernel.const_apply,
      Measure.dirac_prod, Measure.map_map hΦ (by fun_prop)]
    rfl
  · intro μ ν hμ hν
    letI : IsProbabilityMeasure μ := hμ
    letI : IsProbabilityMeasure ν := hν
    have hlaw (ρ : Measure (E × E)) [IsProbabilityMeasure ρ] :
        K ∘ₘ ρ = (ρ.prod Γ).map Φ := by
      dsimp only [K]
      rw [← Measure.map_comp ρ _ hΦ, ← Measure.compProd_eq_comp_prod,
        Measure.compProd_const]
    refine ⟨hlaw μ,hlaw ν,?_⟩
    rw [hlaw μ,hlaw ν]
    let δ := 1-h/(65536*κ)
    have hδ : 0 < δ := by
      dsimp only [δ]
      apply sub_pos.mpr
      exact (div_lt_one (by positivity)).mpr (by linarith)
    have nonnegQ (v : E × E) : 0 ≤ phaseQuadraticForm κ v := by
      have hl := ordinary_energy_le_phaseQuadraticForm hκ v
      nlinarith [sq_nonneg ‖v.1‖,sq_nonneg ‖v.2‖]
    have hcost : ∀ z z' ζ : E × E,
        phaseCost κ (Φ (z,ζ),Φ (z',ζ)) ≤
          ENNReal.ofReal (δ^2)*phaseCost κ (z,z') := by
      intro z z' ζ
      have hcon := ActualContraction.source_synchronous_contraction hκ hf hH hJ hh hstep z z' ζ
      change Real.sqrt (phaseQuadraticForm κ (Φ (z,ζ)-Φ (z',ζ))) ≤
        δ*Real.sqrt (phaseQuadraticForm κ (z-z')) at hcon
      have hsq := (sq_le_sq₀ (Real.sqrt_nonneg _)
        (mul_nonneg hδ.le (Real.sqrt_nonneg _))).mpr hcon
      rw [mul_pow, Real.sq_sqrt (nonnegQ _), Real.sq_sqrt (nonnegQ _)] at hsq
      change ENNReal.ofReal (phaseQuadraticForm κ (Φ (z,ζ)-Φ (z',ζ))) ≤
        ENNReal.ofReal (δ^2)*ENNReal.ofReal (phaseQuadraticForm κ (z-z'))
      rw [← ENNReal.ofReal_mul (sq_nonneg δ)]
      exact ENNReal.ofReal_le_ofReal hsq
    have hc : Measurable (phaseCost (E := E) κ) := by
      unfold phaseCost phaseQuadraticForm
      fun_prop
    exact TechnicalLemmas.Measure.RandomizedMapTransport.transportCost_randomized_map_le
      Φ hΦ (phaseCost κ) hc (ENNReal.ofReal (δ^2))
      (ne_of_gt (ENNReal.ofReal_pos.mpr (sq_pos_of_pos hδ)))
      ENNReal.ofReal_ne_top hcost μ ν Γ

end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualKernelTransport

Exact module and namespace context

Scope and omitted-condition boundaries

Actual Gaussian exact-gradient numerical K at the explicit normalized global C2 curvature interface. Actual f=V_eta smoothing/C2/curvature remains separate. No target invariance/stationarity, numerical target bias, stochastic Khat/Kbar, local errors/history/expected query cost, Wp/proxy-warmness/initialization, PBPS or either complete main/composition result. TV proximity does not transfer unbounded cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Kernel.IsMarkovKernel.map
Kernel.map_apply
Kernel.prod_apply
Kernel.id_apply
Kernel.const_apply
Measure.dirac_prod
Measure.map_map
Measure.map_comp
Measure.compProd_eq_comp_prod
Measure.compProd_const
sq_le_sq₀
Real.sq_sqrt
ENNReal.ofReal_mul
ENNReal.ofReal_le_ofReal
ENNReal.ofReal_pos
ENNReal.ofReal_ne_top
div_lt_one

Mathematical sources

SPHMC actual common-noise transport prerequisite — Actual Gaussian exact-gradient numerical K at the explicit normalized global C2 curvature interface. Actual f=V_eta smoothing/C2/curvature remains separate. No target invariance/stationarity, numerical target bias, stochastic Khat/Kbar, local errors/history/expected query cost, Wp/proxy-warmness/initialization, PBPS or either complete main/composition result. TV proximity does not transfer unbounded cost.

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