Counted phase work
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.CountedPhaseProgram.implemented_phase_expected_query_work · theorem · Teaching coverage
Mathematical statement
Under mu=nu product ((Gaussian product Gaussian) product (Gaussian Fin-m array product Gaussian Fin-m array)), set d=finrank(E), a=exp(-h/2), sigma=sqrt(1-exp(-h)), MR=M+(1-exp(-h))*d, B=6MR+3eps^2+3eta*d, C=2+(1+log((1-c)^(-1)))/(-log c), L0=C[1+log(1+sqrt(2MR)/eps)], L1=C[1+log(1+sqrt(4MR+2S^2B)/eps)]. There exist measurable p,q,N with exact proximal equation, ||q(y)-p(y)||≤eps and successful proximalQuery from y with fuel N(y)+1 returning (q(y),N(y)+1) for every y. 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), Phi=(X+hP0-sum_j positionWeight_j Z1_j, a(P0-sum_j momentumWeight_j Z1_j)+sigma zeta1). The same Phi is measurable and defines the Gaussian pushforward Markov kernel. The count T=2*m+sum_i[(N(Y0_i)+1)+(N(Y1_i)+1)] is measurable. For every driving input w, phaseQuery with fuel(y)=N(y)+1 returns exactly some(Phi(w),T(w)); the real cast of T is integrable under mu and E_mu T≤m*(2+L0+L1).
Lean statement · implemented_phase_expected_query_work
Exact finite arrays, full input/return types, parameters and counting boundary are retained in Lean.
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_expected_query_work {m : ℕ} {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 : Fin m → ℝ) (ht : ∀ i, |t i| ≤ 1) (omega : Fin m → Fin m → ℝ)
(hrow : ∀ i, (∑ j, |omega i j|) ≤ S)
(positionWeight momentumWeight : Fin m → ℝ) :
let a := Real.exp (-h/2)
let sigma := Real.sqrt (1-Real.exp (-h))
let gi := Measure.pi (fun _ : Fin m => 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)
let L0 := C*(1+Real.log (1+Real.sqrt (2*MR)/eps))
let L1 := C*(1+Real.log (1+Real.sqrt (4*MR+2*S^2*B)/eps))
∃ 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) × ((Fin m → E) × (Fin m → 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)
let T := fun w => 2*m+∑ i, ((N (Y0 i w)+1)+(N (Y1 i w)+1))
Measurable Φ ∧ Measurable T ∧
(∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
∀ s, K s = γ.map (fun z => Φ (s,z))) ∧
(∀ w, phaseQuery (gradient V) eta eps h t omega positionWeight momentumWeight
(fun y => N y+1) w = some (Φ w,T w)) ∧
Integrable (fun w => (T w : ℝ)) μ ∧
(∫ w, (T w : ℝ) ∂μ) ≤ (m : ℝ)*(2+L0+L1)Proof roadmap
- 1Execute a finite successful query array
Induct on the finite array size. The empty array returns count zero. For a nonempty array, execute index zero, then the tail, returning the actual vector of outputs and the sum of their returned counts. Fin.cons reconstruction and Fin.sum_univ_succ identify the complete returned vector and count. This helper has no probabilistic or termination premise beyond the individual successful calls.
- 2Run the actual two-layer program
For each first center, run the residual-stopped proximal interpreter and evaluate the Gaussian-shifted gradient of its returned point, adding one direct query. Construct the second centers using these actual first returned gradients; run the second array in the same manner. Form the full updated state including both half-refreshes from the second returned gradients. In both layers each proximal count N(Y)+1 already includes its terminal successful residual test. Thus the returned count is the sum of both arrays plus exactly 2*m direct gradient evaluations. Failed insufficient-fuel calls return none.
- 3Use one actual full-law witness
The existing full-phase moments/work theorem supplies the same measurable p,q,N, full phase map and kernel, with both count integrabilities and the bounds L0,L1 under mu. No center moment, count-integrability or expected-query bound is introduced as a new premise. The execution identity applies its global successful proximal runs directly, with certified fuel N(y)+1.
- 4Prove measurable and integrable total actual cost
The C2 gradient is measurable, as are the stopped q/N and finite center maps. Therefore the natural count T is measurable. Cast the finite natural sum to the reals. Its constant part is integrable under the full probability law; each first- and second-layer count has L1 integrability supplied by the actual-law parent, so finite addition proves L1 integrability of the actual program count.
- 5Integrate and sum the actual query bounds
Use integral_add and integral_finsetSum only after establishing their integrability hypotheses. For each index the two count expectations add to at most L0+L1. Summing over Fin m gives m*(L0+L1); probability normalization makes the constant contribution exactly 2*m. Ring arithmetic yields m*(2+L0+L1). All inputs and costs use the same full Gaussian law.
Full assumptions and notation
All objects and hypotheses
- E is a complete finite-dimensional real inner-product space with Borel sigma-algebra; the actual array index is Fin m for supplied natural m, not silently the source 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. Execute a finite successful query array
Induct on the finite array size. The empty array returns count zero. For a nonempty array, execute index zero, then the tail, returning the actual vector of outputs and the sum of their returned counts. Fin.cons reconstruction and Fin.sum_univ_succ identify the complete returned vector and count. This helper has no probabilistic or termination premise beyond the individual successful calls.
Corresponding Lean step
collectQueries; collectQueries_some
2. Run the actual two-layer program
For each first center, run the residual-stopped proximal interpreter and evaluate the Gaussian-shifted gradient of its returned point, adding one direct query. Construct the second centers using these actual first returned gradients; run the second array in the same manner. Form the full updated state including both half-refreshes from the second returned gradients. In both layers each proximal count N(Y)+1 already includes its terminal successful residual test. Thus the returned count is the sum of both arrays plus exactly 2*m direct gradient evaluations. Failed insufficient-fuel calls return none.
Corresponding Lean step
phaseQuery; phaseQuery_success; Finset.sum_add_distrib
3. Use one actual full-law witness
The existing full-phase moments/work theorem supplies the same measurable p,q,N, full phase map and kernel, with both count integrabilities and the bounds L0,L1 under mu. No center moment, count-integrability or expected-query bound is introduced as a new premise. The execution identity applies its global successful proximal runs directly, with certified fuel N(y)+1.
Corresponding Lean step
ImplementedPhaseWork.implemented_phase_query_moments_and_work; phaseQuery_success
4. Prove measurable and integrable total actual cost
The C2 gradient is measurable, as are the stopped q/N and finite center maps. Therefore the natural count T is measurable. Cast the finite natural sum to the reals. Its constant part is integrable under the full probability law; each first- and second-layer count has L1 integrability supplied by the actual-law parent, so finite addition proves L1 integrability of the actual program count.
Corresponding Lean step
fun_prop; Nat.cast_sum; integrable_finsetSum; Integrable.add
5. Integrate and sum the actual query bounds
Use integral_add and integral_finsetSum only after establishing their integrability hypotheses. For each index the two count expectations add to at most L0+L1. Summing over Fin m gives m*(L0+L1); probability normalization makes the constant contribution exactly 2*m. Ring arithmetic yields m*(2+L0+L1). All inputs and costs use the same full Gaussian law.
Corresponding Lean step
integral_add; integral_finsetSum; Finset.sum_le_sum; probReal_univ; ring
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · implemented_phase_expected_query_work
The proof steps cover both private execution helpers and the public actual-law total-cost theorem. The definition itself is an execution prerequisite, not a proof edge.
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_expected_query_work {m : ℕ} {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 : Fin m → ℝ) (ht : ∀ i, |t i| ≤ 1) (omega : Fin m → Fin m → ℝ)
(hrow : ∀ i, (∑ j, |omega i j|) ≤ S)
(positionWeight momentumWeight : Fin m → ℝ) :
let a := Real.exp (-h/2)
let sigma := Real.sqrt (1-Real.exp (-h))
let gi := Measure.pi (fun _ : Fin m => 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)
let L0 := C*(1+Real.log (1+Real.sqrt (2*MR)/eps))
let L1 := C*(1+Real.log (1+Real.sqrt (4*MR+2*S^2*B)/eps))
∃ 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) × ((Fin m → E) × (Fin m → 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)
let T := fun w => 2*m+∑ i, ((N (Y0 i w)+1)+(N (Y1 i w)+1))
Measurable Φ ∧ Measurable T ∧
(∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
∀ s, K s = γ.map (fun z => Φ (s,z))) ∧
(∀ w, phaseQuery (gradient V) eta eps h t omega positionWeight momentumWeight
(fun y => N y+1) w = some (Φ w,T w)) ∧
Integrable (fun w => (T w : ℝ)) μ ∧
(∫ w, (T w : ℝ) ∂μ) ≤ (m : ℝ)*(2+L0+L1) := by
classical
dsimp only
let gi := Measure.pi (fun _ : Fin m => 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)
let L0 := C*(1+Real.log (1+Real.sqrt (2*MR)/eps))
let L1 := C*(1+Real.log (1+Real.sqrt (4*MR+2*S^2*B)/eps))
obtain ⟨p,q,N,hp,hq,hN,hall,hΦ,K,hK,hKlaw,hw0,hw1⟩ :=
ImplementedPhaseWork.implemented_phase_query_moments_and_work hκ hV hH heta hec hc heps
ν xstar hstar hh hM hS hstateI hstate t ht omega hrow positionWeight momentumWeight
let P0 := fun w : (E × E) × ((E × E) × ((Fin m → E) × (Fin m → E))) =>
Real.exp (-h/2) • w.1.2+Real.sqrt (1-Real.exp (-h)) • 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 T := fun w => 2*m+∑ i, ((N (Y0 i w)+1)+(N (Y1 i w)+1))
have hg : Measurable (gradient V) := by
unfold gradient
exact ((InnerProductSpace.toDual ℝ E).symm.continuous.comp
(hV.continuous_fderiv (by norm_num))).measurable
have hTm : Measurable T := by fun_prop
have hi0 (i : Fin m) : Integrable (fun w => (N (Y0 i w) : ℝ)+1) μ :=
(hw0 i).2.2.1
have hi1 (i : Fin m) : Integrable (fun w => (N (Y1 i w) : ℝ)+1) μ :=
(hw1 i).2.2.1
have hsum : Integrable (fun w => ∑ i, (((N (Y0 i w) : ℝ)+1)+
((N (Y1 i w) : ℝ)+1))) μ :=
integrable_finsetSum Finset.univ (fun i _ => (hi0 i).add (hi1 i))
have hTex : (fun w => (T w : ℝ)) = fun w => 2*(m : ℝ)+
∑ i, (((N (Y0 i w) : ℝ)+1)+((N (Y1 i w) : ℝ)+1)) := by
funext w
simp only [T, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat, Nat.cast_sum, Nat.cast_one]
have hTi : Integrable (fun w => (T w : ℝ)) μ := by
rw [hTex]
exact (integrable_const (2*(m : ℝ))).add hsum
refine ⟨p,q,N,hp,hq,hN,hall,hΦ,hTm,⟨K,hK,hKlaw⟩,?_,hTi,?_⟩
· intro w
exact phaseQuery_success (gradient V) q N (fun y => N y+1) eta eps h t omega
positionWeight momentumWeight (fun y => (hall y).2.2) w
· change (∫ w, (T w : ℝ) ∂μ) ≤ (m : ℝ)*(2+L0+L1)
rw [hTex, integral_add (integrable_const _) hsum]
rw [integral_finsetSum (f := fun i w => ((N (Y0 i w) : ℝ)+1)+
((N (Y1 i w) : ℝ)+1)) Finset.univ (fun i _ => (hi0 i).add (hi1 i))]
have hb : (∑ i : Fin m, ∫ w, (((N (Y0 i w) : ℝ)+1)+
((N (Y1 i w) : ℝ)+1)) ∂μ) ≤ ∑ _i : Fin m, (L0+L1) := by
apply Finset.sum_le_sum
intro i _
rw [integral_add (hi0 i) (hi1 i)]
exact add_le_add (hw0 i).2.2.2 (hw1 i).2.2.2
calc
_ ≤ (∫ _w, 2*(m : ℝ) ∂μ)+∑ _i : Fin m, (L0+L1) := add_le_add_right hb _
_ = (m : ℝ)*(2+L0+L1) := by
simp [integral_const, Finset.sum_const, nsmul_eq_mul]
ring
end ExpectedWork
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.CountedPhaseProgramScope and omitted-condition boundaries
- Single full Gaussian phase with supplied incoming integrable state L2 budget, finite bounded nodes and row l1 bounds; actual successful exact-real interpreter output and total gradient count. Sufficient finite fuel certifies execution and is not a runtime precomputation or a count/cost hypothesis. No cost claim for failed insufficient-fuel executions. Gaussian sampling and arithmetic are not gradient queries. Source quadrature/J adapter, run-wide D7 induction, D8 parameter/iteration substitution, Wp, proxy-warmness, initialization, PBPS and composition/main results remain open. No TV-to-unbounded-cost transfer.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ImplementedPhaseWork.implemented_phase_query_moments_and_workAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.CountedPhaseProgram.phaseQuery
Mathlib API called (external library)
- Fin.sum_univ_succ
- MeasureTheory.integrable_finsetSum
- MeasureTheory.integral_finsetSum
- MeasureTheory.probReal_univ
Mathematical sources
- SPHMC actual two-layer phase queries — Single full Gaussian phase with supplied incoming integrable state L2 budget, finite bounded nodes and row l1 bounds; actual successful exact-real interpreter output and total gradient count. Sufficient finite fuel certifies execution and is not a runtime precomputation or a count/cost hypothesis. No cost claim for failed insufficient-fuel executions. Gaussian sampling and arithmetic are not gradient queries. Source quadrature/J adapter, run-wide D7 induction, D8 parameter/iteration substitution, Wp, proxy-warmness, initialization, PBPS and composition/main results remain open. 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.