Actual compact scalar Gaussian log-Sobolev inequality

Authored compact C2 scalar prerequisite for omitted GaussianLSI background, independently statement-sealed before proof. External real-product/sum-of-integrals route is source context, with representation gaps disclosed; ASTIS actual Boolean count parents are compiled local producers, not an SLT proof certificate.

Complete source statement (Samplinglib restatement)

For every real C2 compactly supported function f, the homogeneous entropy of f squared under the actual centered variance-one Gaussian is at most twice the integral of its squared real derivative. Signed functions and zero mass are included. The count laws, domains, finite inequality and limits are produced internally, with no caller positivity, normalization, integrability, inequality or limit certificate.

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

Actual compact scalar Gaussian log-Sobolev inequality

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactLogSobolev.compact_gaussian_logSobolev · theorem · Teaching coverage

Read this first

Mathematical statement

\[\gamma=\mathcal N(0,1),\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 (f\prime)^2\,d\gamma.\]

Lean statement · compact_gaussian_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_gaussian_logSobolev
    (f : ℝ → ℝ) (hf : ContDiff ℝ 2 f) (hs : HasCompactSupport f) :
    let γ : Measure ℝ := gaussianReal 0 1
    (∫ x, (f x)^2 * Real.log ((f x)^2) ∂γ) -
      (∫ x, (f x)^2 ∂γ) * Real.log (∫ x, (f x)^2 ∂γ) ≤
    2 * ∫ x, (deriv f x)^2 ∂γ

Exact module and namespace context

Proof roadmap

1Use the actual finite Boolean inequality
For each positive successor N, use the literal cardinal-normalized counting probability on all N Boolean coordinates and its sqrt-normalized sign sum S_N. Apply the compiled finite function LSI to h_N=f composed with S_N. This internally supplies true probability/L1 and the entropy inequality, for signed f and zeros as well.
2Identify the same full energy pointwise
The finite inequality writes the original value minus the flipped value. The energy-limit parent writes the opposite orientation. Their squared differences agree for every coordinate and every actual state, so the same full sum under the same integral is used. No product-law identification or sum/integral exchange is supplied.
3Consume the actual entropy and energy limits
Compact C2 observer convergence supplies the literal homogeneous entropy limit, including zero mass via continuity of tlogt. The separately compiled full-flip producer supplies convergence of the actual entire energy integral to4 times Gaussian derivative energy. Multiplication by1/2 yields a limit of twice that energy. These limits concern the same actual count laws and sign sums.
4Pass the inequality through closed real order
Every successor finite entropy is at most its half full energy. The natural-number atTop filter is nontrivial, and the order relation ≤ is closed on the real line. Apply the two-limit order theorem to these genuine convergent sequences. No rate, monotonicity, positive mass, or supplied Gaussian inequality is needed.

Full assumptions and notation

All objects and hypotheses

Only f:Real→Real, ContDiff Real2 f and HasCompactSupport f are public analytic inputs. f may change sign or vanish identically; no mass positivity or normalization is assumed.
The measure is exactly gaussianReal0 1, with variance1. The entropy is the literal homogeneous expression, not an asserted normalized-density KL identity.
Actual34/36/37 internally construct finite count probability, genuine L1 domains and entropy/full-energy limits. The public theorem takes none of them as a premise.
The finite inequality has coefficient1/2 multiplying the full coordinate-flip energy. Its actual Gaussian energy limit is4 times the derivative-square integral, giving exactly2.
This authored compact scalar background does not establish finite-Hilbert/noncompact GaussianLSI, Gaussian T2, printed FIRST4.6, paper main results, expected query costs or composition.

Mathematical proof

1. Use the actual finite Boolean inequality

For each positive successor N, use the literal cardinal-normalized counting probability on all N Boolean coordinates and its sqrt-normalized sign sum S_N. Apply the compiled finite function LSI to h_N=f composed with S_N. This internally supplies true probability/L1 and the entropy inequality, for signed f and zeros as well.

\[\mu_N=2^{-N}\sum_{\varepsilon\in\{0,1\}^N}\delta_\varepsilon,\quad S_N=N^{-1/2}\sum_j\sigma(\varepsilon_j),\quad \operatorname{Ent}_{\mu_N}((f\circ S_N)^2)\le\tfrac12\int\sum_j[f(S_N(\varepsilon))-f(S_N(\varepsilon^{(j)}))]^2\,d\mu_N.\]

Corresponding Lean step

BernoulliLogSobolev.bernoulli_function_logSobolev; hn; actual local mu/S

2. Identify the same full energy pointwise

The finite inequality writes the original value minus the flipped value. The energy-limit parent writes the opposite orientation. Their squared differences agree for every coordinate and every actual state, so the same full sum under the same integral is used. No product-law identification or sum/integral exchange is supplied.

\[[a-b]^2=[b-a]^2,\qquad D_N(\varepsilon)=\sum_j[f(S_N(\varepsilon^{(j)}))-f(S_N(\varepsilon))]^2.\]

Corresponding Lean step

sub_sq_comm; simpa only [sub_sq_comm] using hn

