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

BernoulliLogSobolev: 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. True finite Boolean function log-Sobolev inequality
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

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.

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

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

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

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

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

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 ε ∂μ) := 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

Mathlib API called (external library)

  • MeasureTheory.Integrable.of_finite
  • MeasureTheory.integral_fintype

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.