The actual exact-gradient Picard phase and its first-order difference
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FirstOrderDifference.source_first_order_difference · theorem · Teaching coverage
Mathematical statement
At this explicit normalized C2 curvature interface, the actual exact-gradient two-Picard map Phi is measurable and defines a Markov kernel K(z)=Gamma.map(Phi_z). For every synchronously coupled input pair and every two-vector noise value, the actual integral average H is symmetric, (2kappa)^-1 I≤H≤I and ||H||op≤1. There exists a genuine continuous real linear R on the L2 phase space such that Delta1=Delta0+h*(Delta p,-H Delta x-Delta p)+R Delta0 and ||R||op≤8 Lambda h^2. R may depend on z,zprime,zeta; no measurable choice or global derivative of Phi is asserted. H, Phi, K and the remainder are constructed, not supplied as conclusion certificates.
Lean statement · source_first_order_difference
Actual Chebyshev cardinal integrals, two Gaussian refreshes and genuine gradient f; exact source segment-averaged H; all-input pointwise L2 difference and norm-bounded linear remainder.
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_first_order_difference {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 ^ 2 * Λ ≤ 1 →
let a := Real.exp (-h / 2)
let sigma := Real.sqrt (1 - Real.exp (-h))
let Γ := (stdGaussian E).prod (stdGaussian E)
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)
Measurable Φ ∧
(∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
∀ z, K z = Γ.map (fun ζ => Φ (z, ζ))) ∧
∀ z z' ζ : E × E,
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)
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 ∧
WithLp.toLp 2 ((Φ (z,ζ)).1 - (Φ (z',ζ)).1,
(Φ (z,ζ)).2 - (Φ (z',ζ)).2) =
d + h • WithLp.toLp 2 (z.2-z'.2, -H (z.1-z'.1)-(z.2-z'.2)) + R dProof roadmap
- 1Use the genuine cardinal-integral parents
The compiled coefficient constructor supplies t_j in[0,h], the endpoint t_last=h, Lambda≥1, row absolute-integral bounds and sum b_j=h. The independent positive-weight theorem gives every b_j≥0. The endpoint c_j is exactly the last omega row. From h^2 Lambda≤1 and Lambda≥1 derive h≤1. No convenient coefficient or regularity certificates are assumed.
- 2Construct the real numerical phase and Gaussian kernel
Continuity of the genuine gradient follows from C2 and the continuous Riesz identification. Finite actual Picard sums and both OU half-refreshes therefore make Phi jointly measurable. Push forward Kernel.id product Kernel.const Gamma; the two independent Gaussian coordinates are actual inputs of this same map. The law is exactly Gamma.map Phi_z. This is K with deterministic gradient f, not stochastic Khat or the conditional-mean Kbar.
- 3Bound the actual first Picard error
Use the canonical Hessian-secant constructor at each Y0 pair, deriving the global gradient Lipschitz bound. Common Gaussian noise cancels, giving DeltaY0_j=Delta x+a t_j Delta p. Writing D=||Delta x||+||Delta p||, the actual E_i=-sum omega_ij Delta gradient_j has norm≤h^2 Lambda D/2. Since h^2 Lambda≤1, the loose bound ||DeltaY1_i||≤2D holds. All helpers are private algebra of this same source algorithm, with no separate proof credit.
- 4Produce the source integral average H
At each actual Y1 pair call the compiled genuine Hessian-secant theorem. It produces symmetry, all-vector inherited curvature and norm≤1. Form H=h^-1 sum b_j H_j using the real ordinary-cardinal integrals. Positive b_j and sum b_j=h preserve both diagonal bounds and symmetry; the operator triangle bound gives norm≤1. The source H is this exact integral average, not an arbitrary matrix satisfying the desired result.
- 5Expand both real endpoint residuals with explicit constants
The exact endpoint differences are Delta x+ah Delta p-sum c_j H_j DeltaY1_j and a^2 Delta p-a sum b_j H_j DeltaY1_j. The scalar exponential inequalities give |1-a|≤h/2 and |a^2-1+h|≤h^2. Let e=h^2 Lambda/2. The position residual has norm≤h^2||Delta p||/2+h^2 Lambda D. The momentum residual has norm≤h^2||Delta p||+h^2||Delta x||/2+h(h||Delta p||+eD). With h≤1 and Lambda≥1 their sum is ≤4h^2 Lambda D (in particular bounds 3/2 and 5/2 times h^2 Lambda D). These are actual residuals, not hypotheses.
- 6Use the source Euclidean phase norm
The L2 product norm satisfies ||(rx,rp)||2≤||rx||+||rp|| and each coordinate norm is ≤||(Delta x,Delta p)||2. Hence D≤2||Delta0||2, giving actual residual norm≤8 Lambda h^2||Delta0||2. This avoids using the default max norm as if it were the Euclidean norm.
- 7Construct the pointwise linear remainder
If Delta0=0, the derived residual bound forces r=0 and R=0 works. Otherwise define Rw=inner(Delta0,w) r/||Delta0||^2 using Mathlib rankOne. It satisfies R Delta0=r; its operator norm is ≤||r||/||Delta0||≤8 Lambda h^2. This explicitly elaborates the source existential remainder and omitted universal constant. It is not a differentiability/Jacobian claim or a measurable operator-choice claim.
Full assumptions and notation
All objects and hypotheses
- E is a complete finite-dimensional real inner-product space, including dimension zero, with its Borel measurable space. f:E→R is globally C2. kappa≥1 and every genuine nested second derivative satisfies (2kappa)^-1||v||^2 ≤ D2f(z)[v,v] ≤ ||v||^2 for every z,v. These are the normalized smoothed-potential curvature interface; f=V_eta and Lemma4.1 are independent prerequisites.
- J≥2,h>0. The nodes are t_j=h/2(1-cos(j*pi/(J-1))), ell_j their actual Lagrange cardinal polynomials, Lambda=sup_{s in[0,h]} sum_j|ell_j(s)|, 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. Assume only h^2 Lambda≤1. In particular h≤1 is derived, never added as a premise.
- a=exp(-h/2),sigma=sqrt(1-exp(-h)),Gamma=stdGaussian(E) product stdGaussian(E). Both Gaussian vectors are independent under Gamma and shared synchronously between compared inputs. 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). No stochastic gradient/proximal array appears.
- For every pair z,zprime and every Gaussian vector zeta (not just almost surely), H_j is the ordinary Bochner integral of the Riesz-represented genuine D2f along the Y1prime_j-to-Y1_j segment; H=h^-1 sum_j b_j H_j. The source phase norm is the Euclidean L2 product WithLp2, not the default product max norm.
Mathematical proof
1. Use the genuine cardinal-integral parents
The compiled coefficient constructor supplies t_j in[0,h], the endpoint t_last=h, Lambda≥1, row absolute-integral bounds and sum b_j=h. The independent positive-weight theorem gives every b_j≥0. The endpoint c_j is exactly the last omega row. From h^2 Lambda≤1 and Lambda≥1 derive h≤1. No convenient coefficient or regularity certificates are assumed.
Corresponding Lean step
chebyshev_lobatto_coefficients; nonnegative_momentum_weights; hcoeff; hc; hh1
2. Construct the real numerical phase and Gaussian kernel
Continuity of the genuine gradient follows from C2 and the continuous Riesz identification. Finite actual Picard sums and both OU half-refreshes therefore make Phi jointly measurable. Push forward Kernel.id product Kernel.const Gamma; the two independent Gaussian coordinates are actual inputs of this same map. The law is exactly Gamma.map Phi_z. This is K with deterministic gradient f, not stochastic Khat or the conditional-mean Kbar.
Corresponding Lean step
hg; hPhi; K; Kernel.IsMarkovKernel.map; Measure.dirac_prod; Measure.map_map
3. Bound the actual first Picard error
Use the canonical Hessian-secant constructor at each Y0 pair, deriving the global gradient Lipschitz bound. Common Gaussian noise cancels, giving DeltaY0_j=Delta x+a t_j Delta p. Writing D=||Delta x||+||Delta p||, the actual E_i=-sum omega_ij Delta gradient_j has norm≤h^2 Lambda D/2. Since h^2 Lambda≤1, the loose bound ||DeltaY1_i||≤2D holds. All helpers are private algebra of this same source algorithm, with no separate proof credit.
Corresponding Lean step
secant_data; first_picard_error; hd0; herr; hpic
4. Produce the source integral average H
At each actual Y1 pair call the compiled genuine Hessian-secant theorem. It produces symmetry, all-vector inherited curvature and norm≤1. Form H=h^-1 sum b_j H_j using the real ordinary-cardinal integrals. Positive b_j and sum b_j=h preserve both diagonal bounds and symmetry; the operator triangle bound gives norm≤1. The source H is this exact integral average, not an arbitrary matrix satisfying the desired result.
Corresponding Lean step
S; actual_averaged_hessian; hessian_secant_operator; hb; hbs; hHd
5. Expand both real endpoint residuals with explicit constants
The exact endpoint differences are Delta x+ah Delta p-sum c_j H_j DeltaY1_j and a^2 Delta p-a sum b_j H_j DeltaY1_j. The scalar exponential inequalities give |1-a|≤h/2 and |a^2-1+h|≤h^2. Let e=h^2 Lambda/2. The position residual has norm≤h^2||Delta p||/2+h^2 Lambda D. The momentum residual has norm≤h^2||Delta p||+h^2||Delta x||/2+h(h||Delta p||+eD). With h≤1 and Lambda≥1 their sum is ≤4h^2 Lambda D (in particular bounds 3/2 and 5/2 times h^2 Lambda D). These are actual residuals, not hypotheses.
Corresponding Lean step
refresh_scalar_bounds; Real.abs_exp_sub_one_sub_id_le; endpoint_error; hG; hGn; hvector; hsum
6. Use the source Euclidean phase norm
The L2 product norm satisfies ||(rx,rp)||2≤||rx||+||rp|| and each coordinate norm is ≤||(Delta x,Delta p)||2. Hence D≤2||Delta0||2, giving actual residual norm≤8 Lambda h^2||Delta0||2. This avoids using the default max norm as if it were the Euclidean norm.
Corresponding Lean step
norm_add_le; WithLp.norm_toLp_fst; WithLp.norm_toLp_snd; WithLp.norm_fst_le; WithLp.norm_snd_le; hr
7. Construct the pointwise linear remainder
If Delta0=0, the derived residual bound forces r=0 and R=0 works. Otherwise define Rw=inner(Delta0,w) r/||Delta0||^2 using Mathlib rankOne. It satisfies R Delta0=r; its operator norm is ≤||r||/||Delta0||≤8 Lambda h^2. This explicitly elaborates the source existential remainder and omitted universal constant. It is not a differentiability/Jacobian claim or a measurable operator-choice claim.
Corresponding Lean step
rankOne_apply; norm_rankOne; ContinuousLinearMap.opNorm_smul_le; hRd; zero difference branch
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · source_first_order_difference
Genuine coefficient/positive-weight/Bochner-Hessian parents, finite actual gradient/Picard expansion, exponential remainder, Euclidean residual estimate, rankOne remainder and genuine Gaussian Markov pushforward.
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_first_order_difference {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 ^ 2 * Λ ≤ 1 →
let a := Real.exp (-h / 2)
let sigma := Real.sqrt (1 - Real.exp (-h))
let Γ := (stdGaussian E).prod (stdGaussian E)
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)
Measurable Φ ∧
(∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
∀ z, K z = Γ.map (fun ζ => Φ (z, ζ))) ∧
∀ z z' ζ : E × E,
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)
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 ∧
WithLp.toLp 2 ((Φ (z,ζ)).1 - (Φ (z',ζ)).1,
(Φ (z,ζ)).2 - (Φ (z',ζ)).2) =
d + h • WithLp.toLp 2 (z.2-z'.2, -H (z.1-z'.1)-(z.2-z'.2)) + R d := 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^2*Λ ≤ 1 at hstep
have hcoeff := TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficients hJ hh
change (∀ i, t i ∈ Icc 0 h) ∧ Function.Injective t ∧
t ⟨J-1,by omega⟩ = h ∧
(∀ i j, (ell i).eval (t j) = if i=j then 1 else 0) ∧
(∀ s : ℝ, ∑ j : Fin J, (ell j).eval s = 1) ∧
1 ≤ Λ ∧
(∀ i, (∑ j : Fin J, |ω i j|) ≤ (t i)^2/2*Λ ∧
(∑ j : Fin J, |ω i j|) ≤ h^2/2*Λ) ∧ (∑ j : Fin J, b j) = h at hcoeff
rcases hcoeff with ⟨ht, _, hlast, _, _, hΛ, hw, hbs⟩
have hb : ∀ j, 0 ≤ b j :=
TechnicalLemmas.Analysis.ChebyshevLobattoPositiveWeights.nonnegative_momentum_weights hJ hh
have hc : ∑ j, |c j| ≤ h^2*Λ/2 := by
have hr := (hw ⟨J-1,by omega⟩).2
change ∑ j, |∫ s in 0..t ⟨J-1,by omega⟩, (t ⟨J-1,by omega⟩-s)*(ell j).eval s|
≤ h^2/2*Λ at hr
rw [hlast] at hr
simpa only [c, div_mul_eq_mul_div] using hr
have hh1 : h ≤ 1 := by
have hsq : h^2 ≤ 1 := by nlinarith [sq_nonneg h]
nlinarith
let a := Real.exp (-h / 2)
let sigma := Real.sqrt (1 - Real.exp (-h))
let Γ := (stdGaussian E).prod (stdGaussian E)
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)
change Measurable Φ ∧ (∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
∀ z, K z = Γ.map (fun ζ => Φ (z,ζ))) ∧ _
have hg : Measurable (gradient f) := by
unfold gradient
exact ((InnerProductSpace.toDual ℝ E).symm.continuous.comp
(hf.continuous_fderiv (by norm_num))).measurable
have hΦ : Measurable Φ := by
dsimp only [Φ, Y1, Y0, P0]
fun_prop
let K := (Kernel.id ×ₖ Kernel.const (E × E) Γ).map Φ
have hK : IsMarkovKernel K := Kernel.IsMarkovKernel.map _ hΦ
refine ⟨hΦ, ⟨K,hK,fun 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 z z' ζ
let H := h⁻¹ • ∑ j, b j • S f (Y1 z ζ j) (Y1 z' ζ j)
let d := WithLp.toLp 2 (z.1-z'.1,z.2-z'.2)
let A := WithLp.toLp 2 (z.2-z'.2,-H (z.1-z'.1)-(z.2-z'.2))
let q := WithLp.toLp 2 ((Φ (z,ζ)).1-(Φ (z',ζ)).1,(Φ (z,ζ)).2-(Φ (z',ζ)).2)
let r := q - (d + h • A)
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 • A+R d
have hHd := actual_averaged_hessian hκ hf hH hJ hh (Y1 z ζ) (Y1 z' ζ)
change H.toLinearMap.IsSymmetric ∧ (∀ v, (1/(2*κ))*‖v‖^2 ≤ inner ℝ (H v) v ∧
inner ℝ (H v) v ≤ ‖v‖^2) ∧ ‖H‖ ≤ 1 at hHd
have hr : ‖r‖ ≤ 8*Λ*h^2*‖d‖ := by
exact endpoint_error hκ hf hH hh hh1 hΛ hstep t ω b c ht
(fun i => by simpa only [div_mul_eq_mul_div] using (hw i).2)
hb hbs hc z z' (sigma • ζ.1) (sigma • ζ.2)
refine ⟨hHd.1, hHd.2.1, hHd.2.2, ?_⟩
by_cases hd : d = 0
· have hr0 : r = 0 := norm_eq_zero.mp (by simpa [hd] using hr)
refine ⟨0, ?_, ?_⟩
· simpa only [ContinuousLinearMap.opNorm_zero] using (show (0:ℝ) ≤ 8*Λ*h^2 from by positivity)
simp only [zero_apply, add_zero]
exact sub_eq_zero.mp hr0
· have hn : 0 < ‖d‖ := norm_pos_iff.mpr hd
let R : WithLp 2 (E × E) →L[ℝ] WithLp 2 (E × E) :=
(‖d‖^2)⁻¹ • InnerProductSpace.rankOne ℝ r d
have hRd : R d = r := by
simp only [R, smul_apply, InnerProductSpace.rankOne_apply,
real_inner_self_eq_norm_sq, smul_smul]
rw [inv_mul_cancel₀ (by positivity : ‖d‖^2 ≠ 0), one_smul]
refine ⟨R, ?_, ?_⟩
· calc
‖R‖ ≤ ‖(‖d‖^2)⁻¹‖ * ‖InnerProductSpace.rankOne ℝ r d‖ := ContinuousLinearMap.opNorm_smul_le _ _
_ = ‖r‖/‖d‖ := by
rw [Real.norm_eq_abs, abs_of_pos (by positivity), InnerProductSpace.norm_rankOne]
field_simp
_ ≤ 8*Λ*h^2 := (div_le_iff₀ hn).mpr hr
· rw [hRd]
dsimp only [r]
abel
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FirstOrderDifferenceScope and omitted-condition boundaries
- This is the actual deterministic numerical kernel/first-order difference interface in Lemma4.6, conditional on the explicitly exposed normalized C2 curvature producer. The identity f=V_eta and source Lemma4.1 smoothing/curvature production remain open. It does not prove Proposition4.7 contraction/step absorption, Lemma4.8 M_kappa increment, logarithmic Lambda/B2, Khat/Kbar accuracy, invariance, repeated-history/cost, PBPS, either complete main theorem or their actual-input expected-cost composition. Khat and Kbar cannot be replaced by this K; TV closeness cannot transfer unbounded cost.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficientsAutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoPositiveWeights.nonnegative_momentum_weightsAutoSamplingTheory.TechnicalLemmas.Analysis.HessianSecantOperator.hessian_secant_operator
Mathlib API called (external library)
- ContDiff.continuous_fderiv
- Kernel.IsMarkovKernel.map
- Measure.dirac_prod
- Measure.map_map
- Real.add_one_le_exp
- Real.abs_exp_sub_one_sub_id_le
- norm_add_le
- WithLp.norm_toLp_fst
- WithLp.norm_toLp_snd
- WithLp.norm_fst_le
- WithLp.norm_snd_le
- InnerProductSpace.rankOne_apply
- InnerProductSpace.norm_rankOne
- ContinuousLinearMap.opNorm_smul_le
Mathematical sources
- SPHMC Lemma4.6 actual numerical phase — This is the actual deterministic numerical kernel/first-order difference interface in Lemma4.6, conditional on the explicitly exposed normalized C2 curvature producer. The identity f=V_eta and source Lemma4.1 smoothing/curvature production remain open. It does not prove Proposition4.7 contraction/step absorption, Lemma4.8 M_kappa increment, logarithmic Lambda/B2, Khat/Kbar accuracy, invariance, repeated-history/cost, PBPS, either complete main theorem or their actual-input expected-cost composition. Khat and Kbar cannot be replaced by this K; TV closeness cannot 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.