Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

GaussianCompactLogSobolev: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Actual compact scalar Gaussian log-Sobolev inequality
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

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.

\[\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

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.

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

  1. 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.

  2. 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.

  3. 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.

  4. 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

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 ∂γ := 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

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

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