From the Boolean cube to compact Gaussian log-Sobolev

1. Each \(μₘ\) is a genuine probability law, and Sₘ is measurable on the finite configuration space. The available CLT identifies its actual pushforward distribution, not just an unrelated Gaussian-looking sequence. Working with \(m=n+1\) avoids using the inverse-square-root scaling at zero in the asymptotic calculation.

2. Since f is \(C^{2}\) and compactly supported, \(f^{2}\), \(φ(f^{2})\) and \((f′)^{2}\) are continuous compactly supported functions. In particular f′ is genuinely continuous and supported in the closed support of f. Continuity of \(s\mapsto s\) log s at \(s=0\) is understood via its zero extension; continuity of log alone at zero would be false. These observables are bounded, measurable and integrable under \(γ\) and every finite law.

3. Weak convergence may therefore be tested against each of these three bounded continuous observables. The pushforward integral formula converts the resulting expectations to integrals over the actual cube. Put \[A_m=\mathbb E f(S_m)^2,\quad B_m=\mathbb E\phi(f(S_m)^2),\quad C_m=\mathbb E f'(S_m)^2.\] They converge to the corresponding Gaussian integrals. This is weak convergence plus admissible test functions, not an application of dominated convergence to functions on different spaces \(Ωₘ\).

4. All Aₘ are nonnegative. Continuity of \(φ\) on [0,∞), including zero, gives \[B_m-\phi(A_m)\longrightarrow\int\phi(f^2)\,d\gamma-\phi\!\left(\int f^2\,d\gamma\right)=\operatorname{Ent}_\gamma(f^2).\] There is no need to take a separate limit of log Aₘ or assume the limiting squared mass is strictly positive. This includes f≡0.

5. Compact \(C^{2}\) regularity supplies finite constants \(B,K\ge 0\) with \(|f′|\le B\) and \(|f′(y)-f′(x)|\le K|y-x|\) globally. To obtain K, bound the continuous second derivative on its compact support and use the mean-value theorem. Genuine differentiability is used; the totalized deriv API by itself does not supply this regularity.

6. Flipping coordinate j changes Sₘ by \(δⱼ=±2/√m\), exactly. For any x,y the mean-value theorem gives a secant a with \(f(y)-f(x)=a(y-x)\), \(|a|\le B\) and \(|a-f′(x)|\le K|y-x|\); the \(x=y\) case is immediate. Thus \[\big|(f(y)-f(x))^2-f'(x)^2(y-x)^2\big|\le2BK|y-x|^3.\] This is the squared-increment estimate used by the existing full-flip producer.

7. Let \(Gₘ(ε)=Σⱼ(f(Sₘ(εʲ))-f(Sₘ(ε)))^{2}\). Summing the last estimate over all m coordinates gives the pointwise bound \[|G_m(\varepsilon)-4f'(S_m(\varepsilon))^2|\le\frac{16BK}{\sqrt m}.\] The leading term is four because \(m·(2/√m)^{2}=4\); it would not be four for an average over coordinates. No independence assumption on the individual flip errors is needed.

8. Finite-space integrability licenses subtraction inside the expectation, and the probability mass is one. Hence \[\left|\mathbb E G_m-4C_m\right|\le\frac{16BK}{\sqrt m}\longrightarrow0.\] Together with the derivative-observer limit, this proves \[\mathbb E G_m\longrightarrow4\int(f')^2\,d\gamma.\] This uniform error estimate justifies accumulating m small coordinate errors; a pointwise one-coordinate approximation alone would not.

9. Apply the finite cube inequality to \(h(ε)=f(Sₘ(ε))\). Its energy may use the opposite subtraction order, but squaring makes the two orientations identical. For every \(m\ge 1\), \[B_m-\phi(A_m)\le\frac12\mathbb E G_m.\] Both sides have finite real limits by the preceding domain and convergence arguments.

10. Pass this family of inequalities through the limits using closedness of \(\le \) on \(\mathbb{R}\). The constant is exactly \[\operatorname{Ent}_\gamma(f^2)\le\frac12\left(4\int(f')^2\,d\gamma\right)=2\int(f')^2\,d\gamma.\] This proves the homogeneous compact \(C^{2}\) inequality without dividing by \(\int f^{2}\), choosing a representative outside this regular class, or assuming nonzero mass.

11. The Lean target invokes the existing entropy and full-flip producers, which internally establish the actual finite/Gaussian \(L^{1}\) domains and limits described above. It does not take those limits as additional public assumptions. A general Sobolev/noncompact extension would need its own approximation, representative and convergence arguments; this QA supplies none of those conclusions.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BernoulliLogSobolev
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactEntropy
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianFlipEnergy
import Mathlib.Topology.Order.OrderClosed

open MeasureTheory ProbabilityTheory Filter
open scoped Topology BigOperators ENNReal
open AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities

example
    (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

1. Checks genuine compact \(C^{2}\) regularity, measurable pushforward identities and bounded continuous/integrable test observables; obtains homogeneous entropy convergence via continuous s log s at zero without a positive-mass premise. (1 point)
2. Uses the exact ±2/√m displacement and bounded/Lipschitz derivative to control each squared increment, then sums all coordinates with factor four and a valid uniform vanishing error bound. (1 point)
3. Justifies real integration of the error and convergence of the full energy under actual probability laws, rather than invoking dominated convergence across changing spaces or assuming a one-coordinate approximation suffices. (1 point)
4. Applies the finite inequality with the matching orientation, passes through finite real limits and obtains exactly 2, keeping the signed/zero-mass and compact \(C^{2}\) boundary without claiming the noncompact theorem. (1 point)

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BernoulliLogSobolev
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactEntropy
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianFlipEnergy
import Mathlib.Topology.Order.OrderClosed

open MeasureTheory ProbabilityTheory Filter
open scoped Topology BigOperators ENNReal
open AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities

example
    (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
  -- Replace this comment with your proof.

Download task template

The fixed task reuses exactly the existing source proof with its parent imports, not the completed target module. Local \(μ\) and S are concrete normalized counting laws and actual Rademacher sums. The entropy producer supplies its final Tendsto component tEnt; the full-flip producer supplies tEnergy with coefficient four. change aligns their local let expressions with the target calculation. const_mul and ring turn one half of the energy limit into coefficient two. le_of_tendsto_of_tendsto passes the eventual inequalities to the limit; each inequality comes from the actual Bernoulli theorem at n+1, and sub_sq_comm reconciles the flip orientation. The detailed regularity, pushforward and uniform-error proof is inside the linked parent modules, not repeated inline or supplied as opaque extra assumptions. The aligned target certifies the final compact inequality, not each explanatory estimate as a separate Lean theorem.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BernoulliLogSobolev
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactEntropy
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianFlipEnergy
import Mathlib.Topology.Order.OrderClosed

open MeasureTheory ProbabilityTheory Filter
open scoped Topology BigOperators ENNReal
open AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities

example
    (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

Download runnable reference