Both actual Picard query layers under the full phase law
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ImplementedPhaseWork.implemented_phase_query_moments_and_work · theorem · Teaching coverage
Mathematical statement
For the full independent driving law gamma=(Gaussian zeta0 product Gaussian zeta1) product (Gaussian array G0 product Gaussian array G1), and mu=nu product gamma, set a=exp(-h/2), sigma=sqrt(1-exp(-h)), MR=M+(1-exp(-h))*d, B=6MR+3eps^2+3eta*d and C=2+(1+log((1-c)^(-1)))/(-log c), d=finrank(E). There exist the same measurable exact proximal map p, actual stopped output q and natural index N, with p(y)+eta grad V(p(y))=y, ||q(y)-p(y)||≤eps and run(grad V,eta,eps,y,N(y)+1,y)=some(q(y),N(y)+1) for every y. Define P0=aP+sigma zeta0, Y0_i=X+t_i P0, Z0_j=grad V(q(Y0_j)+sqrt(eta) G0_j), Y1_i=Y0_i-sum_j omega_ij Z0_j, Z1_j=grad V(q(Y1_j)+sqrt(eta) G1_j), and Phi=(X+h P0-sum_j positionWeight_j Z1_j, a(P0-sum_j momentumWeight_j Z1_j)+sigma zeta1). Phi is measurable and gives a Markov kernel K(s)=gamma.map(z → Phi(s,z)). For every i both gradient squares are integrable, with E_mu||grad V(Y0_i)||^2≤2MR and E_mu||grad V(Y1_i)||^2≤4MR+2S^2 B. Both actual counts N(Y0_i)+1 and N(Y1_i)+1 are integrable; their respective expectations are at most C[1+log(1+sqrt(2MR)/eps)] and C[1+log(1+sqrt(4MR+2S^2 B)/eps)].
Lean statement · implemented_phase_query_moments_and_work
Exact supplied parameters, full product law and same actual witnesses are explicit in the compiled theorem.
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 implemented_phase_query_moments_and_work {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 (E × E)) [IsProbabilityMeasure ν]
(xstar : E) (hstar : gradient V xstar = 0)
{h M S : ℝ} (hh : 0 ≤ h) (hM : 0 ≤ M) (hS : 0 ≤ S)
(hstateI : Integrable (fun s : E × E => ‖s.1-xstar‖^2 + ‖s.2‖^2) ν)
(hstate : (∫ s : E × E, ‖s.1-xstar‖^2 + ‖s.2‖^2 ∂ν) ≤ M)
(t : ι → ℝ) (ht : ∀ i, |t i| ≤ 1) (omega : ι → ι → ℝ)
(hrow : ∀ i, (∑ j, |omega i j|) ≤ S)
(positionWeight momentumWeight : ι → ℝ) :
let a := Real.exp (-h/2)
let sigma := Real.sqrt (1-Real.exp (-h))
let gi := Measure.pi (fun _ : ι => stdGaussian E)
let γ := ((stdGaussian E).prod (stdGaussian E)).prod (gi.prod gi)
let μ := ν.prod γ
let MR := M + (1-Real.exp (-h)) * (Module.finrank ℝ E : ℝ)
let B := 6*MR + 3*eps^2 + 3*eta*(Module.finrank ℝ E : ℝ)
let C := 2 + (1+Real.log ((1-c)⁻¹))/(-Real.log c)
∃ p q : E → E, ∃ N : E → ℕ,
Measurable p ∧ Measurable q ∧ Measurable N ∧
(∀ y, p y + eta • gradient V (p 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 P0 := fun w : (E × E) × ((E × E) × ((ι → E) × (ι → E))) =>
a • w.1.2 + sigma • w.2.1.1
let Y0 := fun i w => w.1.1 + t i • P0 w
let Z0 := fun j w => gradient V (q (Y0 j w) + Real.sqrt eta • w.2.2.1 j)
let Y1 := fun i w => Y0 i w - ∑ j, omega i j • Z0 j w
let Z1 := fun j w => gradient V (q (Y1 j w) + Real.sqrt eta • w.2.2.2 j)
let Φ := fun w => (w.1.1 + h • P0 w - ∑ j, positionWeight j • Z1 j w,
a • (P0 w - ∑ j, momentumWeight j • Z1 j w) + sigma • w.2.1.2)
Measurable Φ ∧ ∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
(∀ s, K s = γ.map (fun z => Φ (s,z))) ∧
(∀ i, Integrable (fun w => ‖gradient V (Y0 i w)‖^2) μ ∧
(∫ w, ‖gradient V (Y0 i w)‖^2 ∂μ) ≤ 2*MR ∧
Integrable (fun w => (N (Y0 i w) : ℝ)+1) μ ∧
(∫ w, (N (Y0 i w) : ℝ)+1 ∂μ) ≤
C*(1+Real.log (1+Real.sqrt (2*MR)/eps))) ∧
(∀ i, Integrable (fun w => ‖gradient V (Y1 i w)‖^2) μ ∧
(∫ w, ‖gradient V (Y1 i w)‖^2 ∂μ) ≤ 4*MR+2*S^2*B ∧
Integrable (fun w => (N (Y1 i w) : ℝ)+1) μ ∧
(∫ w, (N (Y1 i w) : ℝ)+1 ∂μ) ≤
C*(1+Real.log (1+Real.sqrt (4*MR+2*S^2*B)/eps)))Proof roadmap
- 1Marginalize the full innovation law exactly
Project ((state,(zeta0,zeta1)),(G0,G1)) to ((state,zeta0),G0). Probability-product first-coordinate projections preserve measure. Their product, followed by inverse product association, gives exactly the input law (nu product Gaussian) product Gaussian-array. Thus omitted zeta1 and G1 factors integrate to one; independence is present in the law, not inferred from TV closeness.
- 2Derive the corrected refresh and Gaussian budgets
Apply the compiled input-law theorem to the incoming state law and the first half-refresh. Pull its L2 integrability and bound, and the exact Gaussian coordinate second moments, back along the measure-preserving projection. The refreshed budget is MR, including the positive innovation contribution (1-exp(-h))*d. The proof does not silently reuse M after adding noise.
- 3Identify the successful queries used by both parents
The implemented-phase theorem supplies p,q,N and the complete phase map/kernel. The Picard-center theorem supplies another successful stopped q and N along with its moment conclusions. At every y, deterministic successful-execution uniqueness equates both returned pairs. Projection of that equality and natural-number cancellation identify q and N pointwise, so the center bounds now concern exactly the kernel witnesses. The exact proximal witnesses p need not be identified.
- 4Use both actual Picard-center moments
Apply the existing normalized-Hessian moment theorem under the full actual law using the derived refreshed state budget, full Gaussian G0 coordinates, supplied node bounds and row l1 bound. It gives the first-center bound 2MR, the first queried-gradient bound B, and the second-center bound 4MR+2S^2B. In particular neither actual-center gradient-square integrability nor its numerical bound is a premise.
- 5Bound the same actual query count in each layer
The C2 gradient and all finite phase-center maps are measurable. Apply the same-implementation expected-work theorem to each actual center under mu with the newly derived square-gradient integrability. Its count is N(Y)+1, including the final successful test. Since C≥0 and eps>0, monotonicity of square root and logarithm replaces the actual gradient moment by each derived numerical upper bound. Count integrability is a conclusion, and no different-law cost comparison is used.
- 6Return the same full phase and both per-node costs
Keep the measurable complete phase map and its canonical Gaussian pushforward Markov kernel from the implementation parent, together with the identified witnesses and both moment/work conclusions. The second array G1 and final refresh zeta1 remain in this phase law even though only the first-array marginal is needed to bound its second-layer centers. This does not yet sum executable per-phase gradient queries or iterate the state bound over a run.
Full assumptions and notation
All objects and hypotheses
- E is a complete finite-dimensional real inner-product space with its Borel sigma-algebra; i ranges over a finite index type of size J.
- V is C2, kappa≥1, and kappa^(-1)||v||^2 ≤ D2V(x)[v,v] ≤ ||v||^2 for all x,v. Its actual gradient vanishes at the supplied xstar.
- 0<eta≤c<1, eps>0, h≥0, M≥0, S≥0. The incoming probability law nu on (X,P) has integrable ||X-xstar||^2+||P||^2, with integral at most M.
- The supplied deterministic nodes satisfy |t_i|≤1 and each supplied omega row satisfies sum_j |omega_ij|≤S. Position and momentum weights are arbitrary supplied real arrays; source Chebyshev quadrature is not instantiated.
Mathematical proof
1. Marginalize the full innovation law exactly
Project ((state,(zeta0,zeta1)),(G0,G1)) to ((state,zeta0),G0). Probability-product first-coordinate projections preserve measure. Their product, followed by inverse product association, gives exactly the input law (nu product Gaussian) product Gaussian-array. Thus omitted zeta1 and G1 factors integrate to one; independence is present in the law, not inferred from TV closeness.
Corresponding Lean step
first_input_projection_preserving; measurePreserving_fst; MeasurePreserving.prod; measurePreserving_prodAssoc
2. Derive the corrected refresh and Gaussian budgets
Apply the compiled input-law theorem to the incoming state law and the first half-refresh. Pull its L2 integrability and bound, and the exact Gaussian coordinate second moments, back along the measure-preserving projection. The refreshed budget is MR, including the positive innovation contribution (1-exp(-h))*d. The proof does not silently reuse M after adding noise.
Corresponding Lean step
PicardInputLaw.partial_refresh_with_picard_innovations; MeasurePreserving.integrable_comp_of_integrable; integral_map
3. Identify the successful queries used by both parents
The implemented-phase theorem supplies p,q,N and the complete phase map/kernel. The Picard-center theorem supplies another successful stopped q and N along with its moment conclusions. At every y, deterministic successful-execution uniqueness equates both returned pairs. Projection of that equality and natural-number cancellation identify q and N pointwise, so the center bounds now concern exactly the kernel witnesses. The exact proximal witnesses p need not be identified.
Corresponding Lean step
ProximalExecutionIdentity.successful_query_unique; congrArg Prod.fst; congrArg Prod.snd; Nat.add_right_cancel
4. Use both actual Picard-center moments
Apply the existing normalized-Hessian moment theorem under the full actual law using the derived refreshed state budget, full Gaussian G0 coordinates, supplied node bounds and row l1 bound. It gives the first-center bound 2MR, the first queried-gradient bound B, and the second-center bound 4MR+2S^2B. In particular neither actual-center gradient-square integrability nor its numerical bound is a premise.
Corresponding Lean step
PicardCenterMoment.picard_center_gradient_moment
5. Bound the same actual query count in each layer
The C2 gradient and all finite phase-center maps are measurable. Apply the same-implementation expected-work theorem to each actual center under mu with the newly derived square-gradient integrability. Its count is N(Y)+1, including the final successful test. Since C≥0 and eps>0, monotonicity of square root and logarithm replaces the actual gradient moment by each derived numerical upper bound. Count integrability is a conclusion, and no different-law cost comparison is used.
Corresponding Lean step
RealizedProximalWork.realized_proximal_expected_work; Real.log_le_log; mul_le_mul_of_nonneg_left; gcongr
6. Return the same full phase and both per-node costs
Keep the measurable complete phase map and its canonical Gaussian pushforward Markov kernel from the implementation parent, together with the identified witnesses and both moment/work conclusions. The second array G1 and final refresh zeta1 remain in this phase law even though only the first-array marginal is needed to bound its second-layer centers. This does not yet sum executable per-phase gradient queries or iterate the state bound over a run.
Corresponding Lean step
ImplementedPhaseKernel.implemented_phase_kernel; implemented_phase_query_moments_and_work
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · implemented_phase_query_moments_and_work
The authored steps explain the entire current module, including the measure-preserving marginal helper where present.
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 implemented_phase_query_moments_and_work {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 (E × E)) [IsProbabilityMeasure ν]
(xstar : E) (hstar : gradient V xstar = 0)
{h M S : ℝ} (hh : 0 ≤ h) (hM : 0 ≤ M) (hS : 0 ≤ S)
(hstateI : Integrable (fun s : E × E => ‖s.1-xstar‖^2 + ‖s.2‖^2) ν)
(hstate : (∫ s : E × E, ‖s.1-xstar‖^2 + ‖s.2‖^2 ∂ν) ≤ M)
(t : ι → ℝ) (ht : ∀ i, |t i| ≤ 1) (omega : ι → ι → ℝ)
(hrow : ∀ i, (∑ j, |omega i j|) ≤ S)
(positionWeight momentumWeight : ι → ℝ) :
let a := Real.exp (-h/2)
let sigma := Real.sqrt (1-Real.exp (-h))
let gi := Measure.pi (fun _ : ι => stdGaussian E)
let γ := ((stdGaussian E).prod (stdGaussian E)).prod (gi.prod gi)
let μ := ν.prod γ
let MR := M + (1-Real.exp (-h)) * (Module.finrank ℝ E : ℝ)
let B := 6*MR + 3*eps^2 + 3*eta*(Module.finrank ℝ E : ℝ)
let C := 2 + (1+Real.log ((1-c)⁻¹))/(-Real.log c)
∃ p q : E → E, ∃ N : E → ℕ,
Measurable p ∧ Measurable q ∧ Measurable N ∧
(∀ y, p y + eta • gradient V (p 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 P0 := fun w : (E × E) × ((E × E) × ((ι → E) × (ι → E))) =>
a • w.1.2 + sigma • w.2.1.1
let Y0 := fun i w => w.1.1 + t i • P0 w
let Z0 := fun j w => gradient V (q (Y0 j w) + Real.sqrt eta • w.2.2.1 j)
let Y1 := fun i w => Y0 i w - ∑ j, omega i j • Z0 j w
let Z1 := fun j w => gradient V (q (Y1 j w) + Real.sqrt eta • w.2.2.2 j)
let Φ := fun w => (w.1.1 + h • P0 w - ∑ j, positionWeight j • Z1 j w,
a • (P0 w - ∑ j, momentumWeight j • Z1 j w) + sigma • w.2.1.2)
Measurable Φ ∧ ∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
(∀ s, K s = γ.map (fun z => Φ (s,z))) ∧
(∀ i, Integrable (fun w => ‖gradient V (Y0 i w)‖^2) μ ∧
(∫ w, ‖gradient V (Y0 i w)‖^2 ∂μ) ≤ 2*MR ∧
Integrable (fun w => (N (Y0 i w) : ℝ)+1) μ ∧
(∫ w, (N (Y0 i w) : ℝ)+1 ∂μ) ≤
C*(1+Real.log (1+Real.sqrt (2*MR)/eps))) ∧
(∀ i, Integrable (fun w => ‖gradient V (Y1 i w)‖^2) μ ∧
(∫ w, ‖gradient V (Y1 i w)‖^2 ∂μ) ≤ 4*MR+2*S^2*B ∧
Integrable (fun w => (N (Y1 i w) : ℝ)+1) μ ∧
(∫ w, (N (Y1 i w) : ℝ)+1 ∂μ) ≤
C*(1+Real.log (1+Real.sqrt (4*MR+2*S^2*B)/eps))) := by
classical
dsimp only
let gi := Measure.pi (fun _ : ι => stdGaussian E)
let γ := ((stdGaussian E).prod (stdGaussian E)).prod (gi.prod gi)
let μ := ν.prod γ
let μ0 := (ν.prod (stdGaussian E)).prod gi
let proj := fun w : (E × E) × ((E × E) × ((ι → E) × (ι → E))) =>
((w.1,w.2.1.1),w.2.2.1)
have hproj : MeasurePreserving proj μ μ0 :=
first_input_projection_preserving ν (stdGaussian E)
obtain ⟨hMR,hX0,hP0,hsI0,hs0,hG0,hGI0,hGint0⟩ :=
PicardInputLaw.partial_refresh_with_picard_innovations (ι := ι) ν xstar hh hM hstateI hstate
let X := fun w : (E × E) × ((E × E) × ((ι → E) × (ι → E))) => w.1.1
let P := fun w : (E × E) × ((E × E) × ((ι → E) × (ι → E))) =>
Real.exp (-h/2) • w.1.2 + Real.sqrt (1-Real.exp (-h)) • w.2.1.1
let G := fun (j : ι) (w : (E × E) × ((E × E) × ((ι → E) × (ι → E)))) =>
w.2.2.1 j
have hsI : Integrable (fun w => ‖X w-xstar‖^2 + ‖P w‖^2) μ :=
hproj.integrable_comp_of_integrable hsI0
have hs : (∫ w, ‖X w-xstar‖^2 + ‖P w‖^2 ∂μ) ≤
M + (1-Real.exp (-h))*(Module.finrank ℝ E : ℝ) := by
calc
_ = ∫ u : ((E × E) × E) × (ι → E), ‖u.1.1.1-xstar‖^2 +
‖Real.exp (-h/2) • u.1.1.2 + Real.sqrt (1-Real.exp (-h)) • u.1.2‖^2 ∂μ0 := by
rw [← hproj.map_eq, integral_map hproj.measurable.aemeasurable (by fun_prop)]
_ ≤ _ := hs0
have hGI (j) : Integrable (fun w => ‖G j w‖^2) μ :=
hproj.integrable_comp_of_integrable (hGI0 j)
have hGint (j) : (∫ w, ‖G j w‖^2 ∂μ) ≤ (Module.finrank ℝ E : ℝ) := by
calc
_ = ∫ u : ((E × E) × E) × (ι → E), ‖u.2 j‖^2 ∂μ0 := by
rw [← hproj.map_eq, integral_map hproj.measurable.aemeasurable (by fun_prop)]
_ ≤ _ := le_of_eq (hGint0 j)
obtain ⟨p,q,N,hp,hq,hN,hall,hphase⟩ :=
ImplementedPhaseKernel.implemented_phase_kernel hκ hV hH heta hec hc heps h hh
t omega positionWeight momentumWeight
obtain ⟨p',N',q',hp',hN',hq',hfix',hrun',hm0,hz0,hm1⟩ :=
PicardCenterMoment.picard_center_gradient_moment hκ hV hH heta hec hc heps μ
X P (by fun_prop) (by fun_prop) xstar hstar t ht G (fun _ => by fun_prop)
omega hMR hS hsI hs hGI hGint hrow
have hid (y) := ProximalExecutionIdentity.successful_query_unique
(gradient V) eta eps y (hall y).2.2 (hrun' y).2
have hqeq : q = q' := funext fun y => congrArg Prod.fst (hid y)
have hNeq : N = N' := funext fun y => Nat.add_right_cancel (congrArg Prod.snd (hid y))
subst q'
subst N'
obtain ⟨hvar,hΦ,K,hK,hKlaw⟩ := hphase
have hg : Measurable (gradient V) := by
unfold gradient
exact ((InnerProductSpace.toDual ℝ E).symm.continuous.comp
(hV.continuous_fderiv (by norm_num))).measurable
have hC : 0 ≤ 2+(1+Real.log ((1-c)⁻¹))/(-Real.log c) := by
have hcp := heta.trans_le hec
have hd : 0 < 1-c := sub_pos.mpr hc
have hi : 1 ≤ (1-c)⁻¹ := (one_le_inv₀ hd).mpr (by linarith)
have hl := Real.log_nonneg hi
have ha := neg_pos.mpr (Real.log_neg hcp hc)
positivity
refine ⟨p,q,N,hp,hq,hN,hall,hΦ,K,hK,hKlaw,?_,?_⟩
· intro i
obtain ⟨hcI,hcB⟩ := RealizedProximalWork.realized_proximal_expected_work μ
hκ hV hH heta hec hc heps q N (fun y => (hall y).2.2)
(fun w => X w+t i • P w) (by fun_prop) (hm0 i).1
refine ⟨(hm0 i).1,(hm0 i).2,hcI,hcB.trans ?_⟩
apply mul_le_mul_of_nonneg_left _ hC
apply add_le_add_right
apply Real.log_le_log (by positivity)
gcongr
exact (hm0 i).2
· intro i
obtain ⟨hcI,hcB⟩ := RealizedProximalWork.realized_proximal_expected_work μ
hκ hV hH heta hec hc heps q N (fun y => (hall y).2.2)
(fun w => X w+t i • P w - ∑ j, omega i j •
gradient V (q (X w+t j • P w) + Real.sqrt eta • G j w))
(by fun_prop) (hm1 i).1
refine ⟨(hm1 i).1,(hm1 i).2,hcI,hcB.trans ?_⟩
apply mul_le_mul_of_nonneg_left _ hC
apply add_le_add_right
apply Real.log_le_log (by positivity)
gcongr
exact (hm1 i).2
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ImplementedPhaseWorkScope and omitted-condition boundaries
- Single actual phase with arbitrary incoming L2 state budget and supplied bounded finite nodes/rows. Same q/N in the full Gaussian phase kernel, both center moments and both actual per-node query costs. No query-center gradient moment or count integrability/cost hypothesis. The run-wide D.7 induction, source quadrature/step selection, full-array direct/proximal execution aggregation D.8, Wp/proxy-warmness, initialization and main results remain separate; no TV-to-unbounded-cost transfer.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ImplementedPhaseKernel.implemented_phase_kernelAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PicardInputLaw.partial_refresh_with_picard_innovationsAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PicardCenterMoment.picard_center_gradient_momentAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalExecutionIdentity.successful_query_uniqueAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RealizedProximalWork.realized_proximal_expected_work
Mathlib API called (external library)
- MeasureTheory.measurePreserving_fst
- MeasureTheory.MeasurePreserving.prod
- MeasureTheory.measurePreserving_prodAssoc
- MeasureTheory.integral_map
- Real.log_le_log
Mathematical sources
- Chen–Chewi–Lu–Zhang, stopped routine and actual Picard query centers — Single actual phase with arbitrary incoming L2 state budget and supplied bounded finite nodes/rows. Same q/N in the full Gaussian phase kernel, both center moments and both actual per-node query costs. No query-center gradient moment or count integrability/cost hypothesis. The run-wide D.7 induction, source quadrature/step selection, full-array direct/proximal execution aggregation D.8, Wp/proxy-warmness, initialization and main results remain separate; no TV-to-unbounded-cost transfer.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.