Actual numerical phase: synchronous increment in the source metric
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualIncrement.source_synchronous_increment · theorem · Teaching coverage
Mathematical statement
For the actual full exact-gradient two-refresh two-Picard Phi, the synchronous increment difference obeys sqrt Q_kappa((Phi_z-Phi_zprime)-(z-zprime)) ≤12 h sqrt Q_kappa(z-zprime), under the explicit normalized C2 curvature interface and actual h Lambda≤1/(65536 kappa). This is the source difference of increments because vector subtraction is additive. The source universal C is explicitly elaborated as12, with the same c1/65536 as the actual contraction. All compared states and common noise values are included.
Lean statement · source_synchronous_increment
Actual integral coefficients, genuine global normalized C2 f, full Phi and all-input/common-noise difference of increments; exact original source Q.
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_increment {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.1-z'.1),
((Φ (z,ζ)).2-(Φ (z',ζ)).2)-(z.2-z'.2))) ≤
12*h*Real.sqrt (phaseQuadraticForm κ (z.1-z'.1,z.2-z'.2))Proof roadmap
- 1Consume the actual numerical expansion
The compiled actual source coefficient constructor gives Lambda≥1. Derive h≤1 and h²Lambda≤1 from the stated source step condition. Then apply the actual FirstOrderDifference constructor to this same Phi, exact source coefficients and genuine gradient. For each compared input/noise, it produces a symmetric actual segment-averaged H, ||H||op≤1, and an internally constructed R, with q=d+h A_H d+Rd and ||R||op≤8Lambda h². No H or R is a public hypothesis.
- 2Control the genuine drift and remainder
From kappa≥1 and hLambda≤1/(65536kappa), derive 8hLambda≤1. The actual remainder therefore satisfies ||Rd||2≤h||d||2. The operator norm bound gives ||Hd_x||≤||d_x||. Decompose the true Euclidean product into its two coordinate axes and use the triangle inequality to obtain ||A_Hd||2≤||d_x||+2||d_p||≤3||d||2. These calculations remain inline inside this real consumer; no copied background theorem receives separate credit.
- 3Bound the actual synchronous increment
Subtract d from the actual expansion. The norm of h A_Hd+Rd is at most h times3||d||2 plus h||d||2. Common noise cancellation is already established in the actual expansion parent; it is not assumed for an abstract phase.
- 4Reuse the exact original source metric comparisons
Call the existing unchanged public source APIs. They prove ||v||2²≤6Q(v) and Q(v)≤3||v||2²/2. Hence Q(q-d)≤24h²||d||2²≤144h²Q(d). Both comparisons use the original exact Q, not a replacement metric or supplied coercivity certificate.
- 5Take square roots without dividing by displacement
The lower comparison proves Q(d)≥0 and Q(q-d)≥0 even when d=0 or the space has dimension zero. Using squared square-root identities and nonnegative h, take square roots of the previous inequality. This yields12h sqrt Q(d); no strictly positive displacement is needed. Reordering coordinate subtraction identifies q-d with the source difference of increments.
Full assumptions and notation
All objects and hypotheses
- E is a complete finite-dimensional real inner-product Borel space, including dimension zero. f:E→R is globally C2, kappa≥1, and its genuine nested second derivative satisfies (2kappa)^-1||v||^2≤D2f(z)[v,v]≤||v||^2 for every z,v. This is the explicit normalized smoothed-potential interface; the actual f=V_eta producer remains independently open.
- J≥2,h>0. Actual Chebyshev-Lobatto nodes t_j=h/2(1-cos(j*pi/(J-1))), cardinal polynomials ell_j and ordinary Lebesgue integral weights 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. Lambda=sup_[0,h] sum_j|ell_j| and h Lambda≤1/(65536 kappa). No supplied convenient weights, Hessian, phase or remainder certificate.
- 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_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). The same two noise vectors are shared by the two inputs. The inequality is for every z,zprime,zeta, not only almost surely.
- Q_kappa(x,p)=((2kappa)^-1+1/2)||x||^2+inner(x,p)+||p||^2. The source M_kappa norm is sqrt Q. Intermediate Euclidean phase norms are the true WithLp2 product; the ordinary product max norm is not substituted.
Mathematical proof
1. Consume the actual numerical expansion
The compiled actual source coefficient constructor gives Lambda≥1. Derive h≤1 and h²Lambda≤1 from the stated source step condition. Then apply the actual FirstOrderDifference constructor to this same Phi, exact source coefficients and genuine gradient. For each compared input/noise, it produces a symmetric actual segment-averaged H, ||H||op≤1, and an internally constructed R, with q=d+h A_H d+Rd and ||R||op≤8Lambda h². No H or R is a public hypothesis.
Corresponding Lean step
hcoeff; hLambda; hs; hfirst; hp; heq; hR
2. Control the genuine drift and remainder
From kappa≥1 and hLambda≤1/(65536kappa), derive 8hLambda≤1. The actual remainder therefore satisfies ||Rd||2≤h||d||2. The operator norm bound gives ||Hd_x||≤||d_x||. Decompose the true Euclidean product into its two coordinate axes and use the triangle inequality to obtain ||A_Hd||2≤||d_x||+2||d_p||≤3||d||2. These calculations remain inline inside this real consumer; no copied background theorem receives separate credit.
Corresponding Lean step
hsmall; hrprime; hHx; hAp; hA; WithLp.norm_toLp_fst; WithLp.norm_toLp_snd
3. Bound the actual synchronous increment
Subtract d from the actual expansion. The norm of h A_Hd+Rd is at most h times3||d||2 plus h||d||2. Common noise cancellation is already established in the actual expansion parent; it is not assumed for an abstract phase.
Corresponding Lean step
hincr; hn; norm_add_le; norm_smul
4. Reuse the exact original source metric comparisons
Call the existing unchanged public source APIs. They prove ||v||2²≤6Q(v) and Q(v)≤3||v||2²/2. Hence Q(q-d)≤24h²||d||2²≤144h²Q(d). Both comparisons use the original exact Q, not a replacement metric or supplied coercivity certificate.
Corresponding Lean step
ordinary_energy_le_phaseQuadraticForm; phaseQuadraticForm_le_ordinary_energy; hl; hu; hquad
5. Take square roots without dividing by displacement
The lower comparison proves Q(d)≥0 and Q(q-d)≥0 even when d=0 or the space has dimension zero. Using squared square-root identities and nonnegative h, take square roots of the previous inequality. This yields12h sqrt Q(d); no strictly positive displacement is needed. Reordering coordinate subtraction identifies q-d with the source difference of increments.
Corresponding Lean step
hQd0; hQi0; hsq; 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_increment
Actual expansion producer, derived R/drift/increment norms, original unchanged source Q comparisons and nonnegative square-root argument.
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_increment {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.1-z'.1),
((Φ (z,ζ)).2-(Φ (z',ζ)).2)-(z.2-z'.2))) ≤
12*h*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 hsmall : 8*h*Λ ≤ 1 := by
have hc : 8/(65536*κ) ≤ (1:ℝ) := (div_le_one (by positivity)).mpr (by linarith)
have hm := mul_le_mul_of_nonneg_left hstep (by norm_num : (0:ℝ) ≤ 8)
calc
8*h*Λ = 8*(h*Λ) := by ring
_ ≤ 8*(1/(65536*κ)) := hm
_ = 8/(65536*κ) := by ring
_ ≤ 1 := hc
have hr' : ‖R d‖ ≤ h*‖d‖ := by
have hc : 8*Λ*h^2 ≤ h := by
have hm := mul_le_mul_of_nonneg_right hsmall (le_of_lt hh)
nlinarith
exact hr.trans (mul_le_mul_of_nonneg_right hc (norm_nonneg d))
let A := WithLp.toLp 2 (d.snd,-H d.fst-d.snd)
have hHx : ‖H d.fst‖ ≤ ‖d.fst‖ :=
(H.le_opNorm _).trans (by simpa using mul_le_mul_of_nonneg_right hHnorm (norm_nonneg d.fst))
have hAp : ‖-H d.fst-d.snd‖ ≤ ‖d.fst‖+‖d.snd‖ :=
(norm_sub_le _ _).trans (by simpa using add_le_add_right hHx ‖d.snd‖)
have hA : ‖A‖ ≤ 3*‖d‖ := by
have ht := norm_add_le (WithLp.toLp 2 (d.snd,(0:E)))
(WithLp.toLp 2 ((0:E),-H d.fst-d.snd))
have hpairs : ‖A‖ ≤ ‖d.snd‖+‖-H d.fst-d.snd‖ := by
simpa only [A, ← WithLp.toLp_add, Prod.mk_add_mk, add_zero, zero_add,
WithLp.norm_toLp_fst, WithLp.norm_toLp_snd] using ht
linarith [WithLp.norm_fst_le (p := 2) E d, WithLp.norm_snd_le (p := 2) E d]
have hincr : q-d = h • A+R d := by rw [heq]; dsimp only [A]; abel
have hn : ‖q-d‖ ≤ 4*h*‖d‖ := by
rw [hincr]
have ht := norm_add_le (h • A) (R d)
rw [norm_smul, Real.norm_eq_abs, abs_of_pos hh] at ht
nlinarith [mul_le_mul_of_nonneg_left hA (le_of_lt hh)]
let Qd := phaseQuadraticForm κ (WithLp.ofLp d)
let Qi := phaseQuadraticForm κ (WithLp.ofLp (q-d))
change Real.sqrt Qi ≤ 12*h*Real.sqrt Qd
have hl := ordinary_energy_le_phaseQuadraticForm hκ (WithLp.ofLp d)
change ‖d.fst‖^2+‖d.snd‖^2 ≤ 6*Qd at hl
rw [← WithLp.prod_norm_sq_eq_of_L2 d] at hl
have hu := phaseQuadraticForm_le_ordinary_energy hκ (WithLp.ofLp (q-d))
change Qi ≤ (3/2:ℝ)*(‖(q-d).fst‖^2+‖(q-d).snd‖^2) at hu
rw [← WithLp.prod_norm_sq_eq_of_L2 (q-d)] at hu
have hQd0 : 0 ≤ Qd := by nlinarith [sq_nonneg ‖d‖]
have hQi0 : 0 ≤ Qi := by
have hlo := ordinary_energy_le_phaseQuadraticForm hκ (WithLp.ofLp (q-d))
change _ ≤ 6*Qi at hlo
nlinarith [sq_nonneg ‖(q-d).fst‖,sq_nonneg ‖(q-d).snd‖]
have hnsq : ‖q-d‖^2 ≤ (4*h*‖d‖)^2 :=
(sq_le_sq₀ (norm_nonneg _) (by positivity)).mpr hn
have hquad : Qi ≤ 144*h^2*Qd := by
have hm := mul_le_mul_of_nonneg_left hl (by positivity : 0 ≤ 24*h^2)
nlinarith
have hsq : (Real.sqrt Qi)^2 ≤ (12*h*Real.sqrt Qd)^2 := by
simpa only [mul_pow,Real.sq_sqrt hQd0,Real.sq_sqrt hQi0,
show (12:ℝ)^2=144 by norm_num] using hquad
exact (sq_le_sq₀ (Real.sqrt_nonneg _) (by positivity)).mp hsq
end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualIncrementScope and omitted-condition boundaries
- Actual Lemma4.8 normalized-curvature numerical interface only. The actual f=V_eta smoothing/C2/curvature producer is a separate prerequisite before claiming the fully instantiated source lemma. No measure-level contraction, Khat/Kbar bias/variance, local discretization, invariance, history/expected query cost, Wp/proxy-warmness/initialization, PBPS or either full main/composition result is proved here. TV closeness cannot transfer unbounded expected cost.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FirstOrderDifference.source_first_order_differenceAutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficientsAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.phaseQuadraticFormAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.ordinary_energy_le_phaseQuadraticFormAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric.phaseQuadraticForm_le_ordinary_energy
Mathlib API called (external library)
- ContinuousLinearMap.le_opNorm
- norm_sub_le
- norm_add_le
- norm_smul
- WithLp.norm_fst_le
- WithLp.norm_snd_le
- WithLp.norm_toLp_fst
- WithLp.norm_toLp_snd
- WithLp.prod_norm_sq_eq_of_L2
- Real.sq_sqrt
- sq_le_sq₀
- div_le_one
Mathematical sources
- SPHMC Lemma4.8 actual synchronous increment — Actual Lemma4.8 normalized-curvature numerical interface only. The actual f=V_eta smoothing/C2/curvature producer is a separate prerequisite before claiming the fully instantiated source lemma. No measure-level contraction, Khat/Kbar bias/variance, local discretization, invariance, history/expected query cost, Wp/proxy-warmness/initialization, PBPS or either full main/composition result is proved here. TV closeness cannot 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.