Expected work of the same implemented query at its realized center
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RealizedProximalWork.realized_proximal_expected_work · theorem · Teaching coverage
Mathematical statement
Attributed implementation/Jensen component of Algorithm D.2 and Lemma D.4, not full D.4. Retain the normalized C2 Hessian bounds, kappa≥1, 0<eta≤c<1 and eps>0. Suppose q:E→E and N:E→Nat satisfy the actual stopped gradient interpreter equation run(grad V,eta,eps,y,N(y)+1,y)=some(q(y),N(y)+1) for every y. For any probability measure mu on an arbitrary measurable space and measurable realized center Y with integrable ||grad V(Y)||^2, the same count N(Y)+1 is integrable and its expectation is at most C_c[1+log(1+sqrt(E_mu||grad V(Y)||^2)/eps)], where C_c=2+(1+log((1-c)^(-1)))/(-log c). Successful interpreter outputs and counts are independent of sufficient fuel; this identifies the supplied implementation with the already compiled expected-work witness before pulling its bound back along Y. No count measurability or integrability is assumed. The actual run-wide moment D.7 and aggregation D.8 are separate.
Lean statement · realized_proximal_expected_work
The exact theorem includes all normalized source assumptions, the successful actual interpreter equation, and the measurable actual-center gradient moment. Count integrability is a conclusion.
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 realized_proximal_expected_work
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{α : Type*} [MeasurableSpace α] (μ : Measure α) [IsProbabilityMeasure μ]
{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)
(q : E → E) (N : E → ℕ)
(hrun : ∀ y, ApproximateProximalExecution.proximalQuery (gradient V) eta eps y
(N y + 1) y = some (q y, N y + 1))
(Y : α → E) (hY : Measurable Y)
(hmoment : Integrable (fun ω => ‖gradient V (Y ω)‖^2) μ) :
Integrable (fun ω => (N (Y ω) : ℝ) + 1) μ ∧
(∫ ω, (N (Y ω) : ℝ) + 1 ∂μ) ≤
(2 + (1 + Real.log ((1-c)⁻¹)) / (-Real.log c)) *
(1 + Real.log (1 + Real.sqrt (∫ ω, ‖gradient V (Y ω)‖^2 ∂μ) / eps))Proof roadmap
- 1Successful executions have identical outputs and query counts
Induct on the first supplied fuel and inspect the other fuel. Zero fuel cannot succeed. At a positive-fuel successful residual test both runs return the same current point with count one. If that test fails, both recurse at the same next iterate, and the induction hypothesis equates the recursive outputs and counts. Both add the same final one.
- 2Use the actual input law
Let nu be the pushforward of mu under Y. Measurability makes nu a probability measure. The C2 potential has continuous gradient; its squared norm is measurable. The pushforward integrability equivalence transfers the supplied actual-center gradient moment to nu.
- 3Identify the implementation with the expected-work witness
The existing expected-work theorem gives a measurable successful count M and its integrable Jensen bound under nu. Compare that successful run at fuel M(y)+1 with the supplied run at N(y)+1, starting at the same y. Equality of the returned pairs implies N(y)+1=M(y)+1, hence N=M pointwise. This derives the needed measurability and integrability for the supplied N, without choosing a new implementation.
- 4Pull the same count back to the realized center
Apply the measurable pushforward identities to the identified count and gradient moment. Integrability of the count under nu pulls back to mu. Both Bochner integrals in the existing exact-constant bound become the corresponding actual-input expectations. No comparison of different probability laws or TV transfer is involved.
Full assumptions and notation
All objects and hypotheses
- E is a complete finite-dimensional real inner-product space with its Borel sigma-algebra; the input space alpha has an arbitrary measurable structure and mu is a probability measure.
- V is C2 and kappa≥1, with kappa^(-1)||v||^2 ≤ D2V(x)[v,v] ≤ ||v||^2 for every x,v.
- 0<eta≤c<1 and eps>0. q and N are arbitrary supplied functions with the successful actual interpreter equation at every y; no count integrability/measurability premise.
- Y is measurable and ||grad V(Y)||^2 is mu-integrable. This is an explicit conditional moment input; the paper run-wide D.7 is not asserted.
Mathematical proof
1. Successful executions have identical outputs and query counts
Induct on the first supplied fuel and inspect the other fuel. Zero fuel cannot succeed. At a positive-fuel successful residual test both runs return the same current point with count one. If that test fails, both recurse at the same next iterate, and the induction hypothesis equates the recursive outputs and counts. Both add the same final one.
Corresponding Lean step
ProximalExecutionIdentity.successful_query_unique; induction on fuel and Option.map_eq_some_iff.
2. Use the actual input law
Let nu be the pushforward of mu under Y. Measurability makes nu a probability measure. The C2 potential has continuous gradient; its squared norm is measurable. The pushforward integrability equivalence transfers the supplied actual-center gradient moment to nu.
Corresponding Lean step
Measure.isProbabilityMeasure_map, integrable_map_measure and integral_map.
3. Identify the implementation with the expected-work witness
The existing expected-work theorem gives a measurable successful count M and its integrable Jensen bound under nu. Compare that successful run at fuel M(y)+1 with the supplied run at N(y)+1, starting at the same y. Equality of the returned pairs implies N(y)+1=M(y)+1, hence N=M pointwise. This derives the needed measurability and integrability for the supplied N, without choosing a new implementation.
Corresponding Lean step
successful_query_unique, congrArg Prod.snd, Nat.add_right_cancel and funext.
4. Pull the same count back to the realized center
Apply the measurable pushforward identities to the identified count and gradient moment. Integrability of the count under nu pulls back to mu. Both Bochner integrals in the existing exact-constant bound become the corresponding actual-input expectations. No comparison of different probability laws or TV transfer is involved.
Corresponding Lean step
integrable_map_measure and integral_map transport the parent bound after pointwise count equality.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · realized_proximal_expected_work
Prove successful-run uniqueness, apply the existing expected-work theorem to the actual pushforward input law, identify the counts pointwise, and pull back the bound.
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 realized_proximal_expected_work
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{α : Type*} [MeasurableSpace α] (μ : Measure α) [IsProbabilityMeasure μ]
{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)
(q : E → E) (N : E → ℕ)
(hrun : ∀ y, ApproximateProximalExecution.proximalQuery (gradient V) eta eps y
(N y + 1) y = some (q y, N y + 1))
(Y : α → E) (hY : Measurable Y)
(hmoment : Integrable (fun ω => ‖gradient V (Y ω)‖^2) μ) :
Integrable (fun ω => (N (Y ω) : ℝ) + 1) μ ∧
(∫ ω, (N (Y ω) : ℝ) + 1 ∂μ) ≤
(2 + (1 + Real.log ((1-c)⁻¹)) / (-Real.log c)) *
(1 + Real.log (1 + Real.sqrt (∫ ω, ‖gradient V (Y ω)‖^2 ∂μ) / eps)) := by
have hg : Continuous (gradient V) := by
unfold gradient
exact (InnerProductSpace.toDual ℝ E).symm.continuous.comp
(hV.continuous_fderiv (by norm_num))
have hgs : Measurable (fun y => ‖gradient V y‖^2) := hg.measurable.norm.pow_const 2
have hm : Integrable (fun y => ‖gradient V y‖^2) (μ.map Y) :=
(integrable_map_measure hgs.aestronglyMeasurable hY.aemeasurable).mpr hmoment
letI : IsProbabilityMeasure (μ.map Y) := Measure.isProbabilityMeasure_map hY.aemeasurable
obtain ⟨p, M, hp, hM, hout, hall, hcount, hbound⟩ :=
ProximalExpectedWork.approximate_proximal_expected_work
hκ hV hH heta hec hc heps (μ.map Y) hm
have hNM : N = M := by
funext y
have h := ProximalExecutionIdentity.successful_query_unique (gradient V) eta eps y (hrun y) (hall y).2.2
exact Nat.add_right_cancel (congrArg Prod.snd h)
subst N
have hcnt : Measurable (fun y => (M y : ℝ) + 1) := by fun_prop
refine ⟨(integrable_map_measure hcnt.aestronglyMeasurable hY.aemeasurable).mp hcount, ?_⟩
simpa only [integral_map hY.aemeasurable hcnt.aestronglyMeasurable,
integral_map hY.aemeasurable hgs.aestronglyMeasurable] using hbound
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RealizedProximalWorkSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| The same gradient-only routine at every realized center, followed by D.3/Jensen. | 0<eta<=c<1 and eps>0. q and N are arbitrary supplied functions with the successful actual interpreter equation at every y; no count integrability/measurability premise. | source-implicit | The successful equation fixes the actual output and count without assuming any cost bound. Deterministic success uniqueness equates separately constructed witnesses. |
| D.4 derives the run-wide center bound D.7 before Jensen. | Y is measurable and ||grad V(Y)||^2 is mu-integrable. This is an explicit conditional moment input; the paper run-wide D.7 is not asserted. | generalization | This closes the same-witness conditional Jensen component. It neither replaces nor proves D.7; the center is the actual measurable map and its moment is explicitly required. |
| Euclidean state and random centers of the sampling routine. | E is a complete finite-dimensional real inner-product space with its Borel sigma-algebra; the input space alpha has an arbitrary measurable structure and mu is a probability measure. | generalization | Finite-dimensional real Hilbert representation and arbitrary measurable input space preserve the same execution/integration argument. |
Same successful stopped query under a measurable actual input with square-integrable gradient. No realized repeated-history D.7 bound, finite-array/run aggregation D.8, quadrature adapter, parameter substitution or main theorem; no TV-to-unbounded-cost transfer.
Encoder–denoiser: source-reviewed · equivalent-after-elaboration
Detected semantic differences
- domains: The expressly scoped component uses finite-dimensional inner-product Borel E and arbitrary measurable input probability spaces instead of only Euclidean sampler centers. — This extension is explicit in the current candidate assumptions and valid for the actual measurable-pushforward proof.
- scopes: The square-gradient moment is an explicit input for the conditional implementation/Jensen component; D.7 and D.8 remain pending. — The source first establishes D.7 and then performs Jensen and aggregation. The current module, lesson scope and obligation list keep these boundaries separate.
- constant_dependencies: The local parent supplies a concrete valid C_c and includes the final successful gradient query; this does not claim the source unspecified constant is optimal. — The exact displayed coefficient is inherited unchanged through count identification and both integral_map identities.
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
- Same successful stopped query under a measurable actual input with square-integrable gradient. No realized repeated-history D.7 bound, finite-array/run aggregation D.8, quadrature adapter, parameter substitution or main theorem; no TV-to-unbounded-cost transfer.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalExpectedWork.approximate_proximal_expected_workAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalExecutionIdentity.successful_query_unique
Mathlib API called (external library)
- Option.map_eq_some_iff
- MeasureTheory.Measure.isProbabilityMeasure_map
- MeasureTheory.integrable_map_measure
- MeasureTheory.integral_map
Mathematical sources
- Chen–Chewi–Lu–Zhang, Algorithm D.2 and D.4 after D.7 — Same successful stopped query under a measurable actual input with square-integrable gradient. No realized repeated-history D.7 bound, finite-array/run aggregation D.8, quadrature adapter, parameter substitution or main theorem; 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.