Compact finite-Hilbert standard Gaussian log-Sobolev inequality

Explicit sufficient compact background, not the printed FIRST statement/full GaussianW12 theorem. Exact640 statement and independently reconstructed109node328edge2OR source topology admitted before proof. Root-created representation-only overlay separately reviewed; original BLOCKED records retained.

Complete source statement (Samplinglib restatement)

For every finite-dimensional real Hilbert/Borel space E, including rank zero, and signed real C2 compactly supported f, let gamma be the actual canonical stdGaussian E. The theorem internally produces true L1 of f squared, f squared times log(f squared), and the Hilbert norm of the true gradient squared, then proves homogeneous Ent_gamma(f squared)<=2 integral norm(gradient f)^2. Canonical basis law transport and orthonormal Parseval are internal; zero mass is included.

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Compact finite-Hilbert standard Gaussian log-Sobolev inequality

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactHilbertLogSobolev.compact_stdGaussian_logSobolev · theorem · Teaching coverage

Read this first

Mathematical statement

For every finite-dimensional real Hilbert/Borel space E, including rank zero, and signed real C2 compactly supported f, let gamma be the actual canonical stdGaussian E. The theorem internally produces true L1 of f squared, f squared times log(f squared), and the Hilbert norm of the true gradient squared, then proves homogeneous Ent_gamma(f squared)≤2 integral norm(gradient f)^2. Canonical basis law transport and orthonormal Parseval are internal; zero mass is included.

\[\gamma=\mathrm{stdGaussian}(E),\qquad f\in C_c^2(E;\mathbb R),\qquad \operatorname{Ent}_{\gamma}(f^2)=\int f^2\log(f^2)\,d\gamma-\left(\int f^2\,d\gamma\right)\log\left(\int f^2\,d\gamma\right)\le2\int\|\nabla f\|^2\,d\gamma.\]

Lean statement · compact_stdGaussian_logSobolev

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.

Download module (.lean)

