AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedHessianBounds

Samplinglib mathematical lesson

Actual SPHMC smoothed Hessian bounds

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedHessianBounds.smoothed_hessian_bounds · theorem · Teaching coverage

Read this first

Mathematical statement

For the actual source Gaussian-smoothed unnormalized potential and true RGO posterior, produce probability and vectorL2, covariance upper norma^2/(kappa^-1+eta^-1), C2 regularity and (kappa+eta)^-1*norma^2≤D2V_eta(y)[a,a]≤(1+eta)^-1*norma^2, and true1-Lipschitz gradient. This is the analytic Lemma4.1, not an algorithm/main theorem.

\[R_y(dx)\propto e^{-V(x)-\|x-y\|^2/(2\eta)}dx,\quad (\kappa+\eta)^{-1}I\preceq D^2V_\eta\preceq(1+\eta)^{-1}I,\quad \operatorname{Lip}(\nabla V_\eta)\le1.\]

Lean statement · smoothed_hessian_bounds

For the actual source Gaussian-smoothed unnormalized potential and true RGO posterior, produce probability and vectorL2, covariance upper norma^2/(kappa^-1+eta^-1), C2 regularity and (kappa+eta)^-1*norma^2<=D2V_eta(y)[a,a]<=(1+eta)^-1*norma^2, and true1-Lipschitz gradient. This is the analytic Lemma4.1, not an algorithm/main theorem.

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.

Download module (.lean)

theorem smoothed_hessian_bounds
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace E]
    {V : E → ℝ} {κ η : ℝ}
    (hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x a : E, κ⁻¹*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a ∧
      fderiv ℝ (fderiv ℝ V) x a a ≤ ‖a‖^2)
    (hη : 0 < η) (hη1 : η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let C := ((Real.sqrt (2*Real.pi*η))⁻¹)^Module.finrank ℝ E
    let A := fun y : E => C*∫ x, Real.exp (-V x-‖y-x‖^2/(2*η)) ∂(volume : Measure E)
    let Vη := fun y => -Real.log (A y)
    let R := fun y : E => μ.tilted (fun x => -‖x-y‖^2/(2*η))
    IsProbabilityMeasure μ ∧ ContDiff ℝ 2 Vη ∧
      (∀ y, IsProbabilityMeasure (R y) ∧ MemLp id 2 (R y) ∧
        (∀ a, ProbabilityTheory.covarianceBilin (R y) a a ≤ ‖a‖^2/(κ⁻¹+η⁻¹)) ∧
        ∀ a, (1/(κ+η))*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ Vη) y a a ∧
          fderiv ℝ (fderiv ℝ Vη) y a a ≤ (1/(1+η))*‖a‖^2) ∧
      LipschitzWith (1 : ℝ≥0) (gradient Vη)

Exact module and namespace context

Proof roadmap

1Construct the actual source smoothing
Positive source curvature gives the true partition and probability. The accepted convolution producer gives C2 V_eta and the literal normalized-U constant shift, with no input normalizer.
2Produce true posterior moments and derivative identity
The Gaussian convolution producer gives R_y probability and vectorL2 for every actualy, and true Hessian of U. The produced constant shift identifies both Hessians.
3Keep the unreflected quadratic law
Set W_y=V+norm(x-y)^2/(2eta). Derive its C2 Hessian shift and both positive curvature bounds. True strong convexity gives its exponential integrability/positive partition; tilted_tilted proves literal R_y equality.
4Apply the canonical covariance producer
Transport the internally produced posterior vectorL2 through the actual law equality, then apply the new Poincare-derived covariance theorem. This suffices for the source isotropic bound; full anisotropic BL remains open.
5Derive the exact lower Hessian constant
Subtract the covariance upper bound in the true identity. kappa/eta and both sum denominators are positive, so algebra preserves inequality and yields the exact source lower constant.
6Reuse the actual reverse-Cramer-Rao half
The independently checked actual posterior covariance lower and source smoothed Hessian upper theorem is specialized to beta1. No duplicated abstract Hessian field or assumed upper bound.
7Prove true global gradient Lipschitz
The produced C2 potential has nonnegative Hessian and upper quadratic bound bynorma^2. Existing Riesz/selfadjoint Rayleigh norm and global mean-value producer yields1-Lipschitz gradient with zero extra regularization. The source eta cap remains an explicit premise.

