GibbsPositionMoment: mathematical reading route

Actual gradient L1 implies position L1;full-space coordinate IBP and finite basis sum;positive normalizer and actual tilt;integrate coercivity.

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_position_moment {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)
    (p : E) (hp : gradient U p = 0) :
    let μ := (volume : Measure E).tilted (fun x => -U x)
    IsProbabilityMeasure μ ∧
    Integrable (fun x => Real.exp (-U x)) (volume : Measure E) ∧
    0 < (∫ x, Real.exp (-U x)) ∧
    Integrable (fun x => ‖x-p‖^2) μ ∧
    Integrable (fun x => inner ℝ (x-p) (gradient U x)) μ ∧
    (∫ x, inner ℝ (x-p) (gradient U x) ∂μ) = Module.finrank ℝ E ∧
    (∫ x, ‖x-p‖^2 ∂μ) ≤ (Module.finrank ℝ E : ℝ)/(α : ℝ) := by
  classical
  let μ := (volume : Measure E).tilted (fun x => -U x)
  let b := stdOrthonormalBasis ℝ E
  rcases stationary_position_integrability hα hαβ hU hH p hp with
    ⟨hprob,hw,hpos,hlin,hpair,hcoerce⟩
  have hgrad := (GibbsGradientMoment.gibbs_gradient_moment hα hαβ hU hH).2.1
  have hdir (i) := coordinate_position_ibp hU p (b i) (b.orthonormal.norm_eq_one i)
    hw hpos hlin hgrad
  have hparseval (x : E) :
      (∑ i, inner ℝ (x-p) (b i)*fderiv ℝ U x (b i)) = inner ℝ (x-p) (gradient U x) := by
    simpa [inner_gradient_right] using b.sum_inner_mul_inner (x-p) (gradient U x)
  have heq : (∫ x, Real.exp (-U x)*inner ℝ (x-p) (gradient U x)) =
      (Module.finrank ℝ E : ℝ)*(∫ x, Real.exp (-U x)) := by
    calc
      (∫ x, Real.exp (-U x)*inner ℝ (x-p) (gradient U x)) =
          ∫ x, ∑ i, Real.exp (-U x)*inner ℝ (x-p) (b i)*fderiv ℝ U x (b i) := by
        apply integral_congr_ae
        filter_upwards with x
        rw [← hparseval x,Finset.mul_sum]
        simp only [mul_assoc]
      _ = ∑ i, ∫ x, Real.exp (-U x)*inner ℝ (x-p) (b i)*fderiv ℝ U x (b i) :=
        integral_finsetSum _ (fun i _ => (hdir i).1)
      _ = ∑ _i : Fin (Module.finrank ℝ E), ∫ x, Real.exp (-U x) := by
        apply Finset.sum_congr rfl
        intro i _
        exact (hdir i).2
      _ = (Module.finrank ℝ E : ℝ)*(∫ x, Real.exp (-U x)) := by simp
  have hZ : 0 < (∫ x, Real.exp (-U x)) := integral_exp_pos hw
  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 hid : (∫ x, inner ℝ (x-p) (gradient U x) ∂μ) = Module.finrank ℝ E := by
    rw [htilt,heq]
    exact mul_div_cancel_right₀ _ hZ.ne'
  refine ⟨hprob,hw,hZ,hpos,hpair,hid,?_⟩
  have hi := integral_mono (hpos.const_mul (α : ℝ)) hpair hcoerce
  rw [integral_const_mul] at hi
  change (∫ x, inner ℝ (x-p) (gradient U x) ∂μ) = Module.finrank ℝ E at hid
  rw [hid] at hi
  apply (le_div_iff₀ (show (0 : ℝ) < α from hα)).2
  nlinarith [hi]


end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GibbsPositionMoment

Exact module and namespace context