theorem compact_stdGaussian_logSobolev
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E]
    (f : E → ℝ) (hf : ContDiff ℝ 2 f) (hs : HasCompactSupport f) :
    let γ : Measure E := ProbabilityTheory.stdGaussian E
    Integrable (fun x => (f x)^2) γ ∧
    Integrable (fun x => (f x)^2 * Real.log ((f x)^2)) γ ∧
    Integrable (fun x => ‖gradient f x‖^2) γ ∧
    (∫ 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 ∂γ

Exact module and namespace context

Proof roadmap

1Choose the actual canonical coordinate homeomorphism
Let n be the real dimension and b the canonical orthonormal basis. The inverse continuous basis equivalence T maps coordinate vectors to their actual finite linear combination. This is an internal linear homeomorphism even at dimension0.
2Identify the literal Gaussian law
The definition of stdGaussian uses precisely this canonical basis sum. Rewriting the inverse basis formula identifies gamma as the pushforward of the actual independent variance-one coordinate Gaussian product. Covariance similarity alone is never used as a law certificate.
3Pull back the true compact smooth function
The actual pullback g=f o T is C2 because T is continuous linear; the homeomorphism pulls compact support back. The compiled finite-product producer40 returns every genuine product L1 domain and the constant2 entropy bound for this same g.
4Compute actual directional derivatives
The inverse basis equivalence sends the literal single-coordinate unit vector to b_i. Chain rule therefore gives D_i g(z)=fderiv f(Tz)[b_i]. The actual Riesz gradient identity rewrites this as the Hilbert inner product, with C2 supplying true differentiability.
5Use orthonormal Parseval without dimension loss
The actual orthonormal sum of squared gradient coordinates equals the Hilbert gradient norm squared. This equality also handles rank0 by the empty basis sum. It does not assert equality with the default Pi derivative operator norm.
6Transport genuine domains and real integrals
Square and continuous tlogt-square are continuous; the reusable C1 gradient helper gives continuity of the true gradient energy. Integrable_map_measure transports the actual product L1 outputs to gamma. Integral_map then identifies the two entropy integrals and the energy integral, with measurable T and actual integrand measurability.
7Return the exact compact Hilbert inequality
Rewrite the finite-product inequality using the true law and Parseval identities. The public result joins the three derived domains with homogeneous entropy≤2 actual gradient energy. The test cuts off the actual32 posterior square-root density at a positive radius using the same proximal witness; passing the radius to infinity is a later theorem.

Full assumptions and notation

All objects and hypotheses

E is any finite-dimensional complete real inner product space, with compatible norm and Borel measurable structure, including rank0. The basis is chosen internally; no positive-dimension assumption.
Only f, globally real C2 regularity and compact support are analytic premises. Signed functions/zero mass are included; no law, covariance, positivity, normalized mass, domain, gradient-Parseval or desired-inequality certificate is supplied.
gamma is literally Mathlib ProbabilityTheory.stdGaussian E. The actual canonical orthonormal basis sum of independent centered variance-one coordinates is identified with the continuous linear homeomorphism internally.
gradient is the literal global Mathlib Riesz Frechet representative. True coordinate chain rule and Parseval give its Hilbert norm squared; no default-Pi supremum operator norm or dimensional multiplier.
All3 L1 domains are conclusions. Measurable law transport and real map integrals carry true product-domain square, continuous tlogt and full energy from actual40.
Exact function-LSI coefficient2. Actual32 standardized RGO square-root-density cutoff test is a genuine consumer; cutoff exhaustion/coherent33 KL/Fisher, full noncompact/W12 LSI, separate GaussianT2/FIRST4.6 and both paper main/error/work/cost remain open.

Mathematical proof

1. Choose the actual canonical coordinate homeomorphism

Let n be the real dimension and b the canonical orthonormal basis. The inverse continuous basis equivalence T maps coordinate vectors to their actual finite linear combination. This is an internal linear homeomorphism even at dimension0.

\[n=\dim_{\mathbb R}E,\quad b=\mathrm{stdOrthonormalBasis},\quad T=(b.\mathrm{equivFunL})^{-1},\quad Tz=\sum_i z_i b_i.\]

Corresponding Lean step

stdOrthonormalBasis; Basis.equivFunL; Basis.equivFun_symm_apply

2. Identify the literal Gaussian law

The definition of stdGaussian uses precisely this canonical basis sum. Rewriting the inverse basis formula identifies gamma as the pushforward of the actual independent variance-one coordinate Gaussian product. Covariance similarity alone is never used as a law certificate.

\[\gamma_n=\bigotimes_{i\in\mathrm{Fin}(n)}\mathcal N(0,1),\qquad \mathrm{stdGaussian}(E)=T_\#\gamma_n.\]

Corresponding Lean step

hγ; literal stdGaussian definition; Basis.equivFun_symm_apply

3. Pull back the true compact smooth function

The actual pullback g=f o T is C2 because T is continuous linear; the homeomorphism pulls compact support back. The compiled finite-product producer40 returns every genuine product L1 domain and the constant2 entropy bound for this same g.

\[g=f\circ T\in C_c^2,\qquad \operatorname{Ent}_{\gamma_n}(g^2)\le2\int\sum_i(D_i g)^2\,d\gamma_n.\]

Corresponding Lean step

ContDiff.comp_continuousLinearMap; HasCompactSupport.comp_homeomorph; compact_gaussian_pi_logSobolev

4. Compute actual directional derivatives

The inverse basis equivalence sends the literal single-coordinate unit vector to b_i. Chain rule therefore gives D_i g(z)=fderiv f(Tz)[b_i]. The actual Riesz gradient identity rewrites this as the Hilbert inner product, with C2 supplying true differentiability.

\[Te_i=b_i,\qquad D_i g(z)=\mathrm{fderiv}_{\mathbb R}f(Tz)[b_i]=\langle\nabla f(Tz),b_i\rangle.\]

Corresponding Lean step

pullback_energy.hsingle/hD; fderiv_comp; ContinuousLinearMap.fderiv; inner_gradient_left

5. Use orthonormal Parseval without dimension loss

The actual orthonormal sum of squared gradient coordinates equals the Hilbert gradient norm squared. This equality also handles rank0 by the empty basis sum. It does not assert equality with the default Pi derivative operator norm.

\[\sum_i(D_i g(z))^2=\sum_i\langle\nabla f(Tz),b_i\rangle^2=\|\nabla f(Tz)\|^2.\]

Corresponding Lean step

pullback_energy; OrthonormalBasis.sum_sq_inner_left

6. Transport genuine domains and real integrals

Square and continuous tlogt-square are continuous; the reusable C1 gradient helper gives continuity of the true gradient energy. Integrable_map_measure transports the actual product L1 outputs to gamma. Integral_map then identifies the two entropy integrals and the energy integral, with measurable T and actual integrand measurability.

\[f^2,\ \Phi(f^2),\ \|\nabla f\|^2\in L^1(\gamma),\quad \int H\,d\gamma=\int H(Tz)\,d\gamma_n,\qquad\Phi(t)=t\log t.\]

Corresponding Lean step

continuous_gradient_of_contDiff_one; Real.Continuous.mul_log; integrable_map_measure; integral_map

7. Return the exact compact Hilbert inequality

Rewrite the finite-product inequality using the true law and Parseval identities. The public result joins the three derived domains with homogeneous entropy≤2 actual gradient energy. The test cuts off the actual32 posterior square-root density at a positive radius using the same proximal witness; passing the radius to infinity is a later theorem.

\[\operatorname{Ent}_{\mathrm{stdGaussian}(E)}(f^2)\le2\int\|\nabla f\|^2\,d\mathrm{stdGaussian}(E).\]

Corresponding Lean step

compact_stdGaussian_logSobolev; actual_posterior_compact_lsi Test

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · compact_stdGaussian_logSobolev

Choose the actual canonical coordinate homeomorphism; Identify the literal Gaussian law; Pull back the true compact smooth function; Compute actual directional derivatives; Use orthonormal Parseval without dimension loss; Transport genuine domains and real integrals; Return the exact compact Hilbert inequality

Download module (.lean)

theorem compact_stdGaussian_logSobolev
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E]
    (f : E → ℝ) (hf : ContDiff ℝ 2 f) (hs : HasCompactSupport f) :
    let γ : Measure E := ProbabilityTheory.stdGaussian E
    Integrable (fun x => (f x)^2) γ ∧
    Integrable (fun x => (f x)^2 * Real.log ((f x)^2)) γ ∧
    Integrable (fun x => ‖gradient f x‖^2) γ ∧
    (∫ 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 ∂γ := by
  dsimp only
  let n := Module.finrank ℝ E
  let b := stdOrthonormalBasis ℝ E
  let T := b.toBasis.equivFunL.symm
  let μ : Measure (Fin n → ℝ) := Measure.pi (fun _ : Fin n => gaussianReal 0 1)
  have hγ : stdGaussian E = μ.map T := by
    unfold stdGaussian
    congr 1
    funext x
    exact (b.toBasis.equivFun_symm_apply x).symm
  have hg : ContDiff ℝ 2 (f ∘ T) :=
    hf.comp_continuousLinearMap (g := T.toContinuousLinearMap)
  have hgs : HasCompactSupport (f ∘ T) := hs.comp_homeomorph T.toHomeomorph
  obtain ⟨hm, hp, _, he, hLSI⟩ :=
    GaussianCompactProductLogSobolev.compact_gaussian_pi_logSobolev n (f ∘ T) hg hgs
  have henergy : ∀ x, (∑ i : Fin n, (fderiv ℝ (f ∘ T) x (Pi.single i 1))^2) =
      ‖gradient f (T x)‖^2 := pullback_energy b f hf
  have cm : Continuous (fun x => (f x)^2) := hf.continuous.pow 2
  have cp : Continuous (fun x => (f x)^2 * Real.log ((f x)^2)) := Real.Continuous.mul_log cm
  have ce : Continuous (fun x => ‖gradient f x‖^2) :=
    (Analysis.Calculus.Gradient.continuous_gradient_of_contDiff_one
      (hf.of_le (by norm_num))).norm.pow 2
  have hTm := T.continuous.measurable.aemeasurable (μ := μ)
  have im : Integrable (fun x => (f x)^2) (stdGaussian E) := by
    rw [hγ]
    exact (integrable_map_measure cm.aestronglyMeasurable hTm).2 hm
  have ip : Integrable (fun x => (f x)^2 * Real.log ((f x)^2)) (stdGaussian E) := by
    rw [hγ]
    exact (integrable_map_measure cp.aestronglyMeasurable hTm).2 hp
  have ie : Integrable (fun x => ‖gradient f x‖^2) (stdGaussian E) := by
    rw [hγ]
    apply (integrable_map_measure ce.aestronglyMeasurable hTm).2
    change Integrable (fun x : Fin n → ℝ => ‖gradient f (T x)‖^2) μ
    simpa only [henergy] using he
  refine ⟨im, ip, ie, ?_⟩
  rw [hγ, integral_map hTm cp.aestronglyMeasurable,
    integral_map hTm cm.aestronglyMeasurable,
    integral_map hTm ce.aestronglyMeasurable]
  simpa only [Function.comp_apply, henergy] using hLSI

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactHilbertLogSobolev

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
FIRST4.6 invokes Gaussian LSI and Talagrand for the real standardized RGO.	For every finite-dimensional real Hilbert/Borel space E, including rank zero, and signed real C2 compactly supported f, let gamma be the actual canonical stdGaussian E. The theorem internally produces true L1 of f squared, f squared times log(f squared), and the Hilbert norm of the true gradient squared, then proves homogeneous Ent_gamma(f squared)<=2 integral norm(gradient f)^2. Canonical basis law transport and orthonormal Parseval are internal; zero mass is included.	source-implicit	Supply compact finiteHilbert Gaussian background with literal law/gradient. Genuine noncompact square-root-density limit and GaussianT2 are still separate prerequisites.
Broader GaussianW12/noncompact function class.	C2compact f with all3L1 internally derived.	API-limitation	Explicit sufficient compact class; no unannounced extra FIRST premise. Actual32 is tested only after real radial cutoff, without exhaustion credit.
Variance-one finiteHilbert function-LSI coefficient2.	Actual40 coordinate-energy bound transported by literal canonical basis law and exact orthonormal Parseval.	same	No dimension factor or Pi operator-norm substitution. Signed/zero/rank0 retained.
Coherent noncompact32/33 KL/Fisher, GaussianT2/FIRST and both papers main/query-cost composition.	Actual stdGaussian E on any finite-dimensional real Hilbert space, including rank0, for signed real C2compact f. Internally produced square/Phi-square/gradient-square L1 and homogeneous entropy<=2 actual gradient-square integral. Actual canonical orthonormal law map and gradient Parseval are internal; no supplied law/LSI/domain/energy/limit/basis certificates. Compact sufficient background only; actual32 noncompact cutoff/coherent33 KL/Fisher, T2/FIRST4.6, both paper algorithms/main/error/work/cost/composition and full reader/PURIFIED remain open. Actual focused3812 passes; generic zero, signed nonzero rank0 and real32 standardized RGO sqrt-density with canonical proximal witness and positive-scale radial cutoff compile. No raw noncompact application or limit claim. Independent proof/fidelity/commit/shared admission pending.	unresolved	No TV transfer of unbounded expected costs or paper completion.

Actual stdGaussian E on any finite-dimensional real Hilbert space, including rank0, for signed real C2compact f. Internally produced square/Phi-square/gradient-square L1 and homogeneous entropy<=2 actual gradient-square integral. Actual canonical orthonormal law map and gradient Parseval are internal; no supplied law/LSI/domain/energy/limit/basis certificates. Compact sufficient background only; actual32 noncompact cutoff/coherent33 KL/Fisher, T2/FIRST4.6, both paper algorithms/main/error/work/cost/composition and full reader/PURIFIED remain open. Actual focused3812 passes; generic zero, signed nonzero rank0 and real32 standardized RGO sqrt-density with canonical proximal witness and positive-scale radial cutoff compile. No raw noncompact application or limit claim. Independent proof/fidelity/commit/shared admission pending.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Actual stdGaussian E on any finite-dimensional real Hilbert space, including rank0, for signed real C2compact f. Internally produced square/Phi-square/gradient-square L1 and homogeneous entropy≤2 actual gradient-square integral. Actual canonical orthonormal law map and gradient Parseval are internal; no supplied law/LSI/domain/energy/limit/basis certificates. Compact sufficient background only; actual32 noncompact cutoff/coherent33 KL/Fisher, T2/FIRST4.6, both paper algorithms/main/error/work/cost/composition and full reader/PURIFIED remain open. Actual focused3812 passes; generic zero, signed nonzero rank0 and real32 standardized RGO sqrt-density with canonical proximal witness and positive-scale radial cutoff compile. No raw noncompact application or limit claim. Independent proof/fidelity/commit/shared admission pending.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

stdOrthonormalBasis
Module.Basis.equivFunL
Module.Basis.equivFun_symm_apply
ProbabilityTheory.stdGaussian
ContDiff.comp_continuousLinearMap
HasCompactSupport.comp_homeomorph
fderiv_comp
ContinuousLinearMap.comp_apply
ContinuousLinearMap.fderiv
inner_gradient_left
OrthonormalBasis.sum_sq_inner_left
Real.Continuous.mul_log
MeasureTheory.integrable_map_measure
MeasureTheory.integral_map

Mathematical sources

FIRST S4.E6 / S4.SS1.p4.3 omitted GaussianLSI background; authored compact finiteHilbert canonical law/gradient adapter from actual40 — Actual stdGaussian E on any finite-dimensional real Hilbert space, including rank0, for signed real C2compact f. Internally produced square/Phi-square/gradient-square L1 and homogeneous entropy<=2 actual gradient-square integral. Actual canonical orthonormal law map and gradient Parseval are internal; no supplied law/LSI/domain/energy/limit/basis certificates. Compact sufficient background only; actual32 noncompact cutoff/coherent33 KL/Fisher, T2/FIRST4.6, both paper algorithms/main/error/work/cost/composition and full reader/PURIFIED remain open. Actual focused3812 passes; generic zero, signed nonzero rank0 and real32 standardized RGO sqrt-density with canonical proximal witness and positive-scale radial cutoff compile. No raw noncompact application or limit claim. Independent proof/fidelity/commit/shared admission pending.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Compact finite-Hilbert standard Gaussian log-Sobolev inequality

Complete source statement (Samplinglib restatement)

Compact finite-Hilbert standard Gaussian log-Sobolev inequality

Read the formalized proofs

Compact finite-Hilbert standard Gaussian log-Sobolev inequality

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Choose the actual canonical coordinate homeomorphism

2. Identify the literal Gaussian law

3. Pull back the true compact smooth function

4. Compute actual directional derivatives

5. Use orthonormal Parseval without dimension loss

6. Transport genuine domains and real integrals

7. Return the exact compact Hilbert inequality

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?