Full assumptions and notation

All objects and hypotheses

Source C2 V with beta=1 and alpha=kappa^-1; kappa≥1; actual allpoint/allvector curvature kappa^-1*norma^2≤D2V[a,a]≤norma^2; source0<eta≤1 retained.
Actual source UNNORMALIZED exp(-V_eta)=exp(-V)*Gaussian_eta, normalized Gibbs mu=volume.tilted(-V), unreflected R_y=mu.tilted(-norm(x-y)^2/(2eta)). Finite Hilbert/Borel including0 is disclosed representation extension.
No partition, covariance, moment, derivative or PI certificate on this source theorem. Actual probability, posterior vectorL2, C2, U=V_eta+logZV, both true Hessian bounds and global Lipschitz are produced internally. No joint measurable posterior kernel selector, higher derivative, numerical kernel, cost or main claim.

Mathematical proof

1. Construct the actual source smoothing

Positive source curvature gives the true partition and probability. The accepted convolution producer gives C2 V_eta and the literal normalized-U constant shift, with no input normalizer.

\[e^{-V_\eta}=e^{-V}*\gamma_\eta,\quad U=V_\eta+\log Z_V.\]

Corresponding Lean step

SmoothedGibbsPotential.smoothed_gibbs_potential

2. Produce true posterior moments and derivative identity

The Gaussian convolution producer gives R_y probability and vectorL2 for every actualy, and true Hessian of U. The produced constant shift identifies both Hessians.

\[D^2V_\eta(y)[a,a]=\|a\|^2/\eta-\operatorname{Cov}_{R_y}(a,a)/\eta^2.\]

Corresponding Lean step

GaussianConvolutionRegularity.gaussian_convolution_derivatives; fderiv_add_const

3. Keep the unreflected quadratic law

Set W_y=V+norm(x-y)^2/(2eta). Derive its C2 Hessian shift and both positive curvature bounds. True strong convexity gives its exponential integrability/positive partition; tilted_tilted proves literal R_y equality.

\[(\kappa^{-1}+\eta^{-1})I\preceq D^2W_y\preceq(1+\eta^{-1})I,\quad R_y=Z_y^{-1}e^{-W_y}dx.\]

Corresponding Lean step

HasFDerivAt.norm_sq; tilted_tilted; StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn

4. Apply the canonical covariance producer

Transport the internally produced posterior vectorL2 through the actual law equality, then apply the new Poincare-derived covariance theorem. This suffices for the source isotropic bound; full anisotropic BL remains open.

\[\operatorname{Cov}_{R_y}(a,a)\le\|a\|^2/(\kappa^{-1}+\eta^{-1}).\]

Corresponding Lean step

GibbsLinearCovarianceUpper.gibbs_linear_covariance_upper

5. Derive the exact lower Hessian constant

Subtract the covariance upper bound in the true identity. kappa/eta and both sum denominators are positive, so algebra preserves inequality and yields the exact source lower constant.

\[\frac{\|a\|^2}{\eta}-\frac{\|a\|^2}{\eta^2(\kappa^{-1}+\eta^{-1})}=\frac{\|a\|^2}{\kappa+\eta}.\]

Corresponding Lean step

div_le_div_of_nonneg_right; sub_le_sub_left; field_simp

6. Reuse the actual reverse-Cramer-Rao half

The independently checked actual posterior covariance lower and source smoothed Hessian upper theorem is specialized to beta1. No duplicated abstract Hessian field or assumed upper bound.

\[D^2V_\eta(y)[a,a]\le\|a\|^2/(1+\eta).\]

Corresponding Lean step

SmoothedHessianUpper.smoothed_hessian_upper

7. Prove true global gradient Lipschitz

The produced C2 potential has nonnegative Hessian and upper quadratic bound bynorma^2. Existing Riesz/selfadjoint Rayleigh norm and global mean-value producer yields1-Lipschitz gradient with zero extra regularization. The source eta cap remains an explicit premise.

\[0\preceq D^2V_\eta\preceq I\Longrightarrow\operatorname{Lip}(\nabla V_\eta)\le1.\]

Corresponding Lean step

QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · smoothed_hessian_bounds

