The actual OU half-refresh and its corrected moment budget
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PartialMomentumRefresh.partial_momentum_refresh_second_moment · theorem · Teaching coverage
Mathematical statement
Set a=exp(−h/2), sigma=sqrt(1−exp(−h)), X0=X and P0=a Pinit+sigma Z on the product law of the incoming state and a fresh standard Gaussian. Then X0 and P0 are measurable, their combined squared distance is integrable, and its expectation satisfies the exact identity and corrected budget below.
Lean statement · partial_momentum_refresh_second_moment
The source's independent Gaussian draw is represented definitionally by a product measure. The conclusion exposes measurability and integrability because the next Picard theorem requires them, and keeps Pinit distinct from the refreshed P0.
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 partial_momentum_refresh_second_moment
(ν : Measure (E × E)) [IsProbabilityMeasure ν]
(xstar : E) {h M : ℝ} (hh : 0 ≤ h)
(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) :
let a := Real.exp (-h / 2)
let sigma := Real.sqrt (1 - Real.exp (-h))
let μ := ν.prod (stdGaussian E)
let X : (E × E) × E → E := fun w => w.1.1
let P0 : (E × E) × E → E := fun w => a • w.1.2 + sigma • w.2
Measurable X ∧ Measurable P0 ∧
Integrable (fun w => ‖X w - xstar‖ ^ 2 + ‖P0 w‖ ^ 2) μ ∧
(∫ w, ‖X w - xstar‖ ^ 2 + ‖P0 w‖ ^ 2 ∂μ) =
(∫ s : E × E, ‖s.1 - xstar‖ ^ 2 + Real.exp (-h) * ‖s.2‖ ^ 2 ∂ν) +
(1 - Real.exp (-h)) * (Module.finrank ℝ E : ℝ) ∧
(∫ w, ‖X w - xstar‖ ^ 2 + ‖P0 w‖ ^ 2 ∂μ) ≤
M + (1 - Real.exp (-h)) * (Module.finrank ℝ E : ℝ)Proof roadmap
- 1Realize the fresh draw by a product law
A sample is a pair ((X,Pinit),Z) distributed according to nu⊗gamma_d. The first coordinate is the incoming phase state and the second is a genuinely fresh standard Gaussian. Coordinate projections and continuous linear combinations make X0 and P0 measurable.
- 2Establish every integrability premise
Nonnegativity lets us extract the position and momentum square integrability from the combined incoming energy. L2 then gives integrability of Pinit itself. The shared ASTIS theorem gives ‖Z‖² in L1, while Mathlib's Gaussian integrability API separately gives Z in L1; together these make the mixed inner product integrable on the product measure.
- 3Use actual independence to kill the cross term
For every fixed incoming momentum, the Gaussian mean is zero. Fubini is legal because the mixed inner product was proved integrable, hence its expectation under the product law vanishes without a centering assumption on Pinit.
- 4Expand the refreshed square
The coefficients satisfy a²=e^(−h) and sigma²=1−e^(−h). Expanding the Hilbert norm, integrating the four integrable terms, using the zero cross term and E‖Z‖²=d gives the exact identity.
- 5Derive the consumer-ready bound
Because h≥0, 0<e^(−h)≤1. Replacing the damped momentum term by the incoming momentum square and applying the input budget yields M+(1−e^(−h))d. The extra dimension term must remain visible until the later paper-parameter absorption step.
Full assumptions and notation
All objects and hypotheses
- The incoming phase-state law nu on E×E is a probability measure, and the combined square ‖X−x*‖²+‖Pinit‖² is integrable with expectation at most M.
- E is a complete finite-dimensional real inner-product Borel space and h≥0.
- Freshness of Z~N(0,I) is represented by the actual product measure nu⊗stdGaussian(E), rather than by assuming the mixed term has expectation zero.
Mathematical proof
1. Realize the fresh draw by a product law
A sample is a pair ((X,Pinit),Z) distributed according to nu⊗gamma_d. The first coordinate is the incoming phase state and the second is a genuinely fresh standard Gaussian. Coordinate projections and continuous linear combinations make X0 and P0 measurable.
Corresponding Lean step
The public X and P0 lets use product projections; the final fun_prop goals prove their measurability.
2. Establish every integrability premise
Nonnegativity lets us extract the position and momentum square integrability from the combined incoming energy. L2 then gives integrability of Pinit itself. The shared ASTIS theorem gives ‖Z‖² in L1, while Mathlib's Gaussian integrability API separately gives Z in L1; together these make the mixed inner product integrable on the product measure.
Corresponding Lean step
hposI, hmomI, hmom1, hgaussI, hz1 and Integrable.op_fst_snd justify Fubini and all subsequent integral algebra.
3. Use actual independence to kill the cross term
For every fixed incoming momentum, the Gaussian mean is zero. Fubini is legal because the mixed inner product was proved integrable, hence its expectation under the product law vanishes without a centering assumption on Pinit.
Corresponding Lean step
integral_strongDual_stdGaussian and integral_prod prove hcross0.
4. Expand the refreshed square
The coefficients satisfy a²=e^(−h) and sigma²=1−e^(−h). Expanding the Hilbert norm, integrating the four integrable terms, using the zero cross term and E‖Z‖²=d gives the exact identity.
Corresponding Lean step
ha2, hs2, hexpand, hpieces and heq mirror this algebra and product integration.
5. Derive the consumer-ready bound
Because h≥0, 0<e^(−h)≤1. Replacing the damped momentum term by the incoming momentum square and applying the input budget yields M+(1−e^(−h))d. The extra dimension term must remain visible until the later paper-parameter absorption step.
Corresponding Lean step
hexp, hweighted and heq prove the final inequality. The focused test passes this result to picard_center_gradient_moment.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · partial_momentum_refresh_second_moment
ASTIS supplies the canonical Gaussian norm-square leaf and the paper-specific product-law adapter. Mathlib supplies product Fubini, Gaussian mean/covariance, Lp-to-integrability and Hilbert norm algebra.
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 partial_momentum_refresh_second_moment
(ν : Measure (E × E)) [IsProbabilityMeasure ν]
(xstar : E) {h M : ℝ} (hh : 0 ≤ h)
(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) :
let a := Real.exp (-h / 2)
let sigma := Real.sqrt (1 - Real.exp (-h))
let μ := ν.prod (stdGaussian E)
let X : (E × E) × E → E := fun w => w.1.1
let P0 : (E × E) × E → E := fun w => a • w.1.2 + sigma • w.2
Measurable X ∧ Measurable P0 ∧
Integrable (fun w => ‖X w - xstar‖ ^ 2 + ‖P0 w‖ ^ 2) μ ∧
(∫ w, ‖X w - xstar‖ ^ 2 + ‖P0 w‖ ^ 2 ∂μ) =
(∫ s : E × E, ‖s.1 - xstar‖ ^ 2 + Real.exp (-h) * ‖s.2‖ ^ 2 ∂ν) +
(1 - Real.exp (-h)) * (Module.finrank ℝ E : ℝ) ∧
(∫ w, ‖X w - xstar‖ ^ 2 + ‖P0 w‖ ^ 2 ∂μ) ≤
M + (1 - Real.exp (-h)) * (Module.finrank ℝ E : ℝ) := by
classical
dsimp only
have hexp : Real.exp (-h) ≤ 1 := Real.exp_le_one_iff.mpr (by linarith)
have hvar : 0 ≤ 1 - Real.exp (-h) := sub_nonneg.mpr hexp
have ha2 : Real.exp (-h / 2) ^ 2 = Real.exp (-h) := by
rw [pow_two, ← Real.exp_add]
congr 1
ring
have hs2 : Real.sqrt (1 - Real.exp (-h)) ^ 2 = 1 - Real.exp (-h) :=
Real.sq_sqrt hvar
have hposI : Integrable (fun s : E × E => ‖s.1 - xstar‖ ^ 2) ν := by
apply hstateI.mono' (by fun_prop)
filter_upwards with s
rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
exact le_add_of_nonneg_right (sq_nonneg _)
have hmomI : Integrable (fun s : E × E => ‖s.2‖ ^ 2) ν := by
apply hstateI.mono' (by fun_prop)
filter_upwards with s
rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
exact le_add_of_nonneg_left (sq_nonneg _)
have hmom1 : Integrable (fun s : E × E => s.2) ν :=
MemLp.integrable (by norm_num : 1 ≤ (2 : ℝ≥0∞))
((memLp_two_iff_integrable_sq_norm (by fun_prop)).2 hmomI)
obtain ⟨hgaussI, hgauss⟩ :=
integrable_norm_sq_and_integral_stdGaussian (E := E)
have hz1 : Integrable (fun z : E => z) (stdGaussian E) := IsGaussian.integrable_id
have hcross : Integrable
(fun w : (E × E) × E => inner ℝ w.1.2 w.2) (ν.prod (stdGaussian E)) :=
hmom1.op_fst_snd (by fun_prop)
⟨1, by intro x y; simpa using norm_inner_le_norm (𝕜 := ℝ) x y⟩ hz1
have hcross0 :
(∫ w : (E × E) × E, inner ℝ w.1.2 w.2 ∂ν.prod (stdGaussian E)) = 0 := by
rw [integral_prod _ hcross]
have hz (s : E × E) :
(∫ z : E, inner ℝ s.2 z ∂stdGaussian E) = 0 :=
integral_strongDual_stdGaussian (innerSL ℝ s.2)
simp only [hz, integral_zero]
have hposP := hposI.comp_fst (stdGaussian E)
have hmomP := hmomI.comp_fst (stdGaussian E)
have hgaussP := hgaussI.comp_snd ν
have hcrossC : Integrable (fun w : (E × E) × E =>
(2 * Real.exp (-h / 2) * Real.sqrt (1 - Real.exp (-h))) *
inner ℝ w.1.2 w.2) (ν.prod (stdGaussian E)) := hcross.const_mul _
have hbase : Integrable (fun w : (E × E) × E =>
‖w.1.1 - xstar‖ ^ 2 + Real.exp (-h) * ‖w.1.2‖ ^ 2)
(ν.prod (stdGaussian E)) := hposP.add (hmomP.const_mul _)
have hbaseCross : Integrable (fun w : (E × E) × E =>
‖w.1.1 - xstar‖ ^ 2 + Real.exp (-h) * ‖w.1.2‖ ^ 2 +
(2 * Real.exp (-h / 2) * Real.sqrt (1 - Real.exp (-h))) *
inner ℝ w.1.2 w.2) (ν.prod (stdGaussian E)) := hbase.add hcrossC
have hnoiseC : Integrable (fun w : (E × E) × E =>
(1 - Real.exp (-h)) * ‖w.2‖ ^ 2) (ν.prod (stdGaussian E)) :=
hgaussP.const_mul _
have hpieces : Integrable (fun w : (E × E) × E =>
‖w.1.1 - xstar‖ ^ 2 + Real.exp (-h) * ‖w.1.2‖ ^ 2 +
(2 * Real.exp (-h / 2) * Real.sqrt (1 - Real.exp (-h))) *
inner ℝ w.1.2 w.2 +
(1 - Real.exp (-h)) * ‖w.2‖ ^ 2) (ν.prod (stdGaussian E)) :=
hbaseCross.add hnoiseC
have hexpand (w : (E × E) × E) :
‖w.1.1 - xstar‖ ^ 2 +
‖Real.exp (-h / 2) • w.1.2 +
Real.sqrt (1 - Real.exp (-h)) • w.2‖ ^ 2 =
‖w.1.1 - xstar‖ ^ 2 + Real.exp (-h) * ‖w.1.2‖ ^ 2 +
(2 * Real.exp (-h / 2) * Real.sqrt (1 - Real.exp (-h))) *
inner ℝ w.1.2 w.2 +
(1 - Real.exp (-h)) * ‖w.2‖ ^ 2 := by
rw [norm_add_sq_real, norm_smul, norm_smul, real_inner_smul_left,
real_inner_smul_right]
rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _),
abs_of_nonneg (Real.sqrt_nonneg _)]
simp only [mul_pow, ha2, hs2]
ring
have houtI : Integrable (fun w : (E × E) × E =>
‖w.1.1 - xstar‖ ^ 2 +
‖Real.exp (-h / 2) • w.1.2 +
Real.sqrt (1 - Real.exp (-h)) • w.2‖ ^ 2)
(ν.prod (stdGaussian E)) := by
simpa only [hexpand] using hpieces
have heq :
(∫ w : (E × E) × E,
‖w.1.1 - xstar‖ ^ 2 +
‖Real.exp (-h / 2) • w.1.2 +
Real.sqrt (1 - Real.exp (-h)) • w.2‖ ^ 2
∂ν.prod (stdGaussian E)) =
(∫ s : E × E,
‖s.1 - xstar‖ ^ 2 + Real.exp (-h) * ‖s.2‖ ^ 2 ∂ν) +
(1 - Real.exp (-h)) * (Module.finrank ℝ E : ℝ) := by
simp_rw [hexpand]
rw [integral_add hbaseCross hnoiseC,
integral_add hbase hcrossC,
integral_const_mul, hcross0, mul_zero, add_zero,
integral_const_mul, integral_prod _ hgaussP]
simp only [hgauss, integral_const]
rw [integral_prod _ hbase]
simp only [integral_const]
simp
have hweighted :
(∫ s : E × E,
‖s.1 - xstar‖ ^ 2 + Real.exp (-h) * ‖s.2‖ ^ 2 ∂ν) ≤ M := by
calc
_ ≤ ∫ s : E × E, ‖s.1 - xstar‖ ^ 2 + ‖s.2‖ ^ 2 ∂ν := by
apply integral_mono (hposI.add (hmomI.const_mul _)) hstateI
intro s
change ‖s.1 - xstar‖ ^ 2 + Real.exp (-h) * ‖s.2‖ ^ 2 ≤
‖s.1 - xstar‖ ^ 2 + ‖s.2‖ ^ 2
have hp : Real.exp (-h) * ‖s.2‖ ^ 2 ≤ ‖s.2‖ ^ 2 := by
simpa only [one_mul] using
mul_le_mul_of_nonneg_right hexp (sq_nonneg ‖s.2‖)
exact add_le_add_right hp (‖s.1 - xstar‖ ^ 2)
_ ≤ M := hstate
refine ⟨by fun_prop, by fun_prop, houtI, heq, ?_⟩
rw [heq]
linarith
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PartialMomentumRefreshSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Algorithm 3.1 draws zeta0 independently of the whole incoming state. | Freshness is represented by the concrete product measure nu.prod(stdGaussian E). | same | The product construction supplies actual independence instead of assuming a zero cross moment. |
| The D.7 proof says the run-wide state estimate also controls layer-one nodes and suppresses this elementary refresh calculation. | The refreshed budget is explicitly M+(1−exp(−h))*finrank(E). | source-implicit | The Gaussian innovation adds this term. Reusing M unchanged is generally false; later universal-constant arithmetic may absorb d only after its own assumptions are present. |
| The source works in R^d. | A complete finite-dimensional real inner-product Borel space is used. | generalization | This contains the Euclidean setting and preserves the norm, Gaussian covariance and dimension calculation. |
| The source's incoming state comes from the repeated Algorithm 3.1 run and D.3/Lemma 4.16. | Its probability law and M-bound are explicit premises. | source-implicit | The history construction and run-wide estimate remain separate visible red obligations rather than being assumed complete. |
One first half-refresh over an abstract incoming state law. No repeated history, derivation of the line-2179 state bound, second refresh, actual Picard Gaussian array, node/weight instantiation, numerical D.7 substitution, D.8 or paper theorem.
Encoder–denoiser: source-reviewed · equivalent-after-elaboration
Detected semantic differences
- assumptions: Freshness and independence are encoded by the concrete product law and structural hypotheses are explicit. — Independent source review classification: explicit-elaboration; nonblocking.
- conclusion: Measurability and refreshed-energy integrability are exposed as supporting conclusions. — Independent source review classification: explicit-elaboration; nonblocking.
- constant_dependencies: The paper's dimension d is resolved as Module.finrank ℝ E. — 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 only Algorithm 3.1's first partial momentum refresh and the adapter needed before the existing two-layer Picard moment theorem. It does not construct the repeated phase history, prove the run-wide state estimate, instantiate the Picard Gaussian array, prove the numerical D.7 bound, aggregate D.8, or prove Theorem 5.1.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- ProbabilityTheory.integral_strongDual_stdGaussian
- MeasureTheory.Integrable.op_fst_snd
- MeasureTheory.integral_prod
- Real.exp_le_one_iff
- InnerProductSpace.norm_add_sq_real
Mathematical sources
- Chen–Chewi–Lu–Zhang, Algorithm 3.1 — First partial momentum refresh at lines 282–300, used in the proof of Lemma D.4 at lines 2177–2180.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.