Bench / discrete sampling
Tensorizing a two-point entropy bound without losing the flip constant
Discrete Sampling / Log-Concave Sampling · natural-language: L3 (author-assigned; calibration pending)
Why this difficulty?
Coordinate a conditional entropy identity, a nonlinear RMS contraction, a full coordinate-flip energy decomposition and dimension induction with exact normalization. Diagnose an arithmetic-mean shortcut using an explicit signed example. This is a multi-step finite-product proof, not empirical difficulty calibration.
Editorial review and exact formal-coverage boundary
AI editorial review accepted. This is not canonical theorem publication, full Lean coverage or empirical difficulty calibration.
- There is deliberately no aligned Lean QA or anonymous decoder report for this core. Acceptance is natural-language editorial acceptance, not a new formal theorem, Registry contribution, or theorem-publication seal.
- The explicit signed conditional-mean counterexample and the strict-convexity calculation distinguishing its true entropy from zero are checked mathematically here but are not conclusions of the cited public theorem.
- The public theorem does not state the pedagogical reverse-triangle proof, the comparison with coordinate-averaged energy, or the absence of a sampler convergence conclusion. The corresponding finite helper inequalities exist in its private source, while the explanatory interpretation remains prose.
- General tensorization, noncompact or Hilbert-space extensions, Gaussian limit passage and algorithmic convergence are outside this core. Family/split provenance and difficulty calibration are also not Lean facts.
Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.
Assumptions and conventions
- For each \(n\ge 0\) let \(Ωₙ=\{0,1\}^{n}\) with the full sigma algebra and uniform probability \(μₙ\), giving every configuration mass \(2^{-n}\). The space \(Ω_{0}\) has one configuration, not zero configurations. All functions considered are finite real-valued, with no positivity or normalization assumption on h.
- Write \(φ(s)=s\) log s for \(s>0\) and \(φ(0)=0\). Define \(Entₙ(h^{2})=Eμₙφ(h^{2})-φ(Eμₙh^{2})\). This convention agrees with \(h^{2}*Real.log(h^{2})\), including zeros.
- For \(j<n\), \(εʲ\) is obtained by toggling only coordinate j. Define \(Dₙh(ε)\) as the sum over all \(j<n\) of \((h(ε)-h(εʲ))^{2}\), not divided by n.
- You may use the existing two-point inequality, valid for all real a,b: \([φ(a^{2})+φ(b^{2})]/2-φ((a^{2}+b^{2})/2)\le (a-b)^{2}/2\). Do not assume the n-dimensional conclusion or an entropy tensorization theorem.
Natural-language question
Prove \(Entₙ(h^{2})\le (1/2)EμₙDₙh\) for all \(n\ge 0\) and all signed h. Construct the conditional RMS after separating the last coordinate; derive the entropy identity, its energy contraction and the dimension induction with the exact factor. Justify finite-law normalization and all integral domains, including \(n=0\) and zero values. Finally exhibit why replacing that RMS by the ordinary conditional mean can invalidate the entropy identity.
Reference mathematical proof
The uniform law has total mass \(2^{n}·2^{-n}=1\), also for \(n=0\). Every displayed finite real function is measurable and integrable on this finite space. The value \(φ(0)=0\) removes any fictitious strict-positivity requirement on h or its squared mean; no logarithm of a positive normalizer is used.
Separate a configuration into \((x,β)\in Ωₙ\times \{0,1\}\). Put a(x)=h(x,0), b(x)=h(x,1) and \[\begin{gathered}R(x)=\sqrt{\frac{a(x)^2+b(x)^2}{2}},\\\ell(x)=\frac{\phi(a(x)^2)+\phi(b(x)^2)}2-\phi(R(x)^2).\end{gathered}\] Uniform counting gives \(Eμₙ_{+1}g=Eμₙ[(g(x,0)+g(x,1))/2]\).
Because \(R^{2}=(a^{2}+b^{2})/2\), the squared mean is preserved: \(EμₙR^{2}=Eμₙ_{+1}h^{2}\). Add and subtract \(Eμₙφ(R^{2})\) to get the exact identity \[\operatorname{Ent}_{n+1}(h^2)=\mathbb E_{\mu_n}\ell+\operatorname{Ent}_n(R^2).\] All subtractions concern finite integrals. This is a proved identity for this finite law, not an invocation of general tensorization.
Define P(x) as the sum over \(j<n\) of \([(a(x)-a(xʲ))^{2}+(b(x)-b(xʲ))^{2}]/2\), and \(L(x)=(a(x)-b(x))^{2}\). Toggling a prefix coordinate preserves the last bit; toggling the last bit exchanges the two slices. Therefore \[\mathbb E_{\mu_{n+1}}D_{n+1}h=\mathbb E_{\mu_n}(P+L).\] Averaging the two last-coordinate square differences gives L, not L/2: they are equal after reversing the subtraction.
For u=(a,b)/√2 and v=(c,d)/√2 in \(\mathbb{R}^{2}\), the reverse triangle inequality gives \[(\sqrt{(a^2+b^2)/2}-\sqrt{(c^2+d^2)/2})^2\le\frac{(a-c)^2+(b-d)^2}{2}.\] Apply this to each pair of neighboring prefix configurations and sum over coordinates. It yields \(DₙR\le P\) pointwise and hence \(EμₙDₙR\le EμₙP\). The existing Lean helper proves this same RMS contraction by Cauchy–Schwarz algebra.
The supplied two-point inequality gives \(ℓ(x)\le L(x)/2\) for every prefix x, for arbitrary signs and zeros. Integrating preserves that inequality. Assuming the n-dimensional bound for R, combine the three ingredients: \[\operatorname{Ent}_{n+1}(h^2)\le\frac12\mathbb E L+\frac12\mathbb E D_nR\le\frac12\mathbb E(L+P)=\frac12\mathbb E D_{n+1}h.\] This keeps the same factor at every dimension.
At \(n=0\), there is one atom, so \(Eφ(h^{2})=φ(Eh^{2})\) and entropy is zero; the empty coordinate sum is zero as well. This starts induction without dividing by n or assuming a positive squared mean. It also covers the identically zero function in every dimension.
For a counterexample to replacing RMS by conditional mean, take a prefix \(x\in \{0,1\}\), set A(0)=1,A(1)=2, and let \(h(x,0)=A(x)\), \(h(x,1)=-A(x)\). Then the conditional mean M is identically zero and the actual local entropy ℓ is identically zero. But \[\operatorname{Ent}_2(h^2)=\frac{\phi(1)+\phi(4)}2-\phi(5/2)>0,\] by strict convexity of \(φ\) on the positive interval [1,4]. The proposed replacement would give \(0+Ent_{1}(M^{2})=0\), contradicting the identity. The squared mean must be preserved; averaging signs does not do that.
The energy here is the full sum of coordinate-flip squared differences under a probability law. Replacing it by an average over coordinates changes constants. The result is a finite functional inequality, not by itself a convergence theorem for a chosen discrete-time sampler or a noncompact Gaussian inequality.
Formal support and missing Lean alignment
The folded exact module includes the real normalized-counting law, finite-integrability obligations and private entropy/RMS induction. Its private entropy_chain, energy_chain and rms_energy helpers implement the three mathematical ingredients above; these short helper names are not advertised as new public declarations. The final public theorem packages the bound and \(probability/L^{1}\) conclusions by calling the proved induction. The module is supplied intact, retaining its upstream Apache notices, authors and pinned SLT provenance. There is no aligned Lean QA: extracting only its final constructor call would test a wrapper rather than reconstruct the substantive induction. The arithmetic-mean counterexample is original prose, not an extra compiled conclusion.
Supporting library Lean (not an aligned QA task)
/-
Copyright (c) 2026 Yuanhe Zhang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yuanhe Zhang, Jason D. Lee, Fanghui Liu
-/
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.TwoPointEntropy
import Mathlib.MeasureTheory.Measure.Count
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.Data.Fin.Tuple.Basic
/-!
# Bernoulli function log-Sobolev inequality
The genuine law is normalized counting measure. Law/snoc helpers are minimally
adapted from the pinned SLT BernoulliLSI source (Apache 2.0, commit
d0f506f0a695018265dccb33bcb05e2f5ca1c876). The entropy/RMS induction below is
an authored alternative to Han tensorization. Gaussian limits remain separate.
-/
open MeasureTheory ProbabilityTheory Real Set Filter Function
open scoped ENNReal NNReal BigOperators Topology
noncomputable section
namespace AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BernoulliLogSobolev
variable {n : ℕ}
private def flipCoord (j : Fin n) (ε : Fin n → Bool) : Fin n → Bool :=
update ε j (!ε j)
@[simp] private theorem flipCoord_same (j : Fin n) (ε : Fin n → Bool) :
(flipCoord j ε) j = !ε j := by
simp [flipCoord]
private theorem flipCoord_noteq (j i : Fin n) (ε : Fin n → Bool) (h : i ≠ j) :
(flipCoord j ε) i = ε i := by
simp only [flipCoord, update_of_ne h]
private def bernoulliUniform (n : ℕ) : Measure (Fin n → Bool) :=
((Finset.univ : Finset (Fin n → Bool)).card : ℝ≥0∞)⁻¹ • Measure.count
private theorem card_fin_bool (n : ℕ) : Finset.card (Finset.univ : Finset (Fin n → Bool)) = 2^n := by
simp only [Finset.card_univ, Fintype.card_fun, Fintype.card_fin, Fintype.card_bool]
private theorem bernoulli_integral_eq_sum {n : ℕ} (f : (Fin n → Bool) → ℝ) :
∫ ε, f ε ∂(bernoulliUniform n) = (∑ ε : Fin n → Bool, f ε) / 2^n := by
unfold bernoulliUniform
rw [integral_smul_measure]
rw [MeasureTheory.integral_fintype (Integrable.of_finite : Integrable f Measure.count)]
rw [card_fin_bool n]
simp only [Nat.cast_pow, Nat.cast_ofNat, smul_eq_mul, count_real_singleton, one_mul]
rw [ENNReal.toReal_inv, ENNReal.toReal_pow, ENNReal.toReal_ofNat]
ring
private theorem sum_fin_succ_bool_eq_sum_snoc {n : ℕ} (f : (Fin (n+1) → Bool) → ℝ) :
∑ ε : Fin (n+1) → Bool, f ε =
∑ ε' : Fin n → Bool, (f (Fin.snoc ε' true) + f (Fin.snoc ε' false)) := by
-- Use Fin.snocEquiv: (Fin (n+1) → α) ≃ α × (Fin n → α) at last position
-- But we need (Fin n → α) × α, so use Prod.swap
let h_equiv : (Fin (n+1) → Bool) ≃ (Fin n → Bool) × Bool :=
(Fin.snocEquiv (fun _ => Bool)).symm.trans (Equiv.prodComm _ _)
calc ∑ ε : Fin (n+1) → Bool, f ε
= ∑ p : (Fin n → Bool) × Bool, f (h_equiv.symm p) := by
rw [Fintype.sum_equiv h_equiv.symm]
simp
_ = ∑ ε' : Fin n → Bool, ∑ b : Bool, f (h_equiv.symm (ε', b)) := by
rw [Fintype.sum_prod_type]
_ = ∑ ε' : Fin n → Bool, (f (h_equiv.symm (ε', true)) + f (h_equiv.symm (ε', false))) := by
congr 1
ext ε'
simp only [Fintype.sum_bool]
_ = ∑ ε' : Fin n → Bool, (f (Fin.snoc ε' true) + f (Fin.snoc ε' false)) := by
congr 1
private theorem bernoulli_integral_succ_split {n : ℕ} (f : (Fin (n+1) → Bool) → ℝ) :
∫ ε, f ε ∂(bernoulliUniform (n+1)) =
∫ ε', (f (Fin.snoc ε' true) + f (Fin.snoc ε' false)) / 2 ∂(bernoulliUniform n) := by
rw [bernoulli_integral_eq_sum, bernoulli_integral_eq_sum]
rw [sum_fin_succ_bool_eq_sum_snoc]
rw [pow_succ]
rw [Finset.sum_div]
-- Goal: ∑ i, (f true + f false) / (2^n * 2) = (∑ i, (f true + f false) / 2) / 2^n
-- Rewrite RHS: (∑ (x/2)) / 2^n = ∑ (x / (2 * 2^n)) = ∑ (x / (2^n * 2))
rw [Finset.sum_div]
congr 1
ext i
ring
private def gradientNormSq (n : ℕ) (h : (Fin n → Bool) → ℝ) (ε : Fin n → Bool) : ℝ :=
∑ j : Fin n, (h ε - h (flipCoord j ε))^2
private theorem gradientNormSq_succ_decomposition {n : ℕ} (h : (Fin (n + 1) → Bool) → ℝ)
(ε : Fin (n + 1) → Bool) :
gradientNormSq (n + 1) h ε =
(∑ j : Fin n, (h ε - h (flipCoord (Fin.castSucc j) ε))^2) +
(h ε - h (flipCoord (Fin.last n) ε))^2 := by
simp only [gradientNormSq]
rw [Fin.sum_univ_castSucc]
private theorem flipCoord_last_snoc {n : ℕ} (ε' : Fin n → Bool) (b : Bool) :
flipCoord (Fin.last n) (Fin.snoc ε' b) = Fin.snoc ε' (!b) := by
ext i
by_cases h : i = Fin.last n
· simp only [h, flipCoord_same, Fin.snoc_last]
· have hi : i.val < n := by
have hlt := i.isLt
have hne : i.val ≠ n := by
intro heq
apply h; ext; simp [Fin.last, heq]
omega
have hne' : i ≠ Fin.last n := fun heq => h heq
rw [flipCoord_noteq (Fin.last n) i _ hne']
simp only [Fin.snoc, hi, ↓reduceDIte]
private theorem flipCoord_castSucc_snoc {n : ℕ} (j : Fin n) (ε' : Fin n → Bool) (b : Bool) :
flipCoord (Fin.castSucc j) (Fin.snoc ε' b) = Fin.snoc (flipCoord j ε') b := by
ext i
by_cases hi_last : i = Fin.last n
· -- i is the last index
simp only [hi_last, Fin.snoc_last]
have hne : Fin.last n ≠ Fin.castSucc j := by
intro heq
have hval : (Fin.last n).val = (Fin.castSucc j).val := congrArg Fin.val heq
simp only [Fin.last, Fin.val_castSucc] at hval
omega
rw [flipCoord_noteq (Fin.castSucc j) (Fin.last n) _ hne]
simp [Fin.snoc]
· -- i is not the last index
have hi : i.val < n := by
have hlt := i.isLt
have hne : i.val ≠ n := by
intro heq
apply hi_last; ext; simp [Fin.last, heq]
omega
by_cases hj : i = Fin.castSucc j
· -- i = castSucc j
subst hj
simp only [flipCoord_same, Fin.snoc]
have hi' : (Fin.castSucc j).val < n := by simp [Fin.val_castSucc]
simp only [hi', ↓reduceDIte]
-- Need to show !ε'(castLT (castSucc j)) = flipCoord j ε' (castLT (castSucc j))
have hcast_eq : Fin.castLT (Fin.castSucc j) hi' = j := by
ext; simp [Fin.castLT, Fin.castSucc]
simp only [hcast_eq, flipCoord_same, cast_eq]
· -- i ≠ castSucc j
have hne' : i ≠ Fin.castSucc j := hj
rw [flipCoord_noteq (Fin.castSucc j) i _ hne']
simp only [Fin.snoc, hi, ↓reduceDIte]
have hj' : Fin.castLT i hi ≠ j := by
intro heq
apply hj
ext
simp only [Fin.val_castSucc]
exact congrArg Fin.val heq
rw [flipCoord_noteq j (Fin.castLT i hi) _ hj']
private instance probability (n : ℕ) : IsProbabilityMeasure (bernoulliUniform n) := by
constructor
unfold bernoulliUniform
simp only [Measure.smul_apply, smul_eq_mul]
rw [Measure.count_apply_finite Set.univ Set.finite_univ]
simp only [Set.Finite.toFinset_univ, Finset.card_univ, Fintype.card_fun,
Fintype.card_fin, Fintype.card_bool, Nat.cast_pow, Nat.cast_ofNat]
rw [ENNReal.inv_mul_cancel]
· exact pow_ne_zero _ (by norm_num)
· exact ENNReal.pow_ne_top (by norm_num : (2 : ℝ≥0∞) ≠ ⊤)
/-- Reverse Euclidean norm inequality, squared, at the actual conditional RMS. -/
private theorem rms_contraction (a b c d : ℝ) :
(sqrt ((a^2+b^2)/2) - sqrt ((c^2+d^2)/2))^2 ≤
((a-c)^2+(b-d)^2)/2 := by
set s := sqrt ((a^2+b^2)/2)
set t := sqrt ((c^2+d^2)/2)
have hs : 0 ≤ s := sqrt_nonneg _
have ht : 0 ≤ t := sqrt_nonneg _
have hs2 : s^2 = (a^2+b^2)/2 := sq_sqrt (by positivity)
have ht2 : t^2 = (c^2+d^2)/2 := sq_sqrt (by positivity)
have hcs : (a*c+b*d)^2 ≤ (2*s*t)^2 := by
nlinarith [sq_nonneg (a*d-b*c)]
have hst : 0 ≤ 2*s*t := by positivity
have hcross : a*c+b*d ≤ 2*s*t := by
nlinarith [sq_nonneg (a*c+b*d-2*s*t)]
nlinarith
private def entropy (n : ℕ) (h : (Fin n → Bool) → ℝ) : ℝ :=
(∫ x, h x^2 * log (h x^2) ∂bernoulliUniform n) -
(∫ x, h x^2 ∂bernoulliUniform n) * log (∫ x, h x^2 ∂bernoulliUniform n)
private def rms {n : ℕ} (h : (Fin (n+1) → Bool) → ℝ) (x : Fin n → Bool) : ℝ :=
sqrt ((h (Fin.snoc x true)^2 + h (Fin.snoc x false)^2)/2)
private theorem rms_sq (h : (Fin (n+1) → Bool) → ℝ) (x : Fin n → Bool) :
rms h x^2 = (h (Fin.snoc x true)^2 + h (Fin.snoc x false)^2)/2 :=
sq_sqrt (by positivity)
private def localEntropy {n : ℕ} (h : (Fin (n+1) → Bool) → ℝ)
(x : Fin n → Bool) : ℝ :=
(h (Fin.snoc x true)^2 * log (h (Fin.snoc x true)^2) +
h (Fin.snoc x false)^2 * log (h (Fin.snoc x false)^2))/2 -
(rms h x)^2 * log ((rms h x)^2)
private theorem entropy_chain (h : (Fin (n+1) → Bool) → ℝ) :
entropy (n+1) h = (∫ x, localEntropy h x ∂bernoulliUniform n) + entropy n (rms h) := by
unfold entropy localEntropy
rw [bernoulli_integral_succ_split, bernoulli_integral_succ_split,
integral_sub (Integrable.of_finite) (Integrable.of_finite)]
simp_rw [rms_sq]
ring
private def prefixEnergy {n : ℕ} (h : (Fin (n+1) → Bool) → ℝ)
(x : Fin n → Bool) : ℝ :=
∑ j : Fin n,
((h (Fin.snoc x true)-h (Fin.snoc (flipCoord j x) true))^2 +
(h (Fin.snoc x false)-h (Fin.snoc (flipCoord j x) false))^2)/2
private def lastEnergy {n : ℕ} (h : (Fin (n+1) → Bool) → ℝ)
(x : Fin n → Bool) : ℝ :=
(h (Fin.snoc x true)-h (Fin.snoc x false))^2
private theorem energy_chain (h : (Fin (n+1) → Bool) → ℝ) :
(∫ x, gradientNormSq (n+1) h x ∂bernoulliUniform (n+1)) =
∫ x, prefixEnergy h x + lastEnergy h x ∂bernoulliUniform n := by
rw [bernoulli_integral_succ_split]
apply integral_congr_ae
filter_upwards [] with x
simp only [gradientNormSq_succ_decomposition, flipCoord_castSucc_snoc,
flipCoord_last_snoc, Bool.not_true, Bool.not_false, prefixEnergy, lastEnergy]
rw [← Finset.sum_div, Finset.sum_add_distrib]
have hs : (h (Fin.snoc x false)-h (Fin.snoc x true))^2 =
(h (Fin.snoc x true)-h (Fin.snoc x false))^2 := by ring
rw [hs]
ring
private theorem rms_energy (h : (Fin (n+1) → Bool) → ℝ) (x : Fin n → Bool) :
gradientNormSq n (rms h) x ≤ prefixEnergy h x := by
unfold gradientNormSq prefixEnergy
apply Finset.sum_le_sum
intro j _
exact rms_contraction _ _ _ _
private theorem entropy_bound (n : ℕ) (h : (Fin n → Bool) → ℝ) :
entropy n h ≤ (1/2 : ℝ) * ∫ x, gradientNormSq n h x ∂bernoulliUniform n := by
induction n with
| zero =>
unfold entropy gradientNormSq
simp only [bernoulli_integral_eq_sum]
simp
| succ n ih =>
have hlocal : (∫ x, localEntropy h x ∂bernoulliUniform n) ≤
(1/2 : ℝ) * ∫ x, lastEnergy h x ∂bernoulliUniform n := by
rw [← integral_const_mul]
apply integral_mono (Integrable.of_finite) (Integrable.of_finite)
intro x
unfold localEntropy lastEnergy
rw [rms_sq]
calc
_ ≤ (h (Fin.snoc x true)-h (Fin.snoc x false))^2/2 :=
TwoPointEntropy.two_point_squared_entropy_le_half_sq_sub _ _
_ = _ := by ring
have hprefix : (∫ x, gradientNormSq n (rms h) x ∂bernoulliUniform n) ≤
∫ x, prefixEnergy h x ∂bernoulliUniform n :=
integral_mono (Integrable.of_finite) (Integrable.of_finite) (rms_energy h)
rw [entropy_chain, energy_chain,
integral_add (Integrable.of_finite) (Integrable.of_finite)]
have hi := ih (rms h)
linarith
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
Download exact supporting module · Uses the project toolchain and its listed imports; not a standalone replacement QA proof.
Assessment rubric · 4 points
- Normalizes the finite law, checks finite measurability/integrability and derives the exact conditional entropy identity using preservation of the squared mean. (1 point)
- Proves the RMS contraction and the prefix/last-coordinate energy decomposition, without losing the factor from averaging the two orientations of the last flip. (1 point)
- Combines the given two-point bound with dimension induction to obtain the exact 1/2 constant, including the singleton \(n=0\) base and signed/zero functions. (1 point)
- Gives a valid explicit failure of the ordinary conditional-mean entropy identity, such as the sign-cancelling unequal-amplitude example, rather than asserting a counterexample to the true log-Sobolev inequality. (1 point)
Lean view: not yet aligned
The folded exact module includes the real normalized-counting law, finite-integrability obligations and private entropy/RMS induction. Its private entropy_chain, energy_chain and rms_energy helpers implement the three mathematical ingredients above; these short helper names are not advertised as new public declarations. The final public theorem packages the bound and \(probability/L^{1}\) conclusions by calling the proved induction. The module is supplied intact, retaining its upstream Apache notices, authors and pinned SLT provenance. There is no aligned Lean QA: extracting only its final constructor call would test a wrapper rather than reconstruct the substantive induction. The arithmetic-mean counterexample is original prose, not an extra compiled conclusion.
Supporting library Lean (not an aligned QA task)
/-
Copyright (c) 2026 Yuanhe Zhang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yuanhe Zhang, Jason D. Lee, Fanghui Liu
-/
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.TwoPointEntropy
import Mathlib.MeasureTheory.Measure.Count
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.Data.Fin.Tuple.Basic
/-!
# Bernoulli function log-Sobolev inequality
The genuine law is normalized counting measure. Law/snoc helpers are minimally
adapted from the pinned SLT BernoulliLSI source (Apache 2.0, commit
d0f506f0a695018265dccb33bcb05e2f5ca1c876). The entropy/RMS induction below is
an authored alternative to Han tensorization. Gaussian limits remain separate.
-/
open MeasureTheory ProbabilityTheory Real Set Filter Function
open scoped ENNReal NNReal BigOperators Topology
noncomputable section
namespace AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BernoulliLogSobolev
variable {n : ℕ}
private def flipCoord (j : Fin n) (ε : Fin n → Bool) : Fin n → Bool :=
update ε j (!ε j)
@[simp] private theorem flipCoord_same (j : Fin n) (ε : Fin n → Bool) :
(flipCoord j ε) j = !ε j := by
simp [flipCoord]
private theorem flipCoord_noteq (j i : Fin n) (ε : Fin n → Bool) (h : i ≠ j) :
(flipCoord j ε) i = ε i := by
simp only [flipCoord, update_of_ne h]
private def bernoulliUniform (n : ℕ) : Measure (Fin n → Bool) :=
((Finset.univ : Finset (Fin n → Bool)).card : ℝ≥0∞)⁻¹ • Measure.count
private theorem card_fin_bool (n : ℕ) : Finset.card (Finset.univ : Finset (Fin n → Bool)) = 2^n := by
simp only [Finset.card_univ, Fintype.card_fun, Fintype.card_fin, Fintype.card_bool]
private theorem bernoulli_integral_eq_sum {n : ℕ} (f : (Fin n → Bool) → ℝ) :
∫ ε, f ε ∂(bernoulliUniform n) = (∑ ε : Fin n → Bool, f ε) / 2^n := by
unfold bernoulliUniform
rw [integral_smul_measure]
rw [MeasureTheory.integral_fintype (Integrable.of_finite : Integrable f Measure.count)]
rw [card_fin_bool n]
simp only [Nat.cast_pow, Nat.cast_ofNat, smul_eq_mul, count_real_singleton, one_mul]
rw [ENNReal.toReal_inv, ENNReal.toReal_pow, ENNReal.toReal_ofNat]
ring
private theorem sum_fin_succ_bool_eq_sum_snoc {n : ℕ} (f : (Fin (n+1) → Bool) → ℝ) :
∑ ε : Fin (n+1) → Bool, f ε =
∑ ε' : Fin n → Bool, (f (Fin.snoc ε' true) + f (Fin.snoc ε' false)) := by
-- Use Fin.snocEquiv: (Fin (n+1) → α) ≃ α × (Fin n → α) at last position
-- But we need (Fin n → α) × α, so use Prod.swap
let h_equiv : (Fin (n+1) → Bool) ≃ (Fin n → Bool) × Bool :=
(Fin.snocEquiv (fun _ => Bool)).symm.trans (Equiv.prodComm _ _)
calc ∑ ε : Fin (n+1) → Bool, f ε
= ∑ p : (Fin n → Bool) × Bool, f (h_equiv.symm p) := by
rw [Fintype.sum_equiv h_equiv.symm]
simp
_ = ∑ ε' : Fin n → Bool, ∑ b : Bool, f (h_equiv.symm (ε', b)) := by
rw [Fintype.sum_prod_type]
_ = ∑ ε' : Fin n → Bool, (f (h_equiv.symm (ε', true)) + f (h_equiv.symm (ε', false))) := by
congr 1
ext ε'
simp only [Fintype.sum_bool]
_ = ∑ ε' : Fin n → Bool, (f (Fin.snoc ε' true) + f (Fin.snoc ε' false)) := by
congr 1
private theorem bernoulli_integral_succ_split {n : ℕ} (f : (Fin (n+1) → Bool) → ℝ) :
∫ ε, f ε ∂(bernoulliUniform (n+1)) =
∫ ε', (f (Fin.snoc ε' true) + f (Fin.snoc ε' false)) / 2 ∂(bernoulliUniform n) := by
rw [bernoulli_integral_eq_sum, bernoulli_integral_eq_sum]
rw [sum_fin_succ_bool_eq_sum_snoc]
rw [pow_succ]
rw [Finset.sum_div]
-- Goal: ∑ i, (f true + f false) / (2^n * 2) = (∑ i, (f true + f false) / 2) / 2^n
-- Rewrite RHS: (∑ (x/2)) / 2^n = ∑ (x / (2 * 2^n)) = ∑ (x / (2^n * 2))
rw [Finset.sum_div]
congr 1
ext i
ring
private def gradientNormSq (n : ℕ) (h : (Fin n → Bool) → ℝ) (ε : Fin n → Bool) : ℝ :=
∑ j : Fin n, (h ε - h (flipCoord j ε))^2
private theorem gradientNormSq_succ_decomposition {n : ℕ} (h : (Fin (n + 1) → Bool) → ℝ)
(ε : Fin (n + 1) → Bool) :
gradientNormSq (n + 1) h ε =
(∑ j : Fin n, (h ε - h (flipCoord (Fin.castSucc j) ε))^2) +
(h ε - h (flipCoord (Fin.last n) ε))^2 := by
simp only [gradientNormSq]
rw [Fin.sum_univ_castSucc]
private theorem flipCoord_last_snoc {n : ℕ} (ε' : Fin n → Bool) (b : Bool) :
flipCoord (Fin.last n) (Fin.snoc ε' b) = Fin.snoc ε' (!b) := by
ext i
by_cases h : i = Fin.last n
· simp only [h, flipCoord_same, Fin.snoc_last]
· have hi : i.val < n := by
have hlt := i.isLt
have hne : i.val ≠ n := by
intro heq
apply h; ext; simp [Fin.last, heq]
omega
have hne' : i ≠ Fin.last n := fun heq => h heq
rw [flipCoord_noteq (Fin.last n) i _ hne']
simp only [Fin.snoc, hi, ↓reduceDIte]
private theorem flipCoord_castSucc_snoc {n : ℕ} (j : Fin n) (ε' : Fin n → Bool) (b : Bool) :
flipCoord (Fin.castSucc j) (Fin.snoc ε' b) = Fin.snoc (flipCoord j ε') b := by
ext i
by_cases hi_last : i = Fin.last n
· -- i is the last index
simp only [hi_last, Fin.snoc_last]
have hne : Fin.last n ≠ Fin.castSucc j := by
intro heq
have hval : (Fin.last n).val = (Fin.castSucc j).val := congrArg Fin.val heq
simp only [Fin.last, Fin.val_castSucc] at hval
omega
rw [flipCoord_noteq (Fin.castSucc j) (Fin.last n) _ hne]
simp [Fin.snoc]
· -- i is not the last index
have hi : i.val < n := by
have hlt := i.isLt
have hne : i.val ≠ n := by
intro heq
apply hi_last; ext; simp [Fin.last, heq]
omega
by_cases hj : i = Fin.castSucc j
· -- i = castSucc j
subst hj
simp only [flipCoord_same, Fin.snoc]
have hi' : (Fin.castSucc j).val < n := by simp [Fin.val_castSucc]
simp only [hi', ↓reduceDIte]
-- Need to show !ε'(castLT (castSucc j)) = flipCoord j ε' (castLT (castSucc j))
have hcast_eq : Fin.castLT (Fin.castSucc j) hi' = j := by
ext; simp [Fin.castLT, Fin.castSucc]
simp only [hcast_eq, flipCoord_same, cast_eq]
· -- i ≠ castSucc j
have hne' : i ≠ Fin.castSucc j := hj
rw [flipCoord_noteq (Fin.castSucc j) i _ hne']
simp only [Fin.snoc, hi, ↓reduceDIte]
have hj' : Fin.castLT i hi ≠ j := by
intro heq
apply hj
ext
simp only [Fin.val_castSucc]
exact congrArg Fin.val heq
rw [flipCoord_noteq j (Fin.castLT i hi) _ hj']
private instance probability (n : ℕ) : IsProbabilityMeasure (bernoulliUniform n) := by
constructor
unfold bernoulliUniform
simp only [Measure.smul_apply, smul_eq_mul]
rw [Measure.count_apply_finite Set.univ Set.finite_univ]
simp only [Set.Finite.toFinset_univ, Finset.card_univ, Fintype.card_fun,
Fintype.card_fin, Fintype.card_bool, Nat.cast_pow, Nat.cast_ofNat]
rw [ENNReal.inv_mul_cancel]
· exact pow_ne_zero _ (by norm_num)
· exact ENNReal.pow_ne_top (by norm_num : (2 : ℝ≥0∞) ≠ ⊤)
/-- Reverse Euclidean norm inequality, squared, at the actual conditional RMS. -/
private theorem rms_contraction (a b c d : ℝ) :
(sqrt ((a^2+b^2)/2) - sqrt ((c^2+d^2)/2))^2 ≤
((a-c)^2+(b-d)^2)/2 := by
set s := sqrt ((a^2+b^2)/2)
set t := sqrt ((c^2+d^2)/2)
have hs : 0 ≤ s := sqrt_nonneg _
have ht : 0 ≤ t := sqrt_nonneg _
have hs2 : s^2 = (a^2+b^2)/2 := sq_sqrt (by positivity)
have ht2 : t^2 = (c^2+d^2)/2 := sq_sqrt (by positivity)
have hcs : (a*c+b*d)^2 ≤ (2*s*t)^2 := by
nlinarith [sq_nonneg (a*d-b*c)]
have hst : 0 ≤ 2*s*t := by positivity
have hcross : a*c+b*d ≤ 2*s*t := by
nlinarith [sq_nonneg (a*c+b*d-2*s*t)]
nlinarith
private def entropy (n : ℕ) (h : (Fin n → Bool) → ℝ) : ℝ :=
(∫ x, h x^2 * log (h x^2) ∂bernoulliUniform n) -
(∫ x, h x^2 ∂bernoulliUniform n) * log (∫ x, h x^2 ∂bernoulliUniform n)
private def rms {n : ℕ} (h : (Fin (n+1) → Bool) → ℝ) (x : Fin n → Bool) : ℝ :=
sqrt ((h (Fin.snoc x true)^2 + h (Fin.snoc x false)^2)/2)
private theorem rms_sq (h : (Fin (n+1) → Bool) → ℝ) (x : Fin n → Bool) :
rms h x^2 = (h (Fin.snoc x true)^2 + h (Fin.snoc x false)^2)/2 :=
sq_sqrt (by positivity)
private def localEntropy {n : ℕ} (h : (Fin (n+1) → Bool) → ℝ)
(x : Fin n → Bool) : ℝ :=
(h (Fin.snoc x true)^2 * log (h (Fin.snoc x true)^2) +
h (Fin.snoc x false)^2 * log (h (Fin.snoc x false)^2))/2 -
(rms h x)^2 * log ((rms h x)^2)
private theorem entropy_chain (h : (Fin (n+1) → Bool) → ℝ) :
entropy (n+1) h = (∫ x, localEntropy h x ∂bernoulliUniform n) + entropy n (rms h) := by
unfold entropy localEntropy
rw [bernoulli_integral_succ_split, bernoulli_integral_succ_split,
integral_sub (Integrable.of_finite) (Integrable.of_finite)]
simp_rw [rms_sq]
ring
private def prefixEnergy {n : ℕ} (h : (Fin (n+1) → Bool) → ℝ)
(x : Fin n → Bool) : ℝ :=
∑ j : Fin n,
((h (Fin.snoc x true)-h (Fin.snoc (flipCoord j x) true))^2 +
(h (Fin.snoc x false)-h (Fin.snoc (flipCoord j x) false))^2)/2
private def lastEnergy {n : ℕ} (h : (Fin (n+1) → Bool) → ℝ)
(x : Fin n → Bool) : ℝ :=
(h (Fin.snoc x true)-h (Fin.snoc x false))^2
private theorem energy_chain (h : (Fin (n+1) → Bool) → ℝ) :
(∫ x, gradientNormSq (n+1) h x ∂bernoulliUniform (n+1)) =
∫ x, prefixEnergy h x + lastEnergy h x ∂bernoulliUniform n := by
rw [bernoulli_integral_succ_split]
apply integral_congr_ae
filter_upwards [] with x
simp only [gradientNormSq_succ_decomposition, flipCoord_castSucc_snoc,
flipCoord_last_snoc, Bool.not_true, Bool.not_false, prefixEnergy, lastEnergy]
rw [← Finset.sum_div, Finset.sum_add_distrib]
have hs : (h (Fin.snoc x false)-h (Fin.snoc x true))^2 =
(h (Fin.snoc x true)-h (Fin.snoc x false))^2 := by ring
rw [hs]
ring
private theorem rms_energy (h : (Fin (n+1) → Bool) → ℝ) (x : Fin n → Bool) :
gradientNormSq n (rms h) x ≤ prefixEnergy h x := by
unfold gradientNormSq prefixEnergy
apply Finset.sum_le_sum
intro j _
exact rms_contraction _ _ _ _
private theorem entropy_bound (n : ℕ) (h : (Fin n → Bool) → ℝ) :
entropy n h ≤ (1/2 : ℝ) * ∫ x, gradientNormSq n h x ∂bernoulliUniform n := by
induction n with
| zero =>
unfold entropy gradientNormSq
simp only [bernoulli_integral_eq_sum]
simp
| succ n ih =>
have hlocal : (∫ x, localEntropy h x ∂bernoulliUniform n) ≤
(1/2 : ℝ) * ∫ x, lastEnergy h x ∂bernoulliUniform n := by
rw [← integral_const_mul]
apply integral_mono (Integrable.of_finite) (Integrable.of_finite)
intro x
unfold localEntropy lastEnergy
rw [rms_sq]
calc
_ ≤ (h (Fin.snoc x true)-h (Fin.snoc x false))^2/2 :=
TwoPointEntropy.two_point_squared_entropy_le_half_sq_sub _ _
_ = _ := by ring
have hprefix : (∫ x, gradientNormSq n (rms h) x ∂bernoulliUniform n) ≤
∫ x, prefixEnergy h x ∂bernoulliUniform n :=
integral_mono (Integrable.of_finite) (Integrable.of_finite) (rms_energy h)
rw [entropy_chain, energy_chain,
integral_add (Integrable.of_finite) (Integrable.of_finite)]
have hi := ih (rms h)
linarith
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
Download exact supporting module · Uses the project toolchain and its listed imports; not a standalone replacement QA proof.
This support theorem does not certify the complete QA or its explanatory counterexamples.
What this does—and does not—verify
An original NL exercise over an existing compiled finite-product theorem, with no equivalent fixed Lean task and no new production declaration. The supporting module does prove the displayed log-Sobolev bound with actual normalization and \(L^{1}\) conclusions, but not the separate counterexample or every explanatory sentence. General entropy tensorization, noncompact/Hilbert extensions and sampler convergence remain outside this QA.
Existing library mathematics reused; no new mathematical leaf or paper-completion credit. The editorial panel records the exact current review scope and remaining unformalized explanation.
Sources, graph location and dependencies
Original library-grounded formulation and proof guide, not copied textbook prose. The exact BernoulliLogSobolev module credits minimally adapted law/snoc helpers to the Apache-2.0 SLT BernoulliLSI source at commit d0f506f0a695018265dccb33bcb05e2f5ca1c876, retaining its Yuanhe Zhang / Jason D. Lee / Fanghui Liu notice; its entropy/RMS induction is the local authored alternative. Its actual consumer GaussianCompactLogSobolev.compact_gaussian_logSobolev applies the finite bound to normalized Rademacher sums. This core shares a public family with sogb-028; their common source/proof route must not be split into nominally independent train/test families. No restricted material or external dataset is used.
Exact local source and full context · Locate the existing Lean declaration
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BernoulliLogSobolev.bernoulli_function_logSobolev
ASTIS formal support (not an equivalent QA)
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.TwoPointEntropy.two_point_squared_entropy_le_half_sq_sub
Mathlib facts / definitions
Integrable.of_finiteReal.sq_sqrtFin.snocEquivFin.sum_univ_castSuccFinset.sum_le_sum
Additional source-bound support (not full QA certification)
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.TwoPointEntropy.two_point_squared_entropy_le_half_sq_sub· LF source SHA-256:11ccdd552603eb128af3a8de174b8dd2d7d60a003423c88b7413d018be6a32b0
Binding SHA-256: 7da6ccd4e2fbac80e8597c8d5421fb083791810652c7a3838214fa305763cf89