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

ActualContraction: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. For every actual input pair and every common two-vector noise value, the source exact-gradient numerical phase obeys the M_kappa norm contraction with simultaneous explicit universal constant c=1/65536 under h Lambda_J<=c/kappa
Samplinglib mathematical lesson

For every actual input pair and every common two-vector noise value, the source exact-gradient numerical phase obeys the M_kappa norm contraction with simultaneous explicit universal constant c=1/65536 under h Lambda_J<=c/kappa

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualContraction.source_synchronous_contraction · theorem · Teaching coverage

Read this first

Mathematical statement

For every actual input pair and every common two-vector noise value, the source exact-gradient numerical phase obeys the M_kappa norm contraction with simultaneous explicit universal constant c=1/65536 under h Lambda_J≤c/kappa. The actual averaged Hessian and remainder are supplied by the independently compiled genuine algorithm producer, never assumed as a contraction/phase certificate.

\[h\Lambda_J\le\frac1{65536\kappa}\quad\Longrightarrow\quad\|\Phi_z(\zeta)-\Phi_{z\prime}(\zeta)\|_{M_\kappa}\le\left(1-\frac{h}{65536\kappa}\right)\|z-z\prime\|_{M_\kappa}.\]
Lean statement · source_synchronous_contraction

For every actual input pair and every common two-vector noise value, the source exact-gradient numerical phase obeys the M_kappa norm contraction with simultaneous explicit universal constant c=1/65536 under h Lambda_J<=c/kappa. The actual averaged Hessian and remainder are supplied by the independently compiled genuine algorithm producer, never assumed as a contraction/phase certificate.

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_synchronous_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)
    ∀ z z' ζ : E × E,
      Real.sqrt (phaseQuadraticForm κ ((Φ (z,ζ)).1-(Φ (z',ζ)).1,
        (Φ (z,ζ)).2-(Φ (z',ζ)).2)) ≤
      (1-h/(65536*κ))*Real.sqrt (phaseQuadraticForm κ (z.1-z'.1,z.2-z'.2))

Exact module and namespace context

Proof roadmap

  1. 1Reuse the actual numerical expansion

    The real coefficient producer gives Lambda≥1. The sole source step restriction derives h≤1 and h²Lambda≤1. Call the actual FirstOrderDifference theorem on this same Phi, obtaining genuine H, curvature, norm≤1 and Delta1=d+hA+Rd with ||R||≤8Lambda h². Its actual measurable Gaussian Markov semantics were established in the parent.

  2. 2Call the existing exact source norm comparisons

    Open the already proved Q definition and two comparisons as public APIs, preserving their original proofs. Polarize Q into B with coefficient alpha+1/2 on the xx block, 1/2 on both mixed blocks and1 on pp. Coordinate Cauchy--Schwarz yields B(u,v)≤3||u||2||v||2. No duplicate norm-comparison proof or new wrapper is introduced.

  3. 3Consume genuine kinetic dissipation

    The parent all-vector H curvature bounds feed the compiled full-space source drift theorem. Exact real inner-product algebra gives 2B(d,A)=-D_H(d)≤-Q(d)/(8kappa). The operator and coordinate triangle bounds imply ||A||≤3||d||, so Q(A)≤162Q(d); this constant is a deliberate conservative weakening.

  4. 4Expand the actual endpoint energy

    For r=Rd and L=Lambda h²≤1, derive ||d+hA||≤4||d|| and ||r||≤8L||d||. Thus the cross remainder is ≤1152LQ(d), the remainder energy is ≤1152LQ(d) using L²≤L, and h²Q(A)≤162LQ(d) using Lambda≥1. The exact polarized identity and drift imply the full endpoint bound.

  5. 5Absorb with an explicit universal step constant

    The actual step condition and2466<4096 give2466Lambda h²≤h/(16kappa). Hence the genuine endpoint Q is ≤(1-h/(16kappa))Q(d). No strengthened convenient h restriction or suppressed dimension dependence is added.

  6. 6Take square roots without division by input energy

    Let t=h/(65536kappa), so0≤t≤1. The stronger squared loss4096t is bounded by the square of1-t. Nonnegativity of both Q values follows from the original lower comparison. Real square-root identities and monotonicity give the target. No division by Q(d), so equal inputs and dimension0 are included.

Full assumptions and notation

All objects and hypotheses

  • E is a complete finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. f:E→R is genuinely globally C2, kappa≥1, and (2kappa)^-1||v||²≤D²f(z)[v,v]≤||v||² for all z,v. This is the explicit normalized potential interface; actual V_eta construction is an independent producer.
  • J≥2,h>0. Actual nodes t_j=h/2(1-cos(j*pi/(J-1))), actual Lagrange cardinals ell_j, Lambda_J=sup_[0,h] sum|ell_j|, omega_ij=integral_0^{t_i}(t_i-s)ell_j(s)ds, b_j=integral_0^h ell_j(s)ds and c_j=integral_0^h(h-s)ell_j(s)ds. The sole step restriction is h Lambda_J≤1/(65536 kappa); h≤1 and h²Lambda≤1 are derived.
  • a=exp(-h/2), sigma=sqrt(1-exp(-h)). P0=a p+sigma zeta0; Y0_j=x+t_j P0; Y1_i=Y0_i-sum omega_ij gradient f(Y0_j); Phi=(x+hP0-sum c_j gradient f(Y1_j), a(P0-sum b_j gradient f(Y1_j))+sigma zeta1). This is the actual exact-gradient phase, shared synchronously at every input/noise pair, not only almost surely.
  • Q_kappa(x,p)=(1/(2kappa)+1/2)||x||²+inner(x,p)+||p||² and norm_M=sqrt(Q). The proof uses genuine Euclidean L2 phase norms throughout; it never treats the default product max norm as Euclidean.

Mathematical proof

1. Reuse the actual numerical expansion

The real coefficient producer gives Lambda≥1. The sole source step restriction derives h≤1 and h²Lambda≤1. Call the actual FirstOrderDifference theorem on this same Phi, obtaining genuine H, curvature, norm≤1 and Delta1=d+hA+Rd with ||R||≤8Lambda h². Its actual measurable Gaussian Markov semantics were established in the parent.

\[\Delta_1=d+hA+Rd,\quad A=(\Delta p,-H\Delta x-\Delta p),\quad\|R\|\le8\Lambda_Jh^2.\]
Corresponding Lean step

source_first_order_difference; chebyshev_lobatto_coefficients; hfirst; hp; hr

2. Call the existing exact source norm comparisons

Open the already proved Q definition and two comparisons as public APIs, preserving their original proofs. Polarize Q into B with coefficient alpha+1/2 on the xx block, 1/2 on both mixed blocks and1 on pp. Coordinate Cauchy--Schwarz yields B(u,v)≤3||u||2||v||2. No duplicate norm-comparison proof or new wrapper is introduced.

\[\|d\|_2^2\le6Q(d),\quad Q(d)\le\tfrac32\|d\|_2^2,\quad B(u,v)\le3\|u\|_2\|v\|_2.\]
Corresponding Lean step

phaseQuadraticForm; ordinary_energy_le_phaseQuadraticForm; phaseQuadraticForm_le_ordinary_energy; B_bound; B_self

3. Consume genuine kinetic dissipation

The parent all-vector H curvature bounds feed the compiled full-space source drift theorem. Exact real inner-product algebra gives 2B(d,A)=-D_H(d)≤-Q(d)/(8kappa). The operator and coordinate triangle bounds imply ||A||≤3||d||, so Q(A)≤162Q(d); this constant is a deliberate conservative weakening.

\[2B(d,A)\le-\frac{Q(d)}{8\kappa},\quad\|A\|_2\le3\|d\|_2,\quad Q(A)\le162Q(d).\]
Corresponding Lean step

source_kinetic_dissipation; hD; hidentity; hlin; hA; hQA

4. Expand the actual endpoint energy

For r=Rd and L=Lambda h²≤1, derive ||d+hA||≤4||d|| and ||r||≤8L||d||. Thus the cross remainder is ≤1152LQ(d), the remainder energy is ≤1152LQ(d) using L²≤L, and h²Q(A)≤162LQ(d) using Lambda≥1. The exact polarized identity and drift imply the full endpoint bound.

\[Q(d+hA+r)=Q(d)+2hB(d,A)+h^2Q(A)+2B(d+hA,r)+Q(r)\le\left(1-\frac h{8\kappa}+2466\Lambda_Jh^2\right)Q(d).\]
Corresponding Lean step

quadratic_expansion; endpoint_quadratic_contraction; hcross; hqr; hAterm; hsum

5. Absorb with an explicit universal step constant

The actual step condition and2466<4096 give2466Lambda h²≤h/(16kappa). Hence the genuine endpoint Q is ≤(1-h/(16kappa))Q(d). No strengthened convenient h restriction or suppressed dimension dependence is added.

\[2466\Lambda_Jh^2\le\frac h{16\kappa},\quad Q(\Delta_1)\le\left(1-\frac h{16\kappa}\right)Q(d).\]
Corresponding Lean step

habsorb; hcoef; hquad

6. Take square roots without division by input energy

Let t=h/(65536kappa), so0≤t≤1. The stronger squared loss4096t is bounded by the square of1-t. Nonnegativity of both Q values follows from the original lower comparison. Real square-root identities and monotonicity give the target. No division by Q(d), so equal inputs and dimension0 are included.

\[1-4096t\le(1-t)^2,\quad\sqrt{Q(\Delta_1)}\le(1-t)\sqrt{Q(d)}.\]
Corresponding Lean step

hQd0; hQq0; hratio; hquadprime; Real.sq_sqrt; sq_le_sq₀

Lean verification

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

Lean proof · source_synchronous_contraction

Exact source form and compiled parent composition, with all source domains/constant absorption and zero cases explicit. Existing Q/comparison proofs unchanged.

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_synchronous_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)
    ∀ z z' ζ : E × E,
      Real.sqrt (phaseQuadraticForm κ ((Φ (z,ζ)).1-(Φ (z',ζ)).1,
        (Φ (z,ζ)).2-(Φ (z',ζ)).2)) ≤
      (1-h/(65536*κ))*Real.sqrt (phaseQuadraticForm κ (z.1-z'.1,z.2-z'.2)) := 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)
  have hfirst := FirstOrderDifference.source_first_order_difference hκ hf hH hJ hh hs
  intro z z' ζ
  let H := h⁻¹ • ∑ j, b j •
    (∫ u in (0:ℝ)..1, InnerProductSpace.continuousLinearMapOfBilin
      (fderiv ℝ (fderiv ℝ f) (Y1 z' ζ j+u • (Y1 z ζ j-Y1 z' ζ j))))
  let d := WithLp.toLp 2 (z.1-z'.1,z.2-z'.2)
  let q := WithLp.toLp 2 ((Φ (z,ζ)).1-(Φ (z',ζ)).1,(Φ (z,ζ)).2-(Φ (z',ζ)).2)
  have hp := hfirst.2.2 z z' ζ
  change H.toLinearMap.IsSymmetric ∧ (∀ v, 1/(2*κ)*‖v‖^2 ≤ inner ℝ (H v) v ∧
    inner ℝ (H v) v ≤ ‖v‖^2) ∧ ‖H‖ ≤ 1 ∧
    ∃ R : WithLp 2 (E × E) →L[ℝ] WithLp 2 (E × E), ‖R‖ ≤ 8*Λ*h^2 ∧
      q = d+h • WithLp.toLp 2 (d.snd,-H d.fst-d.snd)+R d at hp
  rcases hp with ⟨hsym,hcurv,hHnorm,R,hR,heq⟩
  have hr : ‖R d‖ ≤ 8*Λ*h^2*‖d‖ :=
    (R.le_opNorm d).trans (mul_le_mul_of_nonneg_right hR (norm_nonneg d))
  have hquad := endpoint_quadratic_contraction hκ hh hΛ hstep H hsym hcurv hHnorm d (R d) hr
  dsimp only at hquad
  rw [← heq] at hquad
  let Qd := phaseQuadraticForm κ (WithLp.ofLp d)
  let Qq := phaseQuadraticForm κ (WithLp.ofLp q)
  let t := h/(65536*κ)
  change Qq ≤ (1-h/(16*κ))*Qd at hquad
  change Real.sqrt Qq ≤ (1-t)*Real.sqrt Qd
  have hQd0 : 0 ≤ Qd := by
    have hl := ordinary_energy_le_phaseQuadraticForm hκ (WithLp.ofLp d)
    change _ ≤ 6*Qd at hl
    nlinarith [sq_nonneg ‖d.fst‖,sq_nonneg ‖d.snd‖]
  have hQq0 : 0 ≤ Qq := by
    have hl := ordinary_energy_le_phaseQuadraticForm hκ (WithLp.ofLp q)
    change _ ≤ 6*Qq at hl
    nlinarith [sq_nonneg ‖q.fst‖,sq_nonneg ‖q.snd‖]
  have ht0 : 0 ≤ t := by dsimp [t]; positivity
  have ht1 : t ≤ 1 := by
    have hc : h/(65536*κ) ≤ 1 := (div_le_one (by positivity)).mpr (by linarith)
    exact hc
  have hratio : h/(16*κ) = 4096*t := by dsimp only [t];field_simp;ring
  have hquad' : Qq ≤ (1-t)^2*Qd := by
    rw [hratio] at hquad
    nlinarith [mul_nonneg (sq_nonneg t) hQd0, mul_nonneg ht0 hQd0]
  have hsq : (Real.sqrt Qq)^2 ≤ ((1-t)*Real.sqrt Qd)^2 := by
    simpa only [mul_pow,Real.sq_sqrt hQd0,Real.sq_sqrt hQq0] using hquad'
  exact (sq_le_sq₀ (Real.sqrt_nonneg _) (mul_nonneg (sub_nonneg.mpr ht1) (Real.sqrt_nonneg _))).mp hsq

end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualContraction

Exact module and namespace context

Scope and omitted-condition boundaries
  • Actual deterministic exact-gradient numerical phase contraction at the explicit normalized C2 curvature interface. Actual f=V_eta smoothing/C2/curvature producer remains independently open. No Khat/Kbar substitution, increment/logLambda/B2, invariant law/local errors/history/query work, PBPS, either full main theorem or actual-input expected-cost composition. TV proximity does not transfer unbounded expected cost.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • WithLp.prod_norm_sq_eq_of_L2
  • real_inner_le_norm
  • Real.sq_sqrt
  • sq_le_sq₀

Mathematical sources

  • SPHMC actual numerical contraction and M_kappa — Actual deterministic exact-gradient numerical phase contraction at the explicit normalized C2 curvature interface. Actual f=V_eta smoothing/C2/curvature producer remains independently open. No Khat/Kbar substitution, increment/logLambda/B2, invariant law/local errors/history/query work, PBPS, either full main theorem or actual-input expected-cost composition. TV proximity does not transfer unbounded expected 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.