GaussianCompactProductLogSobolev: mathematical reading route

Mathematical statement

For every n≥0 and signed real C2 compactly supported f on Fin n → Real, let gamma_n be the actual product of n independent centered variance-one scalar Gaussian laws and D_i f(x)=fderiv Real f x(Pi.single i1). The theorem internally produces L1 of f squared, f squared times log(f squared), every coordinate derivative squared and their finite sum, and proves homogeneous Ent_gamma_n(f squared)≤2 integral sum_i(D_i f)^2. Zero mass and dimension0 are included.

theorem compact_gaussian_pi_logSobolev
    (n : ℕ) (f : (Fin n → ℝ) → ℝ)
    (hf : ContDiff ℝ 2 f) (hs : HasCompactSupport f) :
    let γ : Measure (Fin n → ℝ) := Measure.pi (fun _ : Fin n => gaussianReal 0 1)
    let D : Fin n → (Fin n → ℝ) → ℝ := fun i x => fderiv ℝ f x (Pi.single i 1)
    Integrable (fun x => (f x)^2) γ ∧
    Integrable (fun x => (f x)^2 * Real.log ((f x)^2)) γ ∧
    (∀ i, Integrable (fun x => (D i x)^2) γ) ∧
    Integrable (fun x => ∑ i, (D i x)^2) γ ∧
    (∫ x, (f x)^2 * Real.log ((f x)^2) ∂γ) -
      (∫ x, (f x)^2 ∂γ) * Real.log (∫ x, (f x)^2 ∂γ) ≤
    2 * ∫ x, ∑ i, (D i x)^2 ∂γ

Proof roadmap

1. 1Produce genuine compact Gaussian domains

   C2 gives continuous actual Frechet derivatives. Compact support is preserved by each fixed directional derivative, squaring, and the continuous tlogt map with value0 at0. Continuous compact functions are integrable under the actual finite Gaussian law. Finite summation gives the full coordinate-energy domain internally.

2. 2Handle the actual empty-coordinate probability law

   At dimension0 the carrier is a singleton and every f is constant there. Actual probability integrals retain that constant; homogeneous entropy cancels identically and the finite coordinate sum is empty. No positive dimension or square-mass assumption is required.

3. 3Split the true law and preserve original slice regularity

   The actual Fin.cons map takes the scalar Gaussian times the n-coordinate Gaussian product to gamma_(n+1). Its continuous linear equivalence supplies the genuine measurable embedding. Fixed scalar and tail insertions are closed embeddings, so compositions with the original f preserve compact support as well as C2 regularity.

4. 4Identify the actual coordinate derivatives

   The real coordinate-update chain rule differentiates the actual original slices. Updating the head gives the0th direction; updating a tail coordinate commutes with Fin.cons and gives its successor direction. These are literal directional identities, with no Hilbert gradient or operator-norm replacement.

5. 5Apply actual binary entropy to original conditional entropies

   Compact continuity supplies a genuine global bound on F(a,y)=f(a,y)^2; joint measurability and pointwise nonnegativity are internal. The actual bounded binary producer supplies all joint/slice/marginal tlogt domains and its marginal inequality. True Fubini and integrable subtraction convert that inequality to the conditional-entropy bound below, including zero fibers/mass.

6. 6Use the scalar theorem and strict dimension induction

   Apply the actual compact scalar Gaussian LSI to each original scalar slice and the induction hypothesis to each original n-dimensional tail slice. Both regularity/support inputs were constructed internally; the square root of a marginal average is never differentiated. Coordinate identities retain the exact coefficient2.

7. 7Integrate and assemble the full finite energy

   The joint coordinate-square domains pull back along the actual measure-preserving map. Their outer integrals and conditional entropies are genuinely integrable, so integral monotonicity is valid. Fubini and the finite head-plus-tail sum identity combine both bounds into exactly2 times the actual total coordinate energy. The public theorem joins this inequality with the internally produced domains.