gaussian_sqrt_density_domain

Plain-English statement

Actual covarianceI Gaussian, true volume/relative tilt equality, internally positive partition and L2/entropy domains, explicit gradients and exact energy1/4. Includes L0/dimension0; source consumes all eta>0. Independent exactcommit 1de412105042ebcfe147d50a3d1022fb0514faad. No weakSobolev/KL/LSI/T2/W2/main/cost credit.

Lean statement

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

Open AutoSamplingTheory/TechnicalLemmas/Measure/GaussianSqrtDensityDomain.lean:211published source at ed709a7f320d

Proof architecture

Actual SPHMC standardized true RGO analytic domains before Gaussian LSI/T2; no SALD or second-consumer admission

Lean proof walkthrough

• Read the quantified variables and typeclass brackets as part of the mathematical statement; inferred arguments are not missing assumptions.
• `have` creates a named intermediate mathematical fact.
• `rw` rewrites by an established identity.
• `simp` normalizes through registered definitional and theorem rewrites.
• `apply` reduces the goal to the hypotheses of a reusable theorem.
• `exact` closes the current goal with an already typed term.
• `simpa` closes the goal after a controlled simplification of a typed result.

Why the statement has this shape

The declaration is kept at the reusable level recorded by its Registry tags and direct consumers. Explicit measures, spaces, wrappers, and regularity hypotheses expose interfaces that paper notation often infers. A theorem card explains those interfaces but never widens the compiled statement.

Hidden assumptions and non-claims

• Measurability is represented explicitly or must be supplied by a dependency.
• Integrability is an input or proved output; a displayed integral alone does not supply it.
• Totalized `fderiv` values must not be read as a differentiability theorem.
• Almost-everywhere hypotheses depend on the stated measure and representative.
• Density statements retain normalization and absolute-continuity prerequisites.