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
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.
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.
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))Proof roadmap
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
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.
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.
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.
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.
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.
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.
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.ActualContractionScope 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
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FirstOrderDifference.source_first_order_differenceAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.KineticDissipation.source_kinetic_dissipationAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.ordinary_energy_le_phaseQuadraticFormAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.phaseQuadraticForm_le_ordinary_energyAutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficientsAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.phaseQuadraticForm
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.