Noncompact C2 Gaussian function log-Sobolev inequality

Mathematical statement

For every finite-dimensional complete real Hilbert/Borel space E, including rank zero, let gamma be literal stdGaussian E. Every signed real globally C2 f with actual f in L2(gamma), true gradient f in L2(gamma), and Phi(f²) integrable satisfies homogeneous Ent_gamma(f²)≤2 integral norm(gradient f)^2. The actual cutoff mass, entropy and gradient-energy limits are proved internally. Phi(t)=t log t is continuous at zero; neither positive mass nor normalization nor compact support is assumed.

theorem gaussian_logSobolev_of_contDiff
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E]
    (f : E → ℝ) (hf : ContDiff ℝ 2 f)
    (hf2 : MemLp f 2 (ProbabilityTheory.stdGaussian E))
    (hgrad2 : MemLp (gradient f) 2 (ProbabilityTheory.stdGaussian E))
    (hentropy : Integrable (fun x => (f x)^2 * Real.log ((f x)^2))
      (ProbabilityTheory.stdGaussian E)) :
    let γ : Measure E := ProbabilityTheory.stdGaussian E
    (∫ x, (f x)^2 * Real.log ((f x)^2) ∂γ) -
      (∫ x, (f x)^2 ∂γ) * Real.log (∫ x, (f x)^2 ∂γ) ≤
      2 * ∫ x, ‖gradient f x‖^2 ∂γ

Proof roadmap

1. 1Derive genuine square and energy domains

   The two genuine L2 hypotheses imply square and Hilbert-gradient-energy L1. The entropy L1 is the third analytic-domain premise. C2 gives continuity and the true Riesz-gradient measurability needed below; no totalized-integral fallback is used.

2. 2Construct actual compact approximants

   Use the canonical radial cutoff at R_n=n+1, multiply by f, and derive C2compact regularity. One positive derivative constant C is chosen before all radii. Range[0,1] and the real neighborhood plateau come from the same actual cutoff.

3. 3Bound the true gradient and identify its limit

   Apply the real product derivative and Riesz inverse, whose isometry identifies derivative norm with gradient norm. With R_n≥1, the square energy is dominated by2G²+2C²f². For each point the cutoff equals1 on a neighborhood for all sufficiently large radii, so its product has exactly the original true gradient there, including rank0.

4. 4Control entropy even where the density vanishes

   The totalized zero-aware product identity gives Phi(aq)=aPhi(q)+qPhi(a). For0≤a≤1, the lower bound a-1≤Phi(a) and Phi(a)≤0 imply |Phi(a)|≤1. With a=chi_n² and q=f² this gives an integrable dominator without taking log of f or dividing by mass.

5. 5Prove all three real integral limits

   Apply dominated convergence separately with q, |Phi(q)|+q and2G²+2C²q. Every sequence is strongly measurable through actual continuity, every dominator is L1 from the analytic domains, and the pointwise limits are proved using the actual cutoff and gradient plateau.

6. 6Pass the compact inequalities without changing the constant

   Apply actual compact41LSI to each f_n. Continuity of Phi at the limiting mass, including mass0, gives the homogeneous entropy limit. Closed-order convergence passes the inequalities with the unchanged coefficient2.

7. 7Exercise the actual noncompact posterior

   The true standardizedRGO theorem supplies C2, fL2, gradientL2 and qlogqL1 at its actual proximal witness, with f²=q. The Test applies this new result to the raw f=exp(-rho/2)/sqrtZ, without a cutoff certificate or upper step-size restriction. The distinct33KL witness must still be reconciled; GaussianT2/FIRST4.6 remain separate.