An RGO of an RGO has an explicit normalized target law
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOClosure.quadratic_tilt_tilt · theorem · Teaching coverage
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.
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 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)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.RGOClosureScope 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.
Source and reuse
ASTIS 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.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.