True finite Boolean function log-Sobolev inequality
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BernoulliLogSobolev.bernoulli_function_logSobolev · theorem · Teaching coverage
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.
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.
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 ε ∂μ)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.
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.
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.
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.
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.
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.BernoulliLogSobolevSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Positive Rothaus and true finite Boolean function-LSI. | 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. | same | Signed squares including zero are internally derived from positive Rothaus; exact arbitrary Boolean function-LSI is unchanged. |
| Han tensorization implementation upstream. | Authored exact entropy-chain/RMS induction. | same | Proof route disclosed; no caller certificate or statement weakening. |
| Gaussian limits and SPHMC LSI/T2/W2/main/composition. | 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. | unresolved | All downstream analytic/algorithm/cost dependencies remain open. |
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.
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
- 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
- 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.