AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOCalculus

- The source's regularized potential has the stated curvature and smoothness, positive finite Gibbs mass, and an actual probability law. A further quadratic regularization gives exactly the updated normalized source potential, with the condition-number formula used by the recursive stages. No minimizer, moment, integrability or conditional-law identity is assumed.

theorem rgo_calculus {U : E → ℝ} {κ a : ℝ} (hκ : 0 < κ)
    (hU : ContDiff ℝ 2 U)
    (hH : ∀ x v : E, κ⁻¹ * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ U) x v) v ∧
      (fderiv ℝ (fderiv ℝ U) x v) v ≤ ‖v‖ ^ 2)
    (r : ℝ≥0) (ha : 0 < a) (u y : E) :
    let W := fun x => U x + (r : ℝ) / 2 * ‖x - u‖ ^ 2
    let α := κ⁻¹ + (r : ℝ)
    let β : ℝ≥0 := 1 + r
    let K := (β : ℝ) / α
    let rp := (r : ℝ) + a⁻¹
    let w := rp⁻¹ • ((r : ℝ) • u + a⁻¹ • y)
    StrongConvexOn Set.univ α W ∧
      LipschitzWith β (gradient W) ∧
      Integrable (fun x => Real.exp (-W x)) (volume : Measure E) ∧
      0 < ∫ x, Real.exp (-W x) ∂(volume : Measure E) ∧
      IsProbabilityMeasure ((volume : Measure E).tilted (fun x => -W x)) ∧
      IsProbabilityMeasure ((volume : Measure E).tilted
        (fun x => -(U x + rp / 2 * ‖x - w‖ ^ 2))) ∧
      (volume : Measure E).tilted (fun x => -(W x + a⁻¹ / 2 * ‖x - y‖ ^ 2)) =
        volume.tilted (fun x => -(U x + rp / 2 * ‖x - w‖ ^ 2)) ∧
      ((β : ℝ) + a⁻¹) / (α + a⁻¹) = (a * (β : ℝ) + 1) * K /
        (a * (β : ℝ) + K) := by
  let W := fun x => U x + (r : ℝ) / 2 * ‖x - u‖ ^ 2
  let m : ℝ≥0 := ⟨κ⁻¹, (inv_pos.mpr hκ).le⟩
  have hbounds : ∀ x v : E,
      (m : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ U) x v) v ∧
      (fderiv ℝ (fderiv ℝ U) x v) v ≤ (1 : ℝ≥0) * ‖v‖ ^ 2 := by
    intro x v
    exact ⟨(hH x v).1, by simpa using (hH x v).2⟩
  have hreg (t : ℝ≥0) (z : E) :=
    TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
      hU hbounds (r := t) z
  have hI (t : ℝ≥0) (z : E) :
      Integrable (fun x => Real.exp (-(U x + (t : ℝ) / 2 * ‖x - z‖ ^ 2)))
        (volume : Measure E) := by
    apply TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn
      (m := ((m + t : ℝ≥0) : ℝ))
    · exact add_pos_of_pos_of_nonneg (inv_pos.mpr hκ) t.coe_nonneg
    · exact (hU.add (contDiff_const.mul
        ((contDiff_id.sub contDiff_const).norm_sq (𝕜 := ℝ)))).differentiable
        (by norm_num)
    · exact (hreg t z).1
  have hIU : Integrable (fun x => Real.exp (-U x)) (volume : Measure E) := by
    simpa only [NNReal.coe_zero, zero_div, zero_mul, add_zero] using hI 0 u
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/RGOCalculus.lean:34published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.