Second moments through the two Picard query layers
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PicardCenterMoment.picard_center_gradient_moment · theorem · Teaching coverage
Mathematical statement
Define the first Picard centers Y⁰_i=X+t_iP₀. The actual stopped gradient-descent proximal program constructs measurable exact proximal points p, stopping indices N and returned points q, with p(y)+eta∇V(p(y))=y, ‖q(y)−p(y)‖≤eps and an exact finite-interpreter return equation. Define Z⁰_j=∇V(q(Y⁰_j)+sqrt(eta)G_j) and Y¹_i=Y⁰_i−Σ_j omega_ij Z⁰_j. Then all three displayed squared-gradient fields are integrable and obey the following explicit bounds. Center moments are established internally as the dominators, but are not separate public conclusions.
Lean statement · picard_center_gradient_moment
The adjacent declaration exposes every probability, regularity, integrability, row-sum and actual-execution hypothesis. Its existential p,N,q are the witnesses constructed by the stopped proximal interpreter, not an abstract oracle.
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 picard_center_gradient_moment {V : E → ℝ} {κ : ℝ≥0}
(hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E, (κ : ℝ)⁻¹ * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
(fderiv ℝ (fderiv ℝ V) x v) v ≤ ‖v‖ ^ 2)
{eta c eps : ℝ} (heta : 0 < eta) (hec : eta ≤ c) (hc : c < 1) (heps : 0 < eps)
(μ : Measure Ω) [IsProbabilityMeasure μ]
(X P : Ω → E) (hX : Measurable X) (hP : Measurable P)
(xstar : E) (hstar : gradient V xstar = 0)
(t : ι → ℝ) (ht : ∀ i, |t i| ≤ 1)
(G : ι → Ω → E) (hG : ∀ j, Measurable (G j))
(omega : ι → ι → ℝ) {M S : ℝ} (hM : 0 ≤ M) (hS : 0 ≤ S)
(hstateI : Integrable (fun w => ‖X w - xstar‖ ^ 2 + ‖P w‖ ^ 2) μ)
(hstate : MeasureTheory.integral μ
(fun w => ‖X w - xstar‖ ^ 2 + ‖P w‖ ^ 2) ≤ M)
(hnoiseI : ∀ j, Integrable (fun w => ‖G j w‖ ^ 2) μ)
(hnoise : ∀ j, MeasureTheory.integral μ (fun w => ‖G j w‖ ^ 2) ≤
(Module.finrank ℝ E : ℝ))
(hrow : ∀ i, (∑ j, |omega i j|) ≤ S) :
let Y0 := fun i w => X w + t i • P w
let B := 6 * M + 3 * eps ^ 2 + 3 * eta * (Module.finrank ℝ E : ℝ)
∃ p : E → E, ∃ N : E → ℕ, ∃ q : E → E,
Measurable p ∧ Measurable N ∧ Measurable q ∧
(∀ y, p y + eta • gradient V (p y) = y) ∧
(∀ y, ‖q y - p y‖ ≤ eps ∧
ApproximateProximalExecution.proximalQuery (gradient V) eta eps y (N y + 1) y =
some (q y, N y + 1)) ∧
let Z0 := fun j w => gradient V (q (Y0 j w) + Real.sqrt eta • G j w)
let Y1 := fun i w => Y0 i w - ∑ j, omega i j • Z0 j w
(∀ i, Integrable (fun w => ‖gradient V (Y0 i w)‖ ^ 2) μ ∧
MeasureTheory.integral μ (fun w => ‖gradient V (Y0 i w)‖ ^ 2) ≤ 2 * M) ∧
(∀ j, Integrable (fun w => ‖Z0 j w‖ ^ 2) μ ∧
MeasureTheory.integral μ (fun w => ‖Z0 j w‖ ^ 2) ≤ B) ∧
(∀ i, Integrable (fun w => ‖gradient V (Y1 i w)‖ ^ 2) μ ∧
MeasureTheory.integral μ (fun w => ‖gradient V (Y1 i w)‖ ^ 2) ≤
4 * M + 2 * S ^ 2 * B)Proof roadmap
- 1Control the first centers
Because |t_i|≤1, expanding Y⁰_i−x*=(X−x*)+t_iP and using (a+b)²≤2a²+2b² gives an integrable pointwise dominator. The state premise can therefore be integrated before any gradient estimate is used.
- 2Use genuine smoothness to control gradients
The upper Hessian bound and C² regularity yield a genuinely 1-Lipschitz gradient. Since ∇V(x*)=0, the gradient norm is bounded by distance to x*. This also supplies measurability, so domination gives integrability rather than merely a numerical inequality.
- 3Relate the actual approximate query to the exact prox
The existing execution theorem returns the actual finite stopped iterate q together with ‖q−p‖≤eps. The exact proximal map p is nonexpansive: subtract its two optimality equations and pair with p(y)−p(z); monotonicity of ∇V makes the extra term nonnegative. As x* solves its own proximal equation, p(x*)=x*.
- 4Bound every random proximal-gradient query
Apply the 1-Lipschitz gradient estimate after adding sqrt(eta)G_j, then use (a+b+c)²≤3(a²+b²+c²). Only the marginal second moment of G_j enters, so no independence or joint Gaussian construction is needed here.
- 5Propagate through the weighted second layer
A weighted Cauchy–Schwarz inequality bounds the square of the finite update by its absolute row sum times the correspondingly weighted query moments. Integrating and using Σ_j|omega_ij|≤S yields S²B. Combining this update with the first-center bound, then using the gradient-distance inequality once more, gives the layer-1 result.
Full assumptions and notation
All objects and hypotheses
- E is a finite-dimensional complete real inner-product space with its Borel sigma algebra. V:E→R is C², kappa≥1, and kappa⁻¹‖v‖²≤D²V(x)[v,v]≤‖v‖² for every x,v.
- On an arbitrary probability space, X and the post-refresh momentum P₀ used by Algorithm 3.1 are measurable and E[‖X−x*‖²+‖P₀‖²]≤M, with the integrability stated separately. A future adapter must derive this from the repeated-chain state estimate and the refresh step. The point x* is a genuine minimizer witness through ∇V(x*)=0.
- The finite node family satisfies |t_i|≤1. Each innovation G_j is measurable, has integrable squared norm and E‖G_j‖²≤dim(E). Independence between nodes, X, P and G is not required for this edge.
- The integrated interpolation weights satisfy Σ_j|omega_ij|≤S. The step parameters obey 0<eta≤c<1 and eps>0, so the existing finite stopped proximal program applies.
Mathematical proof
1. Control the first centers
Because |t_i|≤1, expanding Y⁰_i−x*=(X−x*)+t_iP and using (a+b)²≤2a²+2b² gives an integrable pointwise dominator. The state premise can therefore be integrated before any gradient estimate is used.
Corresponding Lean step
hY0bound, hY0I and hY0int establish the pointwise inequality, Bochner integrability and integral bound in that order.
2. Use genuine smoothness to control gradients
The upper Hessian bound and C² regularity yield a genuinely 1-Lipschitz gradient. Since ∇V(x*)=0, the gradient norm is bounded by distance to x*. This also supplies measurability, so domination gives integrability rather than merely a numerical inequality.
Corresponding Lean step
The shared quadratic-regularization theorem produces hLip; hgrad, hgradI and hgradInt apply it without treating totalized fderiv as differentiability.
3. Relate the actual approximate query to the exact prox
The existing execution theorem returns the actual finite stopped iterate q together with ‖q−p‖≤eps. The exact proximal map p is nonexpansive: subtract its two optimality equations and pair with p(y)−p(z); monotonicity of ∇V makes the extra term nonnegative. As x* solves its own proximal equation, p(x*)=x*.
Corresponding Lean step
hpLip and hpstar are proved from hall and strong-convex gradient monotonicity. The theorem deliberately does not call the older eta≤1/2 Lipschitz wrapper, because D.7 only assumes 0<eta≤c<1.
4. Bound every random proximal-gradient query
Apply the 1-Lipschitz gradient estimate after adding sqrt(eta)G_j, then use (a+b+c)²≤3(a²+b²+c²). Only the marginal second moment of G_j enters, so no independence or joint Gaussian construction is needed here.
Corresponding Lean step
hZbound gives the pointwise estimate; hZdomI and hZI make the integrability obligation explicit; hZint integrates it using the probability normalization.
5. Propagate through the weighted second layer
A weighted Cauchy–Schwarz inequality bounds the square of the finite update by its absolute row sum times the correspondingly weighted query moments. Integrating and using Σ_j|omega_ij|≤S yields S²B. Combining this update with the first-center bound, then using the gradient-distance inequality once more, gives the layer-1 result.
Corresponding Lean step
weighted_sum_norm_sq_le, hweighted, hsumSqI and hsumInt handle the finite sum; hY1I, hY1int and hgrad1I complete the second layer.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · picard_center_gradient_moment
ASTIS supplies the actual stopped program and the C²-to-Lipschitz/strong-convex bridge. Mathlib supplies measurability, Bochner integral domination, finite sums and elementary norm inequalities. Two private algebraic helpers receive no registry leaf credit.
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 picard_center_gradient_moment {V : E → ℝ} {κ : ℝ≥0}
(hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E, (κ : ℝ)⁻¹ * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
(fderiv ℝ (fderiv ℝ V) x v) v ≤ ‖v‖ ^ 2)
{eta c eps : ℝ} (heta : 0 < eta) (hec : eta ≤ c) (hc : c < 1) (heps : 0 < eps)
(μ : Measure Ω) [IsProbabilityMeasure μ]
(X P : Ω → E) (hX : Measurable X) (hP : Measurable P)
(xstar : E) (hstar : gradient V xstar = 0)
(t : ι → ℝ) (ht : ∀ i, |t i| ≤ 1)
(G : ι → Ω → E) (hG : ∀ j, Measurable (G j))
(omega : ι → ι → ℝ) {M S : ℝ} (hM : 0 ≤ M) (hS : 0 ≤ S)
(hstateI : Integrable (fun w => ‖X w - xstar‖ ^ 2 + ‖P w‖ ^ 2) μ)
(hstate : MeasureTheory.integral μ
(fun w => ‖X w - xstar‖ ^ 2 + ‖P w‖ ^ 2) ≤ M)
(hnoiseI : ∀ j, Integrable (fun w => ‖G j w‖ ^ 2) μ)
(hnoise : ∀ j, MeasureTheory.integral μ (fun w => ‖G j w‖ ^ 2) ≤
(Module.finrank ℝ E : ℝ))
(hrow : ∀ i, (∑ j, |omega i j|) ≤ S) :
let Y0 := fun i w => X w + t i • P w
let B := 6 * M + 3 * eps ^ 2 + 3 * eta * (Module.finrank ℝ E : ℝ)
∃ p : E → E, ∃ N : E → ℕ, ∃ q : E → E,
Measurable p ∧ Measurable N ∧ Measurable q ∧
(∀ y, p y + eta • gradient V (p y) = y) ∧
(∀ y, ‖q y - p y‖ ≤ eps ∧
ApproximateProximalExecution.proximalQuery (gradient V) eta eps y (N y + 1) y =
some (q y, N y + 1)) ∧
let Z0 := fun j w => gradient V (q (Y0 j w) + Real.sqrt eta • G j w)
let Y1 := fun i w => Y0 i w - ∑ j, omega i j • Z0 j w
(∀ i, Integrable (fun w => ‖gradient V (Y0 i w)‖ ^ 2) μ ∧
MeasureTheory.integral μ (fun w => ‖gradient V (Y0 i w)‖ ^ 2) ≤ 2 * M) ∧
(∀ j, Integrable (fun w => ‖Z0 j w‖ ^ 2) μ ∧
MeasureTheory.integral μ (fun w => ‖Z0 j w‖ ^ 2) ≤ B) ∧
(∀ i, Integrable (fun w => ‖gradient V (Y1 i w)‖ ^ 2) μ ∧
MeasureTheory.integral μ (fun w => ‖gradient V (Y1 i w)‖ ^ 2) ≤
4 * M + 2 * S ^ 2 * B) := by
classical
dsimp only
obtain ⟨p, N, hp, hN, hq, hall⟩ :=
ApproximateProximalExecution.approximate_proximal_execution
hκ hV hH heta hec hc heps
let q := fun y => (fun x : E => y - eta • gradient V x)^[N y] y
have hq' : Measurable q := by simpa only [q] using hq
have hH' : ∀ x v : E, ((κ⁻¹ : ℝ≥0) : ℝ) * ‖v‖ ^ 2 ≤
(fderiv ℝ (fderiv ℝ V) x v) v ∧
(fderiv ℝ (fderiv ℝ V) x v) v ≤ (1 : ℝ≥0) * ‖v‖ ^ 2 := by
simpa only [NNReal.coe_inv, NNReal.coe_one, one_mul] using hH
have hreg :=
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
(r := 0) hV hH' (0 : E)
have hLip : LipschitzWith 1 (gradient V) := by simpa using hreg.2
have hsc : StrongConvexOn Set.univ ((κ : ℝ)⁻¹) V := by simpa using hreg.1
have hmono (x y : E) : 0 ≤ inner ℝ (gradient V x - gradient V y) (x - y) := by
have hb :=
AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn
hsc (fun z _ => (hV.differentiable (by norm_num) z).hasGradientAt)
(x := y) (y := x) (Set.mem_univ _) (Set.mem_univ _)
exact (mul_nonneg (inv_nonneg.mpr (NNReal.coe_nonneg κ)) (sq_nonneg _)).trans hb
have hpLip : LipschitzWith 1 p := by
apply LipschitzWith.of_dist_le_mul
intro y z
simp only [NNReal.coe_one, one_mul, dist_eq_norm]
have he : y - z = (p y - p z) + eta • (gradient V (p y) - gradient V (p z)) := by
calc
y - z = (p y + eta • gradient V (p y)) -
(p z + eta • gradient V (p z)) :=
congrArg₂ (fun a b : E => a - b) (hall y).1.symm (hall z).1.symm
_ = _ := by module
have hpair : ‖p y - p z‖ ^ 2 ≤ inner ℝ (y - z) (p y - p z) := by
calc
_ ≤ ‖p y - p z‖ ^ 2 +
eta * inner ℝ (gradient V (p y) - gradient V (p z)) (p y - p z) :=
le_add_of_nonneg_right (mul_nonneg heta.le (hmono (p y) (p z)))
_ = inner ℝ (y - z) (p y - p z) := by
conv_rhs => rw [he]
rw [inner_add_left, real_inner_smul_left, real_inner_self_eq_norm_sq]
have hb := hpair.trans (real_inner_le_norm (y - z) (p y - p z))
by_cases hz : ‖p y - p z‖ = 0
· simpa only [hz] using norm_nonneg (y - z)
· have hp : 0 < ‖p y - p z‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hz)
nlinarith
have hpstar : p xstar = xstar := by
have he := (hall xstar).1
have hm := hmono (p xstar) xstar
have hEq : p xstar - xstar = -eta • (gradient V (p xstar) - gradient V xstar) := by
calc
p xstar - xstar = p xstar - (p xstar + eta • gradient V (p xstar)) :=
congrArg (fun z => p xstar - z) he.symm
_ = -eta • (gradient V (p xstar) - gradient V xstar) := by
rw [hstar, sub_zero]
module
have hsq : ‖p xstar - xstar‖ ^ 2 =
-eta * inner ℝ (gradient V (p xstar) - gradient V xstar)
(p xstar - xstar) := by
calc
_ = inner ℝ (p xstar - xstar) (p xstar - xstar) :=
(real_inner_self_eq_norm_sq _).symm
_ = inner ℝ (-eta • (gradient V (p xstar) - gradient V xstar))
(p xstar - xstar) := by rw [hEq]
_ = _ := by rw [real_inner_smul_left]
have hz : ‖p xstar - xstar‖ = 0 := by
have hle : ‖p xstar - xstar‖ ^ 2 ≤ 0 := by rw [hsq]; exact mul_nonpos_of_nonpos_of_nonneg (by linarith) hm
nlinarith [sq_nonneg ‖p xstar - xstar‖]
exact sub_eq_zero.mp (norm_eq_zero.mp hz)
have hgrad (y : E) : ‖gradient V y‖ ≤ ‖y - xstar‖ := by
have hh := hLip.dist_le_mul y xstar
simpa only [hstar, sub_zero, NNReal.coe_one, one_mul, dist_eq_norm] using hh
let Y0 := fun i w => X w + t i • P w
have hY0m (i) : Measurable (Y0 i) := hX.add (hP.const_smul (t i))
have hY0bound (i w) : ‖Y0 i w - xstar‖ ^ 2 ≤
2 * (‖X w - xstar‖ ^ 2 + ‖P w‖ ^ 2) := by
have he : Y0 i w - xstar = (X w - xstar) + t i • P w := by dsimp [Y0]; module
rw [he]
have hn := norm_add_le (X w - xstar) (t i • P w)
rw [norm_smul, Real.norm_eq_abs] at hn
have hti := ht i
have hmul : |t i| * ‖P w‖ ≤ ‖P w‖ := by
simpa only [one_mul] using mul_le_mul_of_nonneg_right hti (norm_nonneg _)
have hn' : ‖X w - xstar + t i • P w‖ ≤ ‖X w - xstar‖ + ‖P w‖ :=
hn.trans (add_le_add_right hmul _)
have hnsq := (sq_le_sq₀ (norm_nonneg _) (by positivity)).2 hn'
nlinarith [norm_nonneg (X w - xstar), norm_nonneg (P w),
sq_nonneg (‖X w - xstar‖ - ‖P w‖)]
have hY0I (i) : Integrable (fun w => ‖Y0 i w - xstar‖ ^ 2) μ := by
apply (hstateI.const_mul 2).mono'
(((hY0m i).sub measurable_const).norm.pow_const 2).aestronglyMeasurable
filter_upwards with w
rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
exact hY0bound i w
have hY0int (i) : MeasureTheory.integral μ
(fun w => ‖Y0 i w - xstar‖ ^ 2) ≤ 2 * M := by
calc
_ ≤ MeasureTheory.integral μ
(fun w => 2 * (‖X w - xstar‖ ^ 2 + ‖P w‖ ^ 2)) :=
integral_mono (hY0I i) (hstateI.const_mul 2) (hY0bound i)
_ = 2 * MeasureTheory.integral μ
(fun w => ‖X w - xstar‖ ^ 2 + ‖P w‖ ^ 2) := integral_const_mul 2 _
_ ≤ 2 * M := mul_le_mul_of_nonneg_left hstate (by norm_num)
have hgradI (i) : Integrable (fun w => ‖gradient V (Y0 i w)‖ ^ 2) μ := by
apply (hY0I i).mono'
((hLip.continuous.measurable.comp (hY0m i)).norm.pow_const 2).aestronglyMeasurable
filter_upwards with w
rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
exact (sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).2 (hgrad _)
have hgradInt (i) : MeasureTheory.integral μ
(fun w => ‖gradient V (Y0 i w)‖ ^ 2) ≤ 2 * M := by
exact (integral_mono (hgradI i) (hY0I i) fun w =>
(sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).2 (hgrad _)).trans (hY0int i)
let Z0 := fun j w => gradient V (q (Y0 j w) + Real.sqrt eta • G j w)
have hZ0m (j) : Measurable (Z0 j) := hLip.continuous.measurable.comp
((hq'.comp (hY0m j)).add ((hG j).const_smul (Real.sqrt eta)))
have hqcenter (y : E) : ‖q y - xstar‖ ≤ ‖y - xstar‖ + eps := by
calc
‖q y - xstar‖ ≤ ‖q y - p y‖ + ‖p y - xstar‖ := by
simpa only [sub_add_sub_cancel] using norm_add_le (q y - p y) (p y - xstar)
_ ≤ eps + ‖p y - p xstar‖ := by rw [hpstar]; gcongr; exact (hall y).2.2.2.2.1
_ ≤ eps + ‖y - xstar‖ := by
gcongr
simpa only [NNReal.coe_one, one_mul, dist_eq_norm] using hpLip.dist_le_mul y xstar
_ = ‖y - xstar‖ + eps := add_comm _ _
have hZbound (j w) : ‖Z0 j w‖ ^ 2 ≤
3 * (‖Y0 j w - xstar‖ ^ 2 + eps ^ 2 + eta * ‖G j w‖ ^ 2) := by
have hg0 := hgrad (q (Y0 j w) + Real.sqrt eta • G j w)
have he : q (Y0 j w) + Real.sqrt eta • G j w - xstar =
(q (Y0 j w) - xstar) + Real.sqrt eta • G j w := by abel
have htri : ‖q (Y0 j w) + Real.sqrt eta • G j w - xstar‖ ≤
‖Y0 j w - xstar‖ + eps + Real.sqrt eta * ‖G j w‖ := by
calc
_ ≤ ‖q (Y0 j w) - xstar‖ + ‖Real.sqrt eta • G j w‖ := by
rw [he]
exact norm_add_le _ _
_ ≤ (‖Y0 j w - xstar‖ + eps) + Real.sqrt eta * ‖G j w‖ := by
rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg eta)]
gcongr
exact hqcenter (Y0 j w)
have hsqrt := Real.sq_sqrt heta.le
have hsq : (‖Y0 j w - xstar‖ + eps + Real.sqrt eta * ‖G j w‖) ^ 2 ≤
3 * (‖Y0 j w - xstar‖ ^ 2 + eps ^ 2 + eta * ‖G j w‖ ^ 2) := by
nlinarith [norm_nonneg (Y0 j w - xstar), norm_nonneg (G j w),
Real.sqrt_nonneg eta, sq_nonneg (‖Y0 j w - xstar‖ - eps),
sq_nonneg (‖Y0 j w - xstar‖ - Real.sqrt eta * ‖G j w‖),
sq_nonneg (eps - Real.sqrt eta * ‖G j w‖)]
exact (sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).2 hg0 |>.trans
((sq_le_sq₀ (norm_nonneg _) (by positivity)).2 htri |>.trans hsq)
let B := 6 * M + 3 * eps ^ 2 + 3 * eta * Module.finrank ℝ E
have hB : 0 ≤ B := by positivity
have hZdomI (j) : Integrable (fun w =>
3 * (‖Y0 j w - xstar‖ ^ 2 + eps ^ 2 + eta * ‖G j w‖ ^ 2)) μ := by
exact (((hY0I j).add (integrable_const (eps ^ 2))).add
((hnoiseI j).const_mul eta)).const_mul 3
have hZI (j) : Integrable (fun w => ‖Z0 j w‖ ^ 2) μ := by
apply (hZdomI j).mono' ((hZ0m j).norm.pow_const 2).aestronglyMeasurable
filter_upwards with w
rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
exact hZbound j w
have hZint (j) : MeasureTheory.integral μ (fun w => ‖Z0 j w‖ ^ 2) ≤ B := by
have houter := integral_add ((hY0I j).add (integrable_const (eps ^ 2)))
((hnoiseI j).const_mul eta)
have hinner := integral_add (hY0I j) (integrable_const (eps ^ 2))
calc
_ ≤ MeasureTheory.integral μ (fun w =>
3 * (‖Y0 j w - xstar‖ ^ 2 + eps ^ 2 + eta * ‖G j w‖ ^ 2)) :=
integral_mono (hZI j) (hZdomI j) (hZbound j)
_ = 3 * (MeasureTheory.integral μ (fun w => ‖Y0 j w - xstar‖ ^ 2) + eps ^ 2 +
eta * MeasureTheory.integral μ (fun w => ‖G j w‖ ^ 2)) := by
rw [integral_const_mul 3]
have ho : MeasureTheory.integral μ (fun w =>
(‖Y0 j w - xstar‖ ^ 2 + eps ^ 2) + eta * ‖G j w‖ ^ 2) =
MeasureTheory.integral μ (fun w => ‖Y0 j w - xstar‖ ^ 2 + eps ^ 2) +
MeasureTheory.integral μ (fun w => eta * ‖G j w‖ ^ 2) := by
simpa only [Pi.add_apply] using houter
rw [ho]
have hi : MeasureTheory.integral μ (fun w => ‖Y0 j w - xstar‖ ^ 2 + eps ^ 2) =
MeasureTheory.integral μ (fun w => ‖Y0 j w - xstar‖ ^ 2) +
MeasureTheory.integral μ (fun _w => eps ^ 2) := by
simpa only [Pi.add_apply] using hinner
rw [hi, integral_const, probReal_univ, smul_eq_mul, one_mul, integral_const_mul]
_ ≤ B := by dsimp [B]; nlinarith [hY0int j, hnoise j]
let Y1 := fun i w => Y0 i w - ∑ j, omega i j • Z0 j w
have hsumM (i) : Measurable (fun w => ∑ j, omega i j • Z0 j w) := by fun_prop
have hY1m (i) : Measurable (Y1 i) := (hY0m i).sub (hsumM i)
have hweighted (i w) : ‖∑ j, omega i j • Z0 j w‖ ^ 2 ≤
S * ∑ j, |omega i j| * ‖Z0 j w‖ ^ 2 := by
calc
_ ≤ (∑ j, |omega i j|) * ∑ j, |omega i j| * ‖Z0 j w‖ ^ 2 :=
weighted_sum_norm_sq_le (omega i) (fun j => Z0 j w)
_ ≤ S * ∑ j, |omega i j| * ‖Z0 j w‖ ^ 2 := by
gcongr
exact hrow i
have hsumSqI (i) : Integrable (fun w => ‖∑ j, omega i j • Z0 j w‖ ^ 2) μ := by
have hi : Integrable (fun w => S * ∑ j, |omega i j| * ‖Z0 j w‖ ^ 2) μ :=
(integrable_finsetSum Finset.univ fun j _ => (hZI j).const_mul |omega i j|).const_mul S
apply hi.mono' ((hsumM i).norm.pow_const 2).aestronglyMeasurable
filter_upwards with w
rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
exact hweighted i w
have hsumInt (i) : MeasureTheory.integral μ
(fun w => ‖∑ j, omega i j • Z0 j w‖ ^ 2) ≤ S ^ 2 * B := by
calc
_ ≤ MeasureTheory.integral μ
(fun w => S * ∑ j, |omega i j| * ‖Z0 j w‖ ^ 2) :=
integral_mono (hsumSqI i)
((integrable_finsetSum Finset.univ fun j _ => (hZI j).const_mul |omega i j|).const_mul S)
(hweighted i)
_ = S * ∑ j, |omega i j| *
MeasureTheory.integral μ (fun w => ‖Z0 j w‖ ^ 2) := by
rw [integral_const_mul, integral_finsetSum]
· simp_rw [integral_const_mul]
· intro j _; exact (hZI j).const_mul _
_ ≤ S * ∑ j, |omega i j| * B := by
gcongr with j
exact hZint j
_ ≤ S ^ 2 * B := by
calc
S * ∑ j, |omega i j| * B = S * ((∑ j, |omega i j|) * B) := by
rw [Finset.sum_mul]
_ ≤ S * (S * B) := by gcongr; exact hrow i
_ = S ^ 2 * B := by ring
have hY1I (i) : Integrable (fun w => ‖Y1 i w - xstar‖ ^ 2) μ := by
have hi := ((hY0I i).const_mul 2).add ((hsumSqI i).const_mul 2)
apply hi.mono'
(((hY1m i).sub measurable_const).norm.pow_const 2).aestronglyMeasurable
filter_upwards with w
have he : Y1 i w - xstar = (Y0 i w - xstar) - ∑ j, omega i j • Z0 j w := by
dsimp [Y1]; module
change |‖Y1 i w - xstar‖ ^ 2| ≤
2 * ‖Y0 i w - xstar‖ ^ 2 + 2 * ‖∑ j, omega i j • Z0 j w‖ ^ 2
rw [abs_of_nonneg (sq_nonneg _), he]
exact norm_sub_sq_le_two _ _
have hY1int (i) : MeasureTheory.integral μ
(fun w => ‖Y1 i w - xstar‖ ^ 2) ≤ 4 * M + 2 * S ^ 2 * B := by
calc
_ ≤ MeasureTheory.integral μ (fun w => 2 * ‖Y0 i w - xstar‖ ^ 2 +
2 * ‖∑ j, omega i j • Z0 j w‖ ^ 2) := by
apply integral_mono (hY1I i) (((hY0I i).const_mul 2).add ((hsumSqI i).const_mul 2))
intro w
have he : Y1 i w - xstar = (Y0 i w - xstar) - ∑ j, omega i j • Z0 j w := by
dsimp [Y1]; module
simpa only [Pi.add_apply, he] using
norm_sub_sq_le_two (Y0 i w - xstar) (∑ j, omega i j • Z0 j w)
_ = 2 * MeasureTheory.integral μ (fun w => ‖Y0 i w - xstar‖ ^ 2) +
2 * MeasureTheory.integral μ (fun w => ‖∑ j, omega i j • Z0 j w‖ ^ 2) := by
rw [integral_add, integral_const_mul, integral_const_mul]
exacts [(hY0I i).const_mul 2, (hsumSqI i).const_mul 2]
_ ≤ 4 * M + 2 * S ^ 2 * B := by nlinarith [hY0int i, hsumInt i]
have hgrad1I (i) : Integrable (fun w => ‖gradient V (Y1 i w)‖ ^ 2) μ := by
apply (hY1I i).mono'
((hLip.continuous.measurable.comp (hY1m i)).norm.pow_const 2).aestronglyMeasurable
filter_upwards with w
rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
exact (sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).2 (hgrad _)
refine ⟨p, N, q, hp, hN, hq', fun y => (hall y).1, ?_, ?_, ?_, ?_⟩
· intro y
exact ⟨by simpa only [q] using (hall y).2.2.2.2.1,
by simpa only [q] using (hall y).2.2.2.2.2.2⟩
· exact fun i => ⟨hgradI i, hgradInt i⟩
· exact fun j => ⟨hZI j, hZint j⟩
· intro i
refine ⟨hgrad1I i, ?_⟩
exact (integral_mono (hgrad1I i) (hY1I i) fun w =>
(sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).2 (hgrad _)).trans (hY1int i)
end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PicardCenterMomentSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| The D.7 proof first invokes the run-wide state estimate from D.3 with q=2 and Lemma 4.16, then Algorithm 3.1 refreshes momentum before forming Y⁰. | The realized X and post-refresh P₀ law and its integrable second-moment upper bound M are explicit premises. | source-implicit | This freezes only the subsequent two-layer propagation. Construction of the repeated state law and the refresh-moment adapter remain separate visible obligations; the same constant is not silently reused. |
| The paper uses standard Gaussian innovations in R^d inside Algorithm 3.1. | Each measurable innovation is required only to satisfy integrability and E‖G_j‖²≤finrank(E); no independence is assumed. | generalization | The displayed moment calculation uses no independence. The future kernel/history theorem must separately construct the correct joint Gaussian law. |
| The paper states a universal C and suppresses the elementary two-layer constants. | The conditional theorem records B=6M+3eps²+3eta*d and 4M+2S²B. | source-implicit | These explicit sufficient constants follow from the same triangle/Cauchy–Schwarz route and are intended to be absorbed by the source's universal C after parameter insertion. |
| Algorithm 3.1 calls an approximate proximal routine and then forms its Picard interpolation layers. | The theorem retains the exact finite-fuel interpreter equation and its measurable p,N,q witnesses, while abstracting only the current phase-state variables and finite node/weight data. | source-implicit | The local execution semantics are real; only the repeated kernel/history law and source-specific node construction remain separate. |
| The source works in R^d under normalized strong-convexity and smoothness assumptions. | A finite-dimensional complete real inner-product Borel space and genuine C² Hessian inequalities are used. | generalization | This includes the Euclidean source setting and makes genuine differentiability explicit instead of relying on totalized fderiv. |
Conditional two-layer L2 propagation for one realized phase. The repeated Algorithm 3.1 history law, the source's run-wide W2/state estimate, insertion of eta, eps, d, kappa and L_q, the final C*kappa*d*L_q^18 value, D.8, sampling accuracy and Theorem 5.1 remain unsupported red obligations.
Encoder–denoiser: source-reviewed · equivalent-after-elaboration
Detected semantic differences
- assumptions: Lean explicitly assumes M>=0 and S>=0; M is redundant and S only restricts the vacuous empty-node edge beyond the nonempty source phase. — Independent source review classification: explicit-elaboration; nonblocking.
- domains: The Euclidean Gaussian phase is factored into a coordinate-free finite-dimensional space and marginal innovation moments; the actual Gaussian joint law remains a visible separate obligation. — Independent source review classification: explicit-elaboration; nonblocking.
- quantifiers: Lean exposes globally measurable proximal/stopping witnesses and the exact finite interpreter return implicit in the source's approximate-proximal call. — Independent source review classification: explicit-elaboration; nonblocking.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
Scope and omitted-condition boundaries
- This is the two-layer L2 propagation used inside SPHMC Lemma D.4 equation (D.7), conditional on the separate run-wide phase-state moment bound and the interpolation-weight row bound. It does not construct the repeated Algorithm 3.1 law, prove that state bound, insert the paper's numerical parameters, prove total work (D.8), or prove Theorem 5.1.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution.approximate_proximal_executionAutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadraticAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn
Mathlib API called (external library)
- LipschitzWith.dist_le_mul
- MeasureTheory.Integrable.mono'
- MeasureTheory.integral_mono
- MeasureTheory.integral_finsetSum
- Finset.sum_sq_le_sum_mul_sum_of_sq_le_mul
- Real.sq_sqrt
Mathematical sources
- Chen–Chewi–Lu–Zhang, SPHMC Lemma D.4 proof of equation (D.7) — Attributed expansion of the layer-0/layer-1 center-moment bookkeeping on lines 2177–2181, not the full lemma.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.