3. Consume the actual entropy and energy limits

Compact C2 observer convergence supplies the literal homogeneous entropy limit, including zero mass via continuity of tlogt. The separately compiled full-flip producer supplies convergence of the actual entire energy integral to4 times Gaussian derivative energy. Multiplication by1/2 yields a limit of twice that energy. These limits concern the same actual count laws and sign sums.

\[\operatorname{Ent}_{\mu_{N+1}}((f\circ S_{N+1})^2)\to\operatorname{Ent}_\gamma(f^2),\qquad \tfrac12\int D_{N+1}\,d\mu_{N+1}\to\tfrac12\,4\int(f\prime)^2\,d\gamma=2\int(f\prime)^2\,d\gamma.\]

Corresponding Lean step

GaussianCompactEntropy.compact_count_gaussian_entropy_limits; GaussianFlipEnergy.compact_count_gaussian_flip_energy_limit; tEnt/tEnergy/tHalf; Filter.Tendsto.const_mul; heq

4. Pass the inequality through closed real order

Every successor finite entropy is at most its half full energy. The natural-number atTop filter is nontrivial, and the order relation ≤ is closed on the real line. Apply the two-limit order theorem to these genuine convergent sequences. No rate, monotonicity, positive mass, or supplied Gaussian inequality is needed.

\[\bigl(\forall N,\ a_N\le b_N\bigr)\land a_N\to a\land b_N\to b\quad\Longrightarrow\quad a\le b;\qquad \operatorname{Ent}_\gamma(f^2)\le2\int(f\prime)^2\,d\gamma.\]

Corresponding Lean step

le_of_tendsto_of_tendsto; Eventually.of_forall

Lean verification

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

Lean proof · compact_gaussian_logSobolev

Use the actual finite Boolean inequality; Identify the same full energy pointwise; Consume the actual entropy and energy limits; Pass the inequality through closed real order

Download module (.lean)

theorem compact_gaussian_logSobolev
    (f : ℝ → ℝ) (hf : ContDiff ℝ 2 f) (hs : HasCompactSupport f) :
    let γ : Measure ℝ := gaussianReal 0 1
    (∫ x, (f x)^2 * Real.log ((f x)^2) ∂γ) -
      (∫ x, (f x)^2 ∂γ) * Real.log (∫ x, (f x)^2 ∂γ) ≤
    2 * ∫ x, (deriv f x)^2 ∂γ := by
  dsimp only
  let μ : (n : ℕ) → Measure (Fin n → Bool) := fun n =>
    (Fintype.card (Fin n → Bool) : ℝ≥0∞)⁻¹ • Measure.count
  let S : (n : ℕ) → (Fin n → Bool) → ℝ := fun n ε =>
    (Real.sqrt (n : ℝ))⁻¹ * ∑ j : Fin n, if ε j then (1 : ℝ) else -1
  rcases GaussianCompactEntropy.compact_count_gaussian_entropy_limits f hf hs
    with ⟨_, _, _, _, _, _, _, tEnt⟩
  rcases GaussianFlipEnergy.compact_count_gaussian_flip_energy_limit f hf hs
    with ⟨_, _, tEnergy⟩
  change Tendsto (fun n : ℕ =>
    (∫ ε, (f (S (n+1) ε))^2 * Real.log ((f (S (n+1) ε))^2) ∂μ (n+1)) -
      (∫ ε, (f (S (n+1) ε))^2 ∂μ (n+1)) *
        Real.log (∫ ε, (f (S (n+1) ε))^2 ∂μ (n+1))) atTop
    (𝓝 ((∫ x, (f x)^2 * Real.log ((f x)^2) ∂gaussianReal 0 1) -
      (∫ x, (f x)^2 ∂gaussianReal 0 1) *
        Real.log (∫ x, (f x)^2 ∂gaussianReal 0 1))) at tEnt
  change Tendsto (fun n : ℕ => ∫ ε : Fin (n+1) → Bool,
    (∑ j : Fin (n+1),
      (f (S (n+1) (Function.update ε j (!ε j))) - f (S (n+1) ε))^2)
      ∂μ (n+1)) atTop (𝓝 (4 * ∫ x, (deriv f x)^2 ∂gaussianReal 0 1)) at tEnergy
  have tHalf : Tendsto (fun n : ℕ => (1/2 : ℝ) *
      ∫ ε : Fin (n+1) → Bool, (∑ j : Fin (n+1),
        (f (S (n+1) (Function.update ε j (!ε j))) - f (S (n+1) ε))^2)
        ∂μ (n+1)) atTop (𝓝 (2 * ∫ x, (deriv f x)^2 ∂gaussianReal 0 1)) := by
    have heq : (1/2 : ℝ) * (4 * ∫ x, (deriv f x)^2 ∂gaussianReal 0 1) =
        2 * ∫ x, (deriv f x)^2 ∂gaussianReal 0 1 := by ring
    simpa only [heq] using tEnergy.const_mul (1/2 : ℝ)
  apply le_of_tendsto_of_tendsto tEnt tHalf
  exact Eventually.of_forall fun n => by
    have hn := (BernoulliLogSobolev.bernoulli_function_logSobolev (n+1)
      (fun ε => f (S (n+1) ε))).2.2.2.2
    change ((∫ ε, (f (S (n+1) ε))^2 * Real.log ((f (S (n+1) ε))^2) ∂μ (n+1)) -
      (∫ ε, (f (S (n+1) ε))^2 ∂μ (n+1)) *
        Real.log (∫ ε, (f (S (n+1) ε))^2 ∂μ (n+1))) ≤
      (1/2 : ℝ) * ∫ ε : Fin (n+1) → Bool, (∑ j : Fin (n+1),
        (f (S (n+1) ε) - f (S (n+1) (Function.update ε j (!ε j))))^2)
        ∂μ (n+1) at hn
    simpa only [sub_sq_comm] using hn

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactLogSobolev

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Compact scalar Gaussian homogeneous entropy-energy background; full printed FIRST requires further analytic and transport producers.	Only f,C2,compact with exact variance1 and constant2, signed/zero included.	same	Every law, domain, finite inequality and limit is an internal actual34/36/37 output, with no public certificate.
Pinned external real-product representation and sum-of-integrals route.	Authored actual Bool normalized count with pointwise square-orientation identity and literal integral-of-full-sum energy.	source-implicit	Concrete representation difference is explicit; no real-product transport certificate or implicit sum/integral exchange.
Finite-Hilbert/noncompact GaussianLSI, T2/FIRST4.6 and full paper errors/costs/composition.	Authored compact C2 scalar Gaussian homogeneous entropy <=2 derivative-square integral, signed f and zero mass included. Only f/C2/compact analytic premises; true Gaussian/count L1 and finite entropy/energy comparison are internal actual34/36/37 outputs. Exact variance1. Not full noncompact/Hilbert GaussianLSI, T2/FIRST4.6/main/work/composition. Actual37 final source/exactcommit/shared readiness is mandatory before claim or proof search. Focused3180PASS for zero observer and concrete signed smooth compact cutoff. Standard3 only. Independent wholeproof/blind/source/exactcommit and shared publication remain separate.	unresolved	Compact scalar inequality only. Continuous product tensorization, actual Gaussian Hilbert law/Parseval and cutoff limits remain to be proved. TV proximity does not transfer unbounded expected costs.

Authored compact C2 scalar Gaussian homogeneous entropy <=2 derivative-square integral, signed f and zero mass included. Only f/C2/compact analytic premises; true Gaussian/count L1 and finite entropy/energy comparison are internal actual34/36/37 outputs. Exact variance1. Not full noncompact/Hilbert GaussianLSI, T2/FIRST4.6/main/work/composition. Actual37 final source/exactcommit/shared readiness is mandatory before claim or proof search. Focused3180PASS for zero observer and concrete signed smooth compact cutoff. Standard3 only. Independent wholeproof/blind/source/exactcommit and shared publication remain separate.

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

Authored compact C2 scalar Gaussian homogeneous entropy ≤2 derivative-square integral, signed f and zero mass included. Only f/C2/compact analytic premises; true Gaussian/count L1 and finite entropy/energy comparison are internal actual34/36/37 outputs. Exact variance1. Not full noncompact/Hilbert GaussianLSI, T2/FIRST4.6/main/work/composition. Actual37 final source/exactcommit/shared readiness is mandatory before claim or proof search. Focused3180PASS for zero observer and concrete signed smooth compact cutoff. Standard3 only. Independent wholeproof/blind/source/exactcommit and shared publication remain separate.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

sub_sq_comm
Filter.Tendsto.const_mul
le_of_tendsto_of_tendsto
Filter.Eventually.of_forall

Mathematical sources

FIRST S4.E6 omitted GaussianLSI background; pinned SLT GaussianLSI/OneDimGLSICompSmo.lean:45-82 compact limit closure; authored actual Bool count alternative — Authored compact C2 scalar Gaussian homogeneous entropy <=2 derivative-square integral, signed f and zero mass included. Only f/C2/compact analytic premises; true Gaussian/count L1 and finite entropy/energy comparison are internal actual34/36/37 outputs. Exact variance1. Not full noncompact/Hilbert GaussianLSI, T2/FIRST4.6/main/work/composition. Actual37 final source/exactcommit/shared readiness is mandatory before claim or proof search. Focused3180PASS for zero observer and concrete signed smooth compact cutoff. Standard3 only. Independent wholeproof/blind/source/exactcommit and shared publication remain separate.
Pinned external compact GaussianLSI source route — External reference only; actual ASTIS count integration replaces the representation, no upstream compile/LSI certificate.

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

Actual compact scalar Gaussian log-Sobolev inequality

Complete source statement (Samplinglib restatement)

Actual compact scalar Gaussian log-Sobolev inequality

Read the formalized proofs

Actual compact scalar Gaussian log-Sobolev inequality

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Use the actual finite Boolean inequality

2. Identify the same full energy pointwise

3. Consume the actual entropy and energy limits

4. Pass the inequality through closed real order

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?