Construct the actual source smoothing; Produce true posterior moments and derivative identity; Keep the unreflected quadratic law; Apply the canonical covariance producer; Derive the exact lower Hessian constant; Reuse the actual reverse-Cramer-Rao half; Prove true global gradient Lipschitz

Download module (.lean)

theorem smoothed_hessian_bounds
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace E]
    {V : E → ℝ} {κ η : ℝ}
    (hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x a : E, κ⁻¹*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a ∧
      fderiv ℝ (fderiv ℝ V) x a a ≤ ‖a‖^2)
    (hη : 0 < η) (hη1 : η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let C := ((Real.sqrt (2*Real.pi*η))⁻¹)^Module.finrank ℝ E
    let A := fun y : E => C*∫ x, Real.exp (-V x-‖y-x‖^2/(2*η)) ∂(volume : Measure E)
    let Vη := fun y => -Real.log (A y)
    let R := fun y : E => μ.tilted (fun x => -‖x-y‖^2/(2*η))
    IsProbabilityMeasure μ ∧ ContDiff ℝ 2 Vη ∧
      (∀ y, IsProbabilityMeasure (R y) ∧ MemLp id 2 (R y) ∧
        (∀ a, ProbabilityTheory.covarianceBilin (R y) a a ≤ ‖a‖^2/(κ⁻¹+η⁻¹)) ∧
        ∀ a, (1/(κ+η))*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ Vη) y a a ∧
          fderiv ℝ (fderiv ℝ Vη) y a a ≤ (1/(1+η))*‖a‖^2) ∧
      LipschitzWith (1 : ℝ≥0) (gradient Vη) := by
  have hk : 0<κ := lt_of_lt_of_le zero_lt_one hκ
  have ha : 0<κ⁻¹ := inv_pos.mpr hk
  let α : ℝ≥0 := ⟨κ⁻¹,ha.le⟩
  have hα : 0<α := ha
  have hα1 : α≤1 := (inv_le_one₀ hk).2 hκ
  have hHV : ∀ x a : E, (α:ℝ)*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a ∧
      fderiv ℝ (fderiv ℝ V) x a a ≤ ((1:ℝ≥0):ℝ)*‖a‖^2 := by
    intro x a
    change κ⁻¹*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a ∧
      fderiv ℝ (fderiv ℝ V) x a a ≤ 1*‖a‖^2
    simpa only [one_mul] using hH x a
  let μ := (volume : Measure E).tilted (fun x => -V x)
  let C := ((Real.sqrt (2*Real.pi*η))⁻¹)^Module.finrank ℝ E
  let A := fun y : E => C*∫ x, Real.exp (-V x-‖y-x‖^2/(2*η)) ∂(volume : Measure E)
  let Vη := fun y => -Real.log (A y)
  let R := fun y : E => μ.tilted (fun x => -‖x-y‖^2/(2*η))
  let U := fun y : E => -Real.log (C*∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ)
  let ZV := ∫ x, Real.exp (-V x) ∂(volume : Measure E)
  obtain ⟨_hZ,hμ,_hlaw,_hI,_hInt,_hTilt,_hA,hC2,hshift⟩ :=
    SmoothedGibbsPotential.smoothed_gibbs_potential ha hV (fun x a => (hH x a).1) hη
  have : IsProbabilityMeasure μ := hμ
  have hC : 0<C := by dsimp only [C]; positivity
  obtain ⟨hRm,_hD,hDD⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Measure.GaussianConvolutionRegularity.gaussian_convolution_derivatives μ hη hC
  have hi := AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn
    ha (hV.differentiable (by norm_num))
    (AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower hV (fun x a => (hH x a).1))
  have hcov (y : E) : ∀ a : E, covarianceBilin (R y) a a ≤ ‖a‖^2/(κ⁻¹+η⁻¹) := by
    let W := fun x => V x+η⁻¹/2*‖x-y‖^2
    have hW : ContDiff ℝ 2 W := hV.add (contDiff_const.mul ((contDiff_id.sub contDiff_const).norm_sq (𝕜:=ℝ)))
    have hVd : Differentiable ℝ V := hV.differentiable (by norm_num)
    have hVdd : Differentiable ℝ (fderiv ℝ V) := (hV.fderiv_right (m:=1) (by norm_num)).differentiable_one
    have hq (x : E) : HasFDerivAt (fun z => η⁻¹/2*‖z-y‖^2)
        (η⁻¹ • innerSL ℝ (x-y)) x := by
      convert (((hasFDerivAt_id x).sub_const y).norm_sq).const_mul (η⁻¹/2)
        using 1 <;> first | rfl | (ext a; simp;ring)
    have hWfd (x : E) : fderiv ℝ W x = fderiv ℝ V x+η⁻¹ • innerSL ℝ (x-y) :=
      ((hVd x).hasFDerivAt.add (hq x)).fderiv
    let J : E →L[ℝ] (E →L[ℝ] ℝ) :=
      {toFun := fun a => innerSL ℝ a
       map_add' := by intros;ext;simp
       map_smul' := by intros;ext;simp
       cont := (innerSL ℝ (E:=E)).continuous}
    have hWdd (x : E) : HasFDerivAt (fderiv ℝ W)
        (fderiv ℝ (fderiv ℝ V) x+η⁻¹ • J) x := by
      rw [show fderiv ℝ W=(fun z => fderiv ℝ V z+η⁻¹ • innerSL ℝ (z-y)) from funext hWfd]
      convert (hVdd x).hasFDerivAt.add ((J.hasFDerivAt.comp x ((hasFDerivAt_id x).sub_const y)).const_smul η⁻¹) using 1 <;> rfl
    have hb (x a : E) : (κ⁻¹+η⁻¹)*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ W) x a a ∧
        fderiv ℝ (fderiv ℝ W) x a a ≤ (1+η⁻¹)*‖a‖^2 := by
      rw [(hWdd x).fderiv]
      change (κ⁻¹+η⁻¹)*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a+η⁻¹*inner ℝ a a ∧
        fderiv ℝ (fderiv ℝ V) x a a+η⁻¹*inner ℝ a a ≤ (1+η⁻¹)*‖a‖^2
      rw [real_inner_self_eq_norm_sq]
      constructor <;> nlinarith [(hH x a).1,(hH x a).2]
    have hm : 0<κ⁻¹+η⁻¹ := add_pos ha (inv_pos.mpr hη)
    have hmM : κ⁻¹+η⁻¹≤1+η⁻¹ := by
      simpa only [add_comm] using (add_le_add_right ((inv_le_one₀ hk).2 hκ) η⁻¹)
    have hiW := AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn
      hm (hW.differentiable (by norm_num))
      (AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower hW (fun x a => (hb x a).1))
    have hRW : R y=(volume : Measure E).tilted (fun x => -W x) := by
      dsimp only [R,μ]
      rw [tilted_tilted hi]
      congr 1
      funext x
      simp only [Pi.add_apply,W]
      field_simp [hη.ne']
      ring
    have hX : MemLp id 2 ((volume : Measure E).tilted (fun x => -W x)) := hRW ▸ (hRm y).2
    rw [hRW]
    exact AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsLinearCovarianceUpper.gibbs_linear_covariance_upper
      W hW hiW (integral_exp_pos hiW) (κ⁻¹+η⁻¹) (1+η⁻¹) hm hmM
      (fun x a => (hb x a).1) (fun x a => (hb x a).2) hX
  have he : U=(fun y => Vη y+Real.log ZV) := funext hshift
  have hd : fderiv ℝ U=fderiv ℝ Vη := by
    rw [he]
    funext y
    exact fderiv_add_const _
  change ∀ y a b, fderiv ℝ (fderiv ℝ U) y a b = _ at hDD
  rw [hd] at hDD
  have hlower (y a : E) : (1/(κ+η))*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ Vη) y a a := by
    rw [hDD y a a,real_inner_self_eq_norm_sq]
    have hm : 0<κ⁻¹+η⁻¹ := add_pos ha (inv_pos.mpr hη)
    have hke : 0<κ+η := add_pos hk hη
    calc
      (1/(κ+η))*‖a‖^2 = ‖a‖^2/η-(‖a‖^2/(κ⁻¹+η⁻¹))/η^2 := by
        field_simp [hk.ne',hη.ne',hm.ne',hke.ne']
        ring
      _ ≤ ‖a‖^2/η-covarianceBilin (R y) a a/η^2 :=
        sub_le_sub_left (div_le_div_of_nonneg_right (hcov y a) (sq_nonneg η)) _
  have hupper : ∀ y a : E, fderiv ℝ (fderiv ℝ Vη) y a a ≤ (1/(1+η))*‖a‖^2 := by
    have hu := (SmoothedHessianUpper.smoothed_hessian_upper hα hα1 hV hHV hη).2
    simpa only [NNReal.coe_one,one_mul] using hu
  have hHVη : ∀ y a : E, ((0:ℝ≥0):ℝ)*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ Vη) y a a ∧
      fderiv ℝ (fderiv ℝ Vη) y a a ≤ ((1:ℝ≥0):ℝ)*‖a‖^2 := by
    intro y a
    have hp : 0≤(1/(κ+η))*‖a‖^2 := by positivity
    have hu : 1/(1+η)≤1 := by
      apply (div_le_iff₀ (by positivity : 0<1+η)).2
      linarith
    simpa only [NNReal.coe_zero,zero_mul,NNReal.coe_one,one_mul] using
      And.intro (hp.trans (hlower y a)) ((hupper y a).trans (mul_le_mul_of_nonneg_right hu (sq_nonneg ‖a‖)))
  have hLip := (AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
    (m:=0) (L:=1) (r:=0) hC2 hHVη (0:E)).2
  simp only [NNReal.coe_zero,zero_div,zero_mul,add_zero] at hLip
  exact ⟨hμ,hC2,fun y => ⟨(hRm y).1,(hRm y).2,hcov y,fun a => ⟨hlower y a,hupper y a⟩⟩,hLip⟩

