Actual Gibbs gradient second moment

Derive noncompact weighted integrability from curvature, apply directional Haar IBP, sum via Parseval, normalize the actual exponential measure and integrate the Hessian bound.

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 gibbs_gradient_moment [CompleteSpace E] {U : E → ℝ} {α β : ℝ≥0}
    (hα : 0 < α) (_hαβ : α ≤ β) (hU : ContDiff ℝ 2 U)
    (hH : ∀ x v : E, (α : ℝ)*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ U) x v v ∧
      fderiv ℝ (fderiv ℝ U) x v v ≤ (β : ℝ)*‖v‖^2) :
    let μ := (volume : Measure E).tilted (fun x => -U x)
    let H := fun x => ∑ i, fderiv ℝ (fderiv ℝ U) x
      ((stdOrthonormalBasis ℝ E) i) ((stdOrthonormalBasis ℝ E) i)
    IsProbabilityMeasure μ ∧ Integrable (fun x => ‖gradient U x‖^2) μ ∧
      Integrable H μ ∧ (∫ x, ‖gradient U x‖^2 ∂μ) = (∫ x, H x ∂μ) ∧
      (∫ x, ‖gradient U x‖^2 ∂μ) ≤ (β : ℝ)*Module.finrank ℝ E := by
  classical
  let μ := (volume : Measure E).tilted (fun x => -U x)
  let b := stdOrthonormalBasis ℝ E
  let H := fun x => ∑ i, fderiv ℝ (fderiv ℝ U) x (b i) (b i)
  have hw := weighted_gradient hα hU hH
  have hunit (i) : ‖b i‖ = 1 := b.orthonormal.norm_eq_one i
  have hdiag (x : E) (i) : 0 ≤ fderiv ℝ (fderiv ℝ U) x (b i) (b i) ∧
      fderiv ℝ (fderiv ℝ U) x (b i) (b i) ≤ β := by
    have hh := hH x (b i)
    rw [hunit,one_pow,mul_one,mul_one] at hh
    exact ⟨(NNReal.coe_nonneg α).trans hh.1,hh.2⟩
  have hdir (i) := directional_ibp hU (b i) (hunit i) (fun x => hdiag x i)
    hw.1 hw.2.1 hw.2.2
  have hHi : Integrable (fun x => Real.exp (-U x)*H x) (volume : Measure E) := by
    have hi := integrable_finsetSum Finset.univ (fun i _ => (hdir i).2.1)
    simpa only [H,Finset.mul_sum] using hi
  have hparseval (x : E) : (∑ i, (fderiv ℝ U x (b i))^2) = ‖gradient U x‖^2 := by
    simpa only [inner_gradient_left,Real.norm_eq_abs,sq_abs] using
      b.sum_sq_norm_inner_left (gradient U x)
  have heq : (∫ x, Real.exp (-U x)*‖gradient U x‖^2) = ∫ x, Real.exp (-U x)*H x := by
    calc
      (∫ x, Real.exp (-U x)*‖gradient U x‖^2) =
          ∫ x, ∑ i, Real.exp (-U x)*(fderiv ℝ U x (b i))^2 := by
        simp only [← Finset.mul_sum,hparseval]
      _ = ∑ i, ∫ x, Real.exp (-U x)*(fderiv ℝ U x (b i))^2 :=
        integral_finsetSum _ (fun i _ => (hdir i).1)
      _ = ∑ i, ∫ x, Real.exp (-U x)*fderiv ℝ (fderiv ℝ U) x (b i) (b i) := by
        apply Finset.sum_congr rfl
        intro i _
        exact (hdir i).2.2
      _ = ∫ x, ∑ i, Real.exp (-U x)*fderiv ℝ (fderiv ℝ U) x (b i) (b i) :=
        (integral_finsetSum _ (fun i _ => (hdir i).2.1)).symm
      _ = ∫ x, Real.exp (-U x)*H x := by simp only [H,Finset.mul_sum]
  have : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hw.1
  have hgμ : Integrable (fun x => ‖gradient U x‖^2) μ := by
    apply (integrable_tilted_iff hw.1 _).2
    simpa only [smul_eq_mul] using hw.2.1
  have hHμ : Integrable H μ := by
    apply (integrable_tilted_iff hw.1 _).2
    simpa only [smul_eq_mul] using hHi
  have htilt (g : E → ℝ) : (∫ x, g x ∂μ) =
      (∫ x, Real.exp (-U x)*g x)/(∫ x, Real.exp (-U x)) := by
    rw [integral_tilted]
    simp only [smul_eq_mul]
    rw [← integral_div]
    apply integral_congr_ae
    filter_upwards with x
    ring
  have heqμ : (∫ x, ‖gradient U x‖^2 ∂μ) = ∫ x, H x ∂μ := by
    rw [htilt,htilt,heq]
  refine ⟨inferInstance,hgμ,hHμ,heqμ,?_⟩
  change (∫ x, ‖gradient U x‖^2 ∂μ) ≤ (β : ℝ)*Module.finrank ℝ E
  rw [heqμ]
  have hbound (x : E) : H x ≤ (β : ℝ)*Module.finrank ℝ E := by
    calc
      H x ≤ ∑ _i : Fin (Module.finrank ℝ E), (β : ℝ) :=
        Finset.sum_le_sum (fun i _ => (hdiag x i).2)
      _ = (β : ℝ)*Module.finrank ℝ E := by simp [mul_comm]
  simpa only [integral_const,probReal_univ,one_smul] using
    integral_mono hHμ (integrable_const ((β : ℝ)*Module.finrank ℝ E)) hbound

end AutoSamplingTheory.TechnicalLemmas.Analysis.GibbsGradientMoment

Exact module and namespace context