An RGO of an RGO has an explicit normalized target law
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOClosure.quadratic_tilt_tilt · theorem · Teaching coverage
Mathematical statement
Let E be a real inner-product space with its Borel measurable sets, and let μ be any probability measure on E. For u,y in E, r≥0 and s>0, normalized reweighting first by exp(−r‖x−u‖²/2) and then by exp(−s‖x−y‖²/2) is exactly one normalized reweighting with precision r+s and centre w=(r+s)⁻¹(ru+sy). No moment or density assumption on μ is needed.
Lean statement · quadratic_tilt_tilt
Measure.tilted μ f is Mathlib's actual normalized exponential-density measure. The theorem compares measures, not informal density proportionality. IsProbabilityMeasure μ is a typeclass assumption. u,y and the two precision inequalities are explicit inputs; no integrability hypothesis is hidden in the signature.
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 quadratic_tilt_tilt (μ : Measure E) [IsProbabilityMeasure μ]
{r s : ℝ} (hr : 0 ≤ r) (hs : 0 < s) (u y : E) :
(μ.tilted (fun x => -(r / 2) * ‖x - u‖ ^ 2)).tilted
(fun x => -(s / 2) * ‖x - y‖ ^ 2) =
μ.tilted (fun x => -((r + s) / 2) *
‖x - (r + s)⁻¹ • (r • u + s • y)‖ ^ 2)Proof roadmap
- 1Show each normalized reweighting is a genuine probability law
For every nonnegative precision t and every centre v, the exponential weight is continuous, hence measurable. It is positive and bounded above by one. Since the base measure is a probability, the weight is integrable and its integral is strictly positive. Thus normalization uses a finite positive number, not Lean's fallback value for a nonintegrable expression.
- 2Complete the square with the exact additive constant
Expand each squared norm as an inner product and collect coefficients of x. The weighted centre makes the linear terms agree. The remaining difference is independent of x. Positivity of r+s justifies division, including r=0.
- 3Cancel normalization rather than assuming proportional laws are equal
The normalizer of the second tilt is the integral of its weight under the first normalized law. Multiplying the two normalized densities cancels the first normalizer. Completing the square contributes the same positive factor exp(−C) to numerator and denominator, which cancels as well.
Full assumptions and notation
All objects and hypotheses
- μ is a probability measure, not an unnormalized Lebesgue density. This is an explicit base-law contract, not a proof that the paper's Gibbs potential is normalizable.
- E carries the Borel sigma-algebra of its norm topology and a real inner product. Finite dimension is unnecessary for this algebraic probability-law identity; the source uses Euclidean space.
- The precisions satisfy r≥0 and s>0, so r+s>0. Source A=infinity is represented by r=0; for finite source parameters r=A⁻¹ and s=a⁻¹.
- No derivatives, a.e. choices of conditional distributions, generator domains, moments, boundary decay or sampling-error premises occur in this selected measure calculation.
Mathematical proof
1. Show each normalized reweighting is a genuine probability law
For every nonnegative precision t and every centre v, the exponential weight is continuous, hence measurable. It is positive and bounded above by one. Since the base measure is a probability, the weight is integrable and its integral is strictly positive. Thus normalization uses a finite positive number, not Lean's fallback value for a nonintegrable expression.
Corresponding Lean step
The internal hint proves Integrable from integrable_const 1 and Integrable.mono'. hcont explicitly composes continuous norm, square, multiplication and exponential; hcont.aestronglyMeasurable supplies the measurable representative. Real.exp_le_one_iff checks the bound. Mathlib tilted_tilted and isProbabilityMeasure_tilted use integral_exp_pos for the nonzero normalization.
2. Complete the square with the exact additive constant
Expand each squared norm as an inner product and collect coefficients of x. The weighted centre makes the linear terms agree. The remaining difference is independent of x. Positivity of r+s justifies division, including r=0.
Corresponding Lean step
hsq is the pointwise identity between the sum of two log-weights and the combined log-weight plus c=−C. Inner-product bilinearity expands the squares; field_simp and ring verify the real polynomial identity.
3. Cancel normalization rather than assuming proportional laws are equal
The normalizer of the second tilt is the integral of its weight under the first normalized law. Multiplying the two normalized densities cancels the first normalizer. Completing the square contributes the same positive factor exp(−C) to numerator and denominator, which cancels as well.
Corresponding Lean step
The first tilted_tilted combines normalized exponential tilts. hsq rewrites their sum. A second tilted_tilted presents the additive constant as a constant tilt; tilted_const removes it because the combined law has already been proved a probability.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · quadratic_tilt_tilt
ASTIS authors the quadratic completion and connects it to Mathlib's existing normalization theorem. The source law's Gibbs representation is deliberately not encoded as an assumption equating the two target laws. All weights used in the proof are integrable by direct domination; Mathlib handles their exact normalizer cancellation.
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 quadratic_tilt_tilt (μ : Measure E) [IsProbabilityMeasure μ]
{r s : ℝ} (hr : 0 ≤ r) (hs : 0 < s) (u y : E) :
(μ.tilted (fun x => -(r / 2) * ‖x - u‖ ^ 2)).tilted
(fun x => -(s / 2) * ‖x - y‖ ^ 2) =
μ.tilted (fun x => -((r + s) / 2) *
‖x - (r + s)⁻¹ • (r • u + s • y)‖ ^ 2) := by
have hint : ∀ (t : ℝ), 0 ≤ t → ∀ (v : E),
Integrable (fun x => Real.exp (-(t / 2) * ‖x - v‖ ^ 2)) μ := by
intro t ht v
have hcont : Continuous (fun x : E => Real.exp (-(t / 2) * ‖x - v‖ ^ 2)) :=
Real.continuous_exp.comp (continuous_const.mul ((continuous_id.sub continuous_const).norm.pow 2))
refine (integrable_const (1 : ℝ)).mono' hcont.aestronglyMeasurable ?_
filter_upwards with x
rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
apply Real.exp_le_one_iff.mpr
exact mul_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr (by positivity)) (sq_nonneg _)
have hrs : 0 < r + s := add_pos_of_nonneg_of_pos hr hs
let w : E := (r + s)⁻¹ • (r • u + s • y)
let c : ℝ := -(r * s / (2 * (r + s))) * ‖u - y‖ ^ 2
have hsq : (fun x => -(r / 2) * ‖x - u‖ ^ 2) +
(fun x => -(s / 2) * ‖x - y‖ ^ 2) =
(fun x => -((r + s) / 2) * ‖x - w‖ ^ 2) + (fun _ => c) := by
funext x
simp only [Pi.add_apply, w, c, ← real_inner_self_eq_norm_sq,
inner_sub_left, inner_sub_right, inner_add_left, inner_add_right,
real_inner_smul_left, real_inner_smul_right]
rw [real_inner_comm y u, real_inner_comm u x, real_inner_comm y x]
field_simp
ring
have : IsProbabilityMeasure
(μ.tilted (fun x => -((r + s) / 2) * ‖x - w‖ ^ 2)) :=
isProbabilityMeasure_tilted (hint (r + s) hrs.le w)
rw [tilted_tilted (hint r hr u), hsq,
← tilted_tilted (hint (r + s) hrs.le w), tilted_const]
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOClosureSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Euclidean Gibbs probability base with a C² potential and Hessian bounds | Arbitrary probability measure on a Borel real inner-product space | generalization | Completing the square and exact normalized reweighting do not use density, finite dimension or derivatives. This wider calculus statement does not transfer the source's algorithm or curvature guarantees to arbitrary laws. |
| A∈(0,infinity] and a>0 | r≥0 and s>0, interpreted as r=A⁻¹ and s=a⁻¹ | same | The precision convention includes infinite first variance as r=0 and keeps total precision strictly positive. No division by zero occurs. |
| The RGO proportional-density notation suppresses normalization details | Actual Measure.tilted equality; integrability and positive finite normalization proved internally | source-implicit | Bounded positive measurable weights over a probability base justify normalization and its cancellation without additional integrability assumptions. |
| RGO built directly from the unnormalized potential U | A supplied probability base μ | unresolved | The source adapter identifying μ and its tilts with the specific Lebesgue densities remains a separately named obligation; this proof does not assume that adapter as its conclusion. |
The normalized-law calculation on a probability base only; the Gibbs-density adapter, curvature conclusions and recursive sampling guarantee remain open.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: The compiled measure identity generalizes the paper's Euclidean Gibbs setting to arbitrary Borel real inner-product spaces and arbitrary probability measures. — This extension is explicit in source.original_text and the lesson. The proof uses inner-product algebra, continuity and finite probability mass, not finite dimension or potential regularity.
- objects: Instantiation with the source Gibbs density remains an unproved adapter, not a hidden assumed equality. — The module contains no potential U or Lebesgue-density identification. The publication context separately lists gibbs-base-identification and explicitly says probability of the supplied μ does not prove normalizability of the paper's potential.
- assumptions: The decoder describes general API totalization without explicitly deriving that the fallback is unreachable here. — The missing explanatory derivation is valid from the reconstructed assumptions: continuous weights in (0,1] have positive finite integral under each probability base. The candidate proof and lesson supply this argument; no mathematical assumption or conclusion is missing.
- scopes: Curvature, condition-number updates, sampler implementation and costs are not proved by this declaration. — These omissions are intentional and visible in the full publication context, obligation map and lesson. They are not blocking for the explicitly selected normalized-measure component, but must remain excluded from completion claims.
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 proves only Lemma 6.4's normalized RGO-family calculation at the probability-base level. Identifying μ with the density proportional to exp(−U), and relating the first tilted law to U_A,u, remain explicit source adapters.
- The strong-convexity and smoothness parameters, their condition-number recurrence, actual recursive sampler, output discrepancy and expected query cost are separate obligations.
- The generic Borel inner-product-space and arbitrary-probability formulation is a disclosed generality of the calculation; it does not claim that the source sampler works in infinite-dimensional spaces or for singular target laws.
- The r=0 test exercises A=infinity, and the equal-positive-precision test checks the midpoint update.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- MeasureTheory.Measure.tilted: existing normalized exponential reweighting.
- MeasureTheory.tilted_tilted and tilted_const: composition and cancellation of constant normalized tilts.
- MeasureTheory.isProbabilityMeasure_tilted and integral_exp_pos: probability and strictly positive normalizer from integrability and nonzero mass.
- MeasureTheory.Integrable.mono': integrability under an integrable envelope; Borel measurability from continuity.
- real_inner_self_eq_norm_sq, inner_sub_left/right, inner_add_left/right, real_inner_smul_left/right: completion of the square.
Mathematical sources
- Chen, Chewi, Lu and Zhang, Smoothed Picard Hamiltonian Monte Carlo v1 — Section 6.2.2, Lemma 6.4 normalized-law clause and (6.1). ASTIS's original expanded proof of the omitted calculation, not quoted paper prose.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.