The actual independent Gaussian inputs for the first Picard layer
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PicardInputLaw.partial_refresh_with_picard_innovations · theorem · Teaching coverage
Mathematical statement
On the nested product of the incoming law, a fresh standard Gaussian, and a finite product of standard Gaussians, the refreshed X and P0 and every Picard innovation G_j are measurable and square-integrable with their exact consumer-ready moment bounds.
Lean statement · partial_refresh_with_picard_innovations
The nested lets expose the exact probability law and random variables, while the conjunction returns every measurability and integrability premise required downstream.
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_refresh_with_picard_innovations
(ν : Measure (E × E)) [IsProbabilityMeasure ν]
(xstar : E) {h M : ℝ} (hh : 0 ≤ h) (hM : 0 ≤ M)
(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 μRefresh := ν.prod (stdGaussian E)
let γι := Measure.pi (fun _ : ι => stdGaussian E)
let μ := μRefresh.prod γι
let X : (((E × E) × E) × (ι → E)) → E := fun w => w.1.1.1
let P0 : (((E × E) × E) × (ι → E)) → E :=
fun w => a • w.1.1.2 + sigma • w.1.2
let G : ι → (((E × E) × E) × (ι → E)) → E := fun j w => w.2 j
let BRefresh := M + (1 - Real.exp (-h)) * (Module.finrank ℝ E : ℝ)
0 ≤ BRefresh ∧
Measurable X ∧ Measurable P0 ∧
Integrable (fun w => ‖X w - xstar‖ ^ 2 + ‖P0 w‖ ^ 2) μ ∧
(∫ w, ‖X w - xstar‖ ^ 2 + ‖P0 w‖ ^ 2 ∂μ) ≤ BRefresh ∧
(∀ j, Measurable (G j)) ∧
(∀ j, Integrable (fun w => ‖G j w‖ ^ 2) μ) ∧
(∀ j, (∫ w, ‖G j w‖ ^ 2 ∂μ) = (Module.finrank ℝ E : ℝ))Proof roadmap
- 1Build the probability space
The nested product measure represents freshness of the first refresh Gaussian and the first Picard innovation array.
- 2Reuse the refresh calculation
The previous theorem already proves measurability, integrability, and the corrected OU moment budget; product integration lifts it unchanged over the extra innovation array.
- 3Read each Gaussian coordinate
Evaluation at j is measurable. Finite-product marginal integration returns the original standard Gaussian law, so every coordinate has exactly dimension d as its squared-norm moment.
- 4Feed the real variables to the next theorem
The focused test passes the product-law coordinate projections to the two-layer Picard moment theorem, and separately checks a nondegenerate one-dimensional Gaussian coordinate moment.
Full assumptions and notation
All objects and hypotheses
- The incoming phase-state law is a probability measure with an integrable combined square bounded by M≥0.
- The phase length is nonnegative and the Picard index type is finite.
- E is a complete finite-dimensional real inner-product Borel space.
Mathematical proof
1. Build the probability space
The nested product measure represents freshness of the first refresh Gaussian and the first Picard innovation array.
Corresponding Lean step
Measure.prod constructs the refresh factor and Measure.pi constructs the finite innovation array.
2. Reuse the refresh calculation
The previous theorem already proves measurability, integrability, and the corrected OU moment budget; product integration lifts it unchanged over the extra innovation array.
Corresponding Lean step
Integrable.comp_fst and integral_prod transport the established result.
3. Read each Gaussian coordinate
Evaluation at j is measurable. Finite-product marginal integration returns the original standard Gaussian law, so every coordinate has exactly dimension d as its squared-norm moment.
Corresponding Lean step
integrable_comp_eval and integral_comp_eval are the pinned Mathlib APIs.
4. Feed the real variables to the next theorem
The focused test passes the product-law coordinate projections to the two-layer Picard moment theorem, and separately checks a nondegenerate one-dimensional Gaussian coordinate moment.
Corresponding Lean step
Tests.SmoothedPicardHMCPartialMomentumRefresh checks symbolic API composition in dimension zero and the exact positive-dimensional Gaussian moment in E=R.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · partial_refresh_with_picard_innovations
ASTIS owns the OU refresh and Gaussian norm-square results. Mathlib owns finite product measures, coordinate marginals, and product integration.
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_refresh_with_picard_innovations
(ν : Measure (E × E)) [IsProbabilityMeasure ν]
(xstar : E) {h M : ℝ} (hh : 0 ≤ h) (hM : 0 ≤ M)
(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 μRefresh := ν.prod (stdGaussian E)
let γι := Measure.pi (fun _ : ι => stdGaussian E)
let μ := μRefresh.prod γι
let X : (((E × E) × E) × (ι → E)) → E := fun w => w.1.1.1
let P0 : (((E × E) × E) × (ι → E)) → E :=
fun w => a • w.1.1.2 + sigma • w.1.2
let G : ι → (((E × E) × E) × (ι → E)) → E := fun j w => w.2 j
let BRefresh := M + (1 - Real.exp (-h)) * (Module.finrank ℝ E : ℝ)
0 ≤ BRefresh ∧
Measurable X ∧ Measurable P0 ∧
Integrable (fun w => ‖X w - xstar‖ ^ 2 + ‖P0 w‖ ^ 2) μ ∧
(∫ w, ‖X w - xstar‖ ^ 2 + ‖P0 w‖ ^ 2 ∂μ) ≤ BRefresh ∧
(∀ j, Measurable (G j)) ∧
(∀ j, Integrable (fun w => ‖G j w‖ ^ 2) μ) ∧
(∀ j, (∫ w, ‖G j w‖ ^ 2 ∂μ) = (Module.finrank ℝ E : ℝ)) := by
classical
dsimp only
obtain ⟨hX, hP0, hrefreshI, hrefreshEq, hrefresh⟩ :=
PartialMomentumRefresh.partial_momentum_refresh_second_moment
ν xstar hh hstateI hstate
let μRefresh := ν.prod (stdGaussian E)
let γι := Measure.pi (fun _ : ι => stdGaussian E)
have hvar : 0 ≤ 1 - Real.exp (-h) :=
sub_nonneg.mpr (Real.exp_le_one_iff.mpr (by linarith))
have hB : 0 ≤ M + (1 - Real.exp (-h)) * (Module.finrank ℝ E : ℝ) :=
add_nonneg hM (mul_nonneg hvar (Nat.cast_nonneg _))
have hrefreshOuter : Integrable
(fun w : ((E × E) × E) × (ι → E) =>
‖w.1.1.1 - xstar‖ ^ 2 +
‖Real.exp (-h / 2) • w.1.1.2 +
Real.sqrt (1 - Real.exp (-h)) • w.1.2‖ ^ 2)
(μRefresh.prod γι) := hrefreshI.comp_fst γι
have hrefreshOuterInt :
(∫ w : ((E × E) × E) × (ι → E),
‖w.1.1.1 - xstar‖ ^ 2 +
‖Real.exp (-h / 2) • w.1.1.2 +
Real.sqrt (1 - Real.exp (-h)) • w.1.2‖ ^ 2
∂μRefresh.prod γι) ≤
M + (1 - Real.exp (-h)) * (Module.finrank ℝ E : ℝ) := by
rw [integral_prod _ hrefreshOuter]
simpa [γι, μRefresh] using hrefresh
obtain ⟨hgaussI, hgauss⟩ :=
integrable_norm_sq_and_integral_stdGaussian (E := E)
have hcoordI (j : ι) : Integrable (fun z : ι → E => ‖z j‖ ^ 2) γι :=
by
simpa [γι] using
(integrable_comp_eval (X := fun _ : ι => E)
(μ := fun _ : ι => stdGaussian E) (i := j) hgaussI)
have hcoordOuterI (j : ι) : Integrable
(fun w : ((E × E) × E) × (ι → E) => ‖w.2 j‖ ^ 2)
(μRefresh.prod γι) := (hcoordI j).comp_snd μRefresh
have hcoordOuter (j : ι) :
(∫ w : ((E × E) × E) × (ι → E), ‖w.2 j‖ ^ 2
∂μRefresh.prod γι) = (Module.finrank ℝ E : ℝ) := by
rw [integral_prod _ (hcoordOuterI j)]
simp [μRefresh, γι,
integral_comp_eval (X := fun _ : ι => E) (μ := fun _ : ι => stdGaussian E)
(i := j) hgaussI.aestronglyMeasurable,
hgauss]
exact ⟨hB, by fun_prop, by fun_prop, hrefreshOuter, hrefreshOuterInt,
fun _ => by fun_prop, hcoordOuterI, hcoordOuter⟩
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PicardInputLawSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Algorithm 3.1 says all displayed Gaussian variables are independent. | The first refresh and first innovation array are represented by nested product measures. | same | Product measures make the stated freshness semantic rather than an informal label. |
| Lemma D.4 uses Gaussian second moments without spelling out measurability or integrability. | Every coordinate is proved measurable and square-integrable with exact moment finrank(E). | source-implicit | These conditions are required before the expectations in D.7 are legal. |
| Algorithm 3.1 samples a second array and zeta_1 later in the phase. | This deliberately scoped declaration constructs only the variables consumed by the already-formalized first two query-center layers. | same | It formalizes an exact initial segment of the algorithm; later phase outputs are explicitly separate rather than treated as implicit premises. |
No repeated phase history, D.3/M_kappa adapter, second array, second refresh, quadrature construction, complete D.7, D.8 or theorem result.
Encoder–denoiser: source-reviewed · equivalent-after-elaboration
Detected semantic differences
- assumptions: Nested product measures expose independence, and measurability/integrability legalize the moment calculations. — Independent source review classification: explicit-elaboration; nonblocking.
- scopes: The declaration is an exact conditional initial-segment adapter, not all of Algorithm 3.1 or Lemma D.4. — Independent source review classification: scope-boundary; nonblocking.
- conclusion: Tests separate a positive-dimensional Gaussian coordinate moment from zero-dimensional end-to-end Picard API composition. — Independent source review classification: validation-boundary; nonblocking.
- objects: The source field is explicitly an ASTIS faithful paraphrase rather than a quotation. — Independent source review classification: provenance; 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 constructs the first refresh noise and first finite Picard innovation array. The incoming run-wide moment, second array, second refresh, quadrature data, numerical D.7 and D.8 remain separate.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PartialMomentumRefresh.partial_momentum_refresh_second_momentAutoSamplingTheory.TechnicalLemmas.Probability.StdGaussianMoment.integrable_norm_sq_and_integral_stdGaussian
Mathlib API called (external library)
- MeasureTheory.Measure.pi
- MeasureTheory.integrable_comp_eval
- MeasureTheory.integral_comp_eval
- MeasureTheory.integral_prod
Mathematical sources
- Chen–Chewi–Lu–Zhang, Algorithm 3.1 — Independent zeta_0 and G_j^[0] draws; Lemma D.4 uses their second moments.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.