end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedHessianBounds

Exact module and namespace context

Scope and omitted-condition boundaries

Canonical BOTH-curvature Gibbs linear covariance upper with genuine vectorL2, actual positive partition and probability normalization; not full anisotropic Brascamp-Lieb. Actual source beta=1 alpha=kappa^-1, 1≤kappa, 0<eta≤1; genuine posterior law R_y, internally produced probability/vectorL2/positive partitions/C2 and normalized-U versus unnormalized-V_eta constant shift. Derive true covariance upper and both Hessian bounds (kappa+eta)^-1 and (1+eta)^-1, then true 1-Lipschitz gradient. Finite real Hilbert/Borel including zero dimension is disclosed representation extension. No input covariance/PI/oracle/moment/normalizer certificate on source Anchor. No joint measurable posterior kernel selector, higher smoothing derivatives, algorithm/Wp/proxy-warmness/main/querycost/composition. PBPS reflected quarter law and source-score remain separate. TV never transfers unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

tilted_tilted
integral_exp_pos
HasFDerivAt.norm_sq
fderiv_add_const
div_le_div_of_nonneg_right
sub_le_sub_left
field_simp

Mathematical sources

SPHMC actual Lemma4.1 and explicit covariance prerequisite — Canonical BOTH-curvature Gibbs linear covariance upper with genuine vectorL2, actual positive partition and probability normalization; not full anisotropic Brascamp-Lieb. Actual source beta=1 alpha=kappa^-1, 1<=kappa, 0<eta<=1; genuine posterior law R_y, internally produced probability/vectorL2/positive partitions/C2 and normalized-U versus unnormalized-V_eta constant shift. Derive true covariance upper and both Hessian bounds (kappa+eta)^-1 and (1+eta)^-1, then true 1-Lipschitz gradient. Finite real Hilbert/Borel including zero dimension is disclosed representation extension. No input covariance/PI/oracle/moment/normalizer certificate on source Anchor. No joint measurable posterior kernel selector, higher smoothing derivatives, algorithm/Wp/proxy-warmness/main/querycost/composition. PBPS reflected quarter law and source-score remain separate. TV never transfers unbounded expected cost.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

SmoothedHessianBounds: mathematical reading route

Actual SPHMC smoothed Hessian bounds

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Construct the actual source smoothing

2. Produce true posterior moments and derivative identity

3. Keep the unreflected quadratic law

4. Apply the canonical covariance producer

5. Derive the exact lower Hessian constant

6. Reuse the actual reverse-Cramer-Rao half

7. Prove true global gradient Lipschitz

Lean verification

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources