Actual Gaussian-Gibbs square-root density and energy domains

Derive the nonnegative residual and gradient growth; Normalize against the actual standard Gaussian; Identify the canonical volume Gibbs law; Differentiate the explicit positive square root; Produce the finite gradient and entropy domains; Integrate the exact Dirichlet-Fisher identity

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 gaussian_sqrt_density_domain
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {rho : E → ℝ} {L : ℝ≥0} (hrho : ContDiff ℝ 2 rho)
    (hrho0 : rho 0 = 0) (hgrad0 : gradient rho 0 = 0)
    (hH : ∀ u v : E, 0 ≤ fderiv ℝ (fderiv ℝ rho) u v v ∧
      fderiv ℝ (fderiv ℝ rho) u v v ≤ (L : ℝ)*‖v‖^2) :
    let gamma := stdGaussian E
    let Z := ∫ u, Real.exp (-rho u) ∂gamma
    let q := fun u => Real.exp (-rho u)/Z
    let f := fun u => Real.exp (-rho u/2)/Real.sqrt Z
    let r := gamma.tilted (fun u => -rho u)
    0 < Z ∧ Z ≤ 1 ∧
      r = (volume : Measure E).tilted (fun u => -(‖u‖^2/2+rho u)) ∧
      r = gamma.withDensity (fun u => ENNReal.ofReal (q u)) ∧
      IsProbabilityMeasure r ∧
      (∀ u, 0 < q u ∧ f u^2 = q u) ∧
      (∫ u, q u ∂gamma) = 1 ∧
      ContDiff ℝ 2 f ∧ MemLp f 2 gamma ∧
      MemLp (gradient f) 2 gamma ∧ MemLp (gradient rho) 2 r ∧
      Integrable (fun u => q u*Real.log (q u)) gamma ∧
      (∀ u, gradient f u = -(f u/2) • gradient rho u) ∧
      (∀ u, gradient (fun z => Real.log (q z)) u = -gradient rho u) ∧
      (∫ u, ‖gradient f u‖^2 ∂gamma) =
        (1/4 : ℝ)*(∫ u, ‖gradient rho u‖^2 ∂r) := by
  let gamma := stdGaussian E
  let Z := ∫ u, Real.exp (-rho u) ∂gamma
  let q := fun u => Real.exp (-rho u)/Z
  let f := fun u => Real.exp (-rho u/2)/Real.sqrt Z
  let r := gamma.tilted (fun u => -rho u)
  obtain ⟨hn,hg⟩ := rho_nonneg_and_gradient_growth hrho hrho0 hgrad0 hH
  obtain ⟨hw,hZ,hZone⟩ := weight_normalization hrho.continuous hn
  obtain ⟨hf,hfq,hdf,hdlog⟩ := density_calculus hrho hZ
  have hprob : IsProbabilityMeasure r := isProbabilityMeasure_tilted hw
  have hq : Integrable q gamma := hw.div_const Z
  have hqone : (∫ u, q u ∂gamma) = 1 := by
    rw [integral_div]
    exact div_self hZ.ne'
  have hflp : MemLp f 2 gamma := by
    apply (memLp_two_iff_integrable_sq_norm hf.continuous.aestronglyMeasurable).mpr
    apply hq.congr
    exact ae_of_all _ (fun u => by
      change q u = ‖f u‖^2
      rw [Real.norm_eq_abs,sq_abs]
      exact (hfq u).2.symm)
  have hwg := weighted_gradient_square_integrable hrho hn hg
  have hgc := Analysis.Calculus.Gradient.continuous_gradient_of_contDiff_one
    (hrho.of_le (by norm_num))
  have hir : Integrable (fun u => ‖gradient rho u‖^2) r :=
    (integrable_tilted_iff hw (fun u => ‖gradient rho u‖^2)).mpr
      (by simpa only [smul_eq_mul] using hwg)
  have hrlp : MemLp (gradient rho) 2 r :=
    (memLp_two_iff_integrable_sq_norm hgc.aestronglyMeasurable).mpr hir
  have hpoint (u : E) : ‖gradient f u‖^2 =
      (1/(4*Z))*(Real.exp (-rho u)*‖gradient rho u‖^2) := by
    rw [hdf u,norm_smul,mul_pow,Real.norm_eq_abs,sq_abs,neg_sq,div_pow,(hfq u).2]
    change (Real.exp (-rho u)/Z)/(2:ℝ)^2*‖gradient rho u‖^2 = _
    ring
  have hfg : Integrable (fun u => ‖gradient f u‖^2) gamma :=
    (hwg.const_mul (1/(4*Z))).congr (ae_of_all _ (fun u => (hpoint u).symm))
  have hfgc := Analysis.Calculus.Gradient.continuous_gradient_of_contDiff_one
    (hf.of_le (by norm_num))
  have hfglp : MemLp (gradient f) 2 gamma :=
    (memLp_two_iff_integrable_sq_norm hfgc.aestronglyMeasurable).mpr hfg
  have he := entropy_integrable hrho.continuous hn hZ
  have henergy : (∫ u, ‖gradient f u‖^2 ∂gamma) =
      (1/4 : ℝ)*(∫ u, ‖gradient rho u‖^2 ∂r) := by
    rw [integral_tilted,← integral_const_mul]
    apply integral_congr_ae
    exact ae_of_all _ (fun u => by
      change ‖gradient f u‖^2 = (1/4 : ℝ)*(Real.exp (-rho u)/Z) • ‖gradient rho u‖^2
      rw [hpoint u]
      simp only [smul_eq_mul]
      ring)
  exact ⟨hZ,hZone,actual_gaussian_tilt_volume rho,rfl,hprob,hfq,hqone,hf,hflp,
    hfglp,hrlp,he,hdf,hdlog,henergy⟩

end
end AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSqrtDensityDomain

Exact module and namespace context