Samplinglib mathematical lesson

True finite Boolean function log-Sobolev inequality

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BernoulliLogSobolev.bernoulli_function_logSobolev · theorem · Teaching coverage

Read this first

Mathematical statement

For every finite n including zero and arbitrary signed real h on all Boolean coordinates, normalized counting measure is probability and all three integrals are genuine L1; homogeneous entropy of h squared is at most half the expectation of the unnormalized sum of full coordinate-flip squares.

\[\mu_n=2^{-n}\sum_{\varepsilon\in\{0,1\}^n}\delta_\varepsilon,\qquad\operatorname{Ent}_{\mu_n}(h^2)\le\frac12\mathbb E_{\mu_n}\sum_{j=1}^n(h(\varepsilon)-h(\varepsilon^{(j)}))^2.\]

Lean statement · bernoulli_function_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 bernoulli_function_logSobolev (n : ℕ) (h : (Fin n → Bool) → ℝ) :
    let μ : Measure (Fin n → Bool) :=
      (Fintype.card (Fin n → Bool) : ℝ≥0∞)⁻¹ • Measure.count
    let D := fun ε : Fin n → Bool =>
      ∑ j : Fin n, (h ε - h (Function.update ε j (!ε j))) ^ 2
    IsProbabilityMeasure μ ∧
      Integrable (fun ε => (h ε) ^ 2) μ ∧
      Integrable (fun ε => (h ε) ^ 2 * Real.log ((h ε) ^ 2)) μ ∧
      Integrable D μ ∧
      ((∫ ε, (h ε) ^ 2 * Real.log ((h ε) ^ 2) ∂μ) -
        (∫ ε, (h ε) ^ 2 ∂μ) * Real.log (∫ ε, (h ε) ^ 2 ∂μ) ≤
      (1 / 2 : ℝ) * ∫ ε, D ε ∂μ)

Exact module and namespace context

Proof roadmap

1Use the actual finite law
Construct probability from normalized counting measure and actual cardinal2^n. Finite Bochner integrability is derived, and Fin.snoc gives the true balanced last-coordinate integral decomposition.
2Exact entropy chain
Let g(x)=sqrt((h(x,+)²+h(x,-)²)/2). Expanding both sides under the same finite law gives an equality: the last-coordinate two-point entropy plus the entropy of g². No conditional entropy bound is assumed.
3Genuine RMS contraction
The reverse two-dimensional Euclidean norm inequality yields the squared difference bound for g across each retained coordinate. Its proof derives the Cauchy-Schwarz cross term from (ad-bc)²≥0 and actual sqrt square identities.
4Integrate the two bounds with the exact energy split
Use the signed two-point theorem for the last coordinate and induction for g. Summing the RMS contraction and splitting the actual full-flip energy gives the same half constant. For n=0 there is one state, zero entropy and no energy.

Full assumptions and notation

All objects and hypotheses

Arbitrary natural n, including0; arbitrary signed real h on all Fin n→Bool.
Literal normalized counting law and full Function.update flip; probability/three L1 domains are outputs. No public inequality, smoothness or domain certificates.

Mathematical proof

1. Use the actual finite law

Construct probability from normalized counting measure and actual cardinal2^n. Finite Bochner integrability is derived, and Fin.snoc gives the true balanced last-coordinate integral decomposition.

\[\mathbb E_{\mu_{n+1}}F=\mathbb E_{\mu_n}\frac{F(x,+)+F(x,-)}2.\]

Corresponding Lean step

private probability; bernoulli_integral_succ_split; Integrable.of_finite

2. Exact entropy chain

Let g(x)=sqrt((h(x,+)²+h(x,-)²)/2). Expanding both sides under the same finite law gives an equality: the last-coordinate two-point entropy plus the entropy of g². No conditional entropy bound is assumed.

\[\operatorname{Ent}_{\mu_{n+1}}(h^2)=\mathbb E_{\mu_n}\operatorname{Ent}_2(h_+^2,h_-^2)+\operatorname{Ent}_{\mu_n}(g^2).\]

Corresponding Lean step

private rms_sq; entropy_chain

3. Genuine RMS contraction

The reverse two-dimensional Euclidean norm inequality yields the squared difference bound for g across each retained coordinate. Its proof derives the Cauchy-Schwarz cross term from (ad-bc)²≥0 and actual sqrt square identities.

\[(\sqrt{(a^2+b^2)/2}-\sqrt{(c^2+d^2)/2})^2\le\tfrac12((a-c)^2+(b-d)^2).\]

Corresponding Lean step

private rms_contraction; rms_energy

4. Integrate the two bounds with the exact energy split

Use the signed two-point theorem for the last coordinate and induction for g. Summing the RMS contraction and splitting the actual full-flip energy gives the same half constant. For n=0 there is one state, zero entropy and no energy.

\[\operatorname{Ent}(h^2)\le\tfrac12\mathbb E L+\tfrac12\mathbb E D_g\le\tfrac12\mathbb E(L+A)=\tfrac12\mathbb E D_h.\]

Corresponding Lean step

TwoPointEntropy.two_point_squared_entropy_le_half_sq_sub; private energy_chain; entropy_bound

Lean verification

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

Lean proof · bernoulli_function_logSobolev

Use the actual finite law; Exact entropy chain; Genuine RMS contraction; Integrate the two bounds with the exact energy split

Download module (.lean)

theorem bernoulli_function_logSobolev (n : ℕ) (h : (Fin n → Bool) → ℝ) :
    let μ : Measure (Fin n → Bool) :=
      (Fintype.card (Fin n → Bool) : ℝ≥0∞)⁻¹ • Measure.count
    let D := fun ε : Fin n → Bool =>
      ∑ j : Fin n, (h ε - h (Function.update ε j (!ε j))) ^ 2
    IsProbabilityMeasure μ ∧
      Integrable (fun ε => (h ε) ^ 2) μ ∧
      Integrable (fun ε => (h ε) ^ 2 * Real.log ((h ε) ^ 2)) μ ∧
      Integrable D μ ∧
      ((∫ ε, (h ε) ^ 2 * Real.log ((h ε) ^ 2) ∂μ) -
        (∫ ε, (h ε) ^ 2 ∂μ) * Real.log (∫ ε, (h ε) ^ 2 ∂μ) ≤
      (1 / 2 : ℝ) * ∫ ε, D ε ∂μ) := by
  dsimp only
  change IsProbabilityMeasure (bernoulliUniform n) ∧
    Integrable (fun ε => (h ε)^2) (bernoulliUniform n) ∧
    Integrable (fun ε => (h ε)^2 * log ((h ε)^2)) (bernoulliUniform n) ∧
    Integrable (gradientNormSq n h) (bernoulliUniform n) ∧
    entropy n h ≤ (1/2 : ℝ) * ∫ ε, gradientNormSq n h ε ∂bernoulliUniform n
  exact ⟨inferInstance, Integrable.of_finite, Integrable.of_finite,
    Integrable.of_finite, entropy_bound n h⟩

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BernoulliLogSobolev

Exact module and namespace context

Scope and omitted-condition boundaries

Genuine signed two-point and true finite Bool function LSI with exact half coefficient, derived probability/L1 domains; authored direct RMS-induction route. No GaussianLSI/T2/FIRST4.6/W2/bias/main/work/composition. Focused2653 passed actual n0/indicator/signed/normalizedRademacher n2 tests; all6 prints standard3 only. Independent wholeproof/blind/source/exactcommit admission, integration and exposition remain separate.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.TwoPointEntropy.two_point_squared_entropy_le_half_sq_sub

Mathlib API called (external library)

MeasureTheory.Integrable.of_finite
MeasureTheory.integral_fintype

Mathematical sources

bernoulli_logSobolev L1236 onward; actual law L113-L225; authored entropy/RMS induction replaces Han proof route — Genuine signed two-point and true finite Bool function LSI with exact half coefficient, derived probability/L1 domains; authored direct RMS-induction route. No GaussianLSI/T2/FIRST4.6/W2/bias/main/work/composition. Focused2653 passed actual n0/indicator/signed/normalizedRademacher n2 tests; all6 prints standard3 only. Independent wholeproof/blind/source/exactcommit admission, integration and exposition remain separate.

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