Actual compact Gaussian observer and homogeneous entropy limits

Actual compact scalar specialization authored for the omitted GaussianLSI background. Pinned SLT is external source reference, not an imported proof certificate; all called proof APIs are ASTIS/Mathlib. Independent exact StatementSeal before proof. No full GaussianLSI or printed SPHMC inequality claimed.

Complete source statement (Samplinglib restatement)

For every real C2 function f with compact support, the actual variance-one centered Gaussian integrates f squared, f squared times log(f squared), and the square of its real derivative. Each actual normalized Bool counting measure integrates those same functions of the signed sum divided by sqrt(N), including N=0. Their positive-index (N+1) count integrals converge respectively to the Gaussian integrals. The corresponding homogeneous entropy, including zero mass, converges to the Gaussian homogeneous entropy. All domains and limits are produced internally.

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual compact Gaussian observer and homogeneous entropy limits

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactEntropy.compact_count_gaussian_entropy_limits · theorem · Teaching coverage

Read this first

Mathematical statement

\[\mu_N=2^{-N}\sum_{\varepsilon\in\{0,1\}^N}\delta_\varepsilon,\quad S_N=N^{-1/2}\sum_j\sigma(\varepsilon_j),\quad\gamma=\mathcal N(0,1);\quad\int A(S_{N+1})\,d\mu_{N+1}\to\int A\,d\gamma\quad(A=f^2,\ f^2\log f^2,\ (f\prime)^2),\quad\operatorname{Ent}_{\mu_{N+1}}(f^2\circ S_{N+1})\to\operatorname{Ent}_{\gamma}(f^2).\]

Lean statement · compact_count_gaussian_entropy_limits

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 compact_count_gaussian_entropy_limits
    (f : ℝ → ℝ) (hf : ContDiff ℝ 2 f) (hs : HasCompactSupport f) :
    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
    let γ : Measure ℝ := gaussianReal 0 1
    Integrable (fun x => (f x)^2) γ ∧
    Integrable (fun x => (f x)^2 * Real.log ((f x)^2)) γ ∧
    Integrable (fun x => (deriv f x)^2) γ ∧
    (∀ n : ℕ,
      Integrable (fun ε => (f (S n ε))^2) (μ n) ∧
      Integrable (fun ε => (f (S n ε))^2 * Real.log ((f (S n ε))^2)) (μ n) ∧
      Integrable (fun ε => (deriv f (S n ε))^2) (μ n)) ∧
    Tendsto (fun n : ℕ => ∫ ε, (f (S (n+1) ε))^2 ∂μ (n+1)) atTop
      (𝓝 (∫ x, (f x)^2 ∂γ)) ∧
    Tendsto (fun n : ℕ => ∫ ε,
      (f (S (n+1) ε))^2 * Real.log ((f (S (n+1) ε))^2) ∂μ (n+1)) atTop
      (𝓝 (∫ x, (f x)^2 * Real.log ((f x)^2) ∂γ)) ∧
    Tendsto (fun n : ℕ => ∫ ε, (deriv f (S (n+1) ε))^2 ∂μ (n+1)) atTop
      (𝓝 (∫ x, (deriv f x)^2 ∂γ)) ∧
    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) ∂γ) -
        (∫ x, (f x)^2 ∂γ) * Real.log (∫ x, (f x)^2 ∂γ)))

Exact module and namespace context

Proof roadmap

1Use the actual weak probability laws
Invoke the verified actual count-law CLT. Its internally constructed law lambda_N equals the pushforward of the literal count law under the literal sum for everyN. The successor family converges weakly to the exact Gaussian; no caller law or limit certificate enters this theorem.
2Build the three bounded compact observers
C2 gives continuous f and fprime. Their squares are continuous and compactly supported, since zero is preserved. The map t→t log t is continuous also at0 and takes0 to0, so f²logf² has the same compact-support property. The derivative support is contained in the support of f.
3Produce genuine integrability and count-map transport
Each continuous compact observer is genuinely Bochner integrable for every probability law lambda_N and for gamma. The finite sum map is measurable by its finite domain; Integrable.comp_measurable transfers the actual L1 property to the literal count law. The strongly measurable integral-map identity transports the same integrals. L1 is established separately, so totalized integral equalities do not replace domains.
4Convert weak convergence to the three real integral limits
Root ofCompactSupport packages each actual observer as a bounded continuous function without changing its values. The pinned weak-probability integral characterization gives its Gaussian integral limit. The proven map equality returns the literal successor count integrals.
5Combine the homogeneous entropy, including zero mass
Let m_N be the actual f² count integral. The mass limit and continuous tlogt give m_N log m_N → m log m even when m=0. Subtract this limit from the log-observer limit. The separate derivative-observer limit is not the full coordinate-flip-energy limit.

Full assumptions and notation

All objects and hypotheses

f:Real→Real, ContDiff Real 2 f, HasCompactSupport f: exact C2 AND compact support; no normalization or positive mass.
Canonical real Borel Gaussian of mean0 varianceNNReal1 and canonical finite Boolean carrier. The literal normalized count law and signsum map are fixed; all L1 and limits are outputs.
Real.log0=0 and tlogt is continuous at0. All N finite L1 includes0; only successor sequences assert asymptotic limits. AtN0 derivative observer equals fprime(0)^2 and need not vanish.
Authored compact scalar background integration, not printed SPHMC FIRST4.6. Fullflip-energy4, GaussianLSI, finite-Hilbert/noncompact extension, T2, main and expected costs remain open.

Mathematical proof

1. Use the actual weak probability laws

Invoke the verified actual count-law CLT. Its internally constructed law lambda_N equals the pushforward of the literal count law under the literal sum for everyN. The successor family converges weakly to the exact Gaussian; no caller law or limit certificate enters this theorem.

\[\lambda_N=(S_N)_\#\mu_N,\qquad\lambda_{N+1}\Rightarrow\gamma.\]

Corresponding Lean step

compact_observer; BalancedRademacherCLT.balanced_count_sum_tendsto_gaussian; hmap

2. Build the three bounded compact observers

C2 gives continuous f and fprime. Their squares are continuous and compactly supported, since zero is preserved. The map t→t log t is continuous also at0 and takes0 to0, so f²logf² has the same compact-support property. The derivative support is contained in the support of f.

\[A=f^2,\quad B=A\log A,\quad C=(f\prime)^2,\qquad A,B,C\in C_c(\mathbb R).\]

Corresponding Lean step

hA/sA,hB/sB,hC/sC; ContDiff.continuous_deriv; HasCompactSupport.deriv; HasCompactSupport.comp_left; Real.continuous_mul_log

3. Produce genuine integrability and count-map transport

Each continuous compact observer is genuinely Bochner integrable for every probability law lambda_N and for gamma. The finite sum map is measurable by its finite domain; Integrable.comp_measurable transfers the actual L1 property to the literal count law. The strongly measurable integral-map identity transports the same integrals. L1 is established separately, so totalized integral equalities do not replace domains.

\[\int g\,d\lambda_N=\int g(S_N)\,d\mu_N,\qquad g\in L^1(\gamma)\cap L^1(\lambda_N),\quad g\circ S_N\in L^1(\mu_N).\]

Corresponding Lean step

compact_observer; hi/hic/hI; Continuous.integrable_of_hasCompactSupport; Integrable.comp_measurable; integral_map_of_stronglyMeasurable

4. Convert weak convergence to the three real integral limits

Root ofCompactSupport packages each actual observer as a bounded continuous function without changing its values. The pinned weak-probability integral characterization gives its Gaussian integral limit. The proven map equality returns the literal successor count integrals.

\[\int g(S_{N+1})\,d\mu_{N+1}\longrightarrow\int g\,d\gamma\quad(g=A,B,C).\]

Corresponding Lean step

ofCompactSupport; ProbabilityMeasure.tendsto_iff_forall_integral_tendsto; ht; tA/tB/tC

5. Combine the homogeneous entropy, including zero mass

Let m_N be the actual f² count integral. The mass limit and continuous tlogt give m_N log m_N → m log m even when m=0. Subtract this limit from the log-observer limit. The separate derivative-observer limit is not the full coordinate-flip-energy limit.

\[\operatorname{Ent}_{\mu_N}(f^2\circ S_N)=\int B(S_N)\,d\mu_N-m_N\log m_N\longrightarrow\int B\,d\gamma-m\log m.\]

Corresponding Lean step

tE; Real.continuous_mul_log.continuousAt.tendsto; Tendsto.comp; Tendsto.sub

Lean verification

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

Lean proof · compact_count_gaussian_entropy_limits

Use the actual weak probability laws; Build the three bounded compact observers; Produce genuine integrability and count-map transport; Convert weak convergence to the three real integral limits; Combine the homogeneous entropy, including zero mass

Download module (.lean)

theorem compact_count_gaussian_entropy_limits
    (f : ℝ → ℝ) (hf : ContDiff ℝ 2 f) (hs : HasCompactSupport f) :
    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
    let γ : Measure ℝ := gaussianReal 0 1
    Integrable (fun x => (f x)^2) γ ∧
    Integrable (fun x => (f x)^2 * Real.log ((f x)^2)) γ ∧
    Integrable (fun x => (deriv f x)^2) γ ∧
    (∀ n : ℕ,
      Integrable (fun ε => (f (S n ε))^2) (μ n) ∧
      Integrable (fun ε => (f (S n ε))^2 * Real.log ((f (S n ε))^2)) (μ n) ∧
      Integrable (fun ε => (deriv f (S n ε))^2) (μ n)) ∧
    Tendsto (fun n : ℕ => ∫ ε, (f (S (n+1) ε))^2 ∂μ (n+1)) atTop
      (𝓝 (∫ x, (f x)^2 ∂γ)) ∧
    Tendsto (fun n : ℕ => ∫ ε,
      (f (S (n+1) ε))^2 * Real.log ((f (S (n+1) ε))^2) ∂μ (n+1)) atTop
      (𝓝 (∫ x, (f x)^2 * Real.log ((f x)^2) ∂γ)) ∧
    Tendsto (fun n : ℕ => ∫ ε, (deriv f (S (n+1) ε))^2 ∂μ (n+1)) atTop
      (𝓝 (∫ x, (deriv f x)^2 ∂γ)) ∧
    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) ∂γ) -
        (∫ x, (f x)^2 ∂γ) * Real.log (∫ x, (f x)^2 ∂γ))) := by
  have hA : Continuous (fun x => (f x)^2) := hf.continuous.pow 2
  have sA : HasCompactSupport (fun x => (f x)^2) := by
    simpa only [Function.comp_def] using hs.comp_left (g := fun t : ℝ => t^2) (by simp)
  have hB : Continuous (fun x => (f x)^2 * Real.log ((f x)^2)) :=
    Real.continuous_mul_log.comp hA
  have sB : HasCompactSupport (fun x => (f x)^2 * Real.log ((f x)^2)) := by
    simpa only [Function.comp_def] using
      sA.comp_left (g := fun t : ℝ => t * Real.log t) (by simp)
  have hC : Continuous (fun x => (deriv f x)^2) :=
    (hf.continuous_deriv (by norm_num)).pow 2
  have sC : HasCompactSupport (fun x => (deriv f x)^2) := by
    simpa only [Function.comp_def] using
      hs.deriv.comp_left (g := fun t : ℝ => t^2) (by simp)
  rcases compact_observer (fun x => (f x)^2) hA sA with ⟨iA, jA, tA⟩
  rcases compact_observer (fun x => (f x)^2 * Real.log ((f x)^2)) hB sB
    with ⟨iB, jB, tB⟩
  rcases compact_observer (fun x => (deriv f x)^2) hC sC with ⟨iC, jC, tC⟩
  have tE := tB.sub ((Real.continuous_mul_log.continuousAt.tendsto).comp tA)
  exact ⟨iA, iB, iC, fun n => ⟨jA n, jB n, jC n⟩, tA, tB, tC, tE⟩

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactEntropy

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
External compactly supported smooth background uses ContDiff Real2 AND HasCompactSupport.	Exact f/hf/hs analytic binders; continuity/support of three actual observers derived internally.	same	C2 is the pinned definition, not C-infinity. No positivity/normalization/BCF/domain binder added.
Weak real Rademacher laws and entropy-limit background.	Literal card-normalized Bool count and real signsum maps, allN domains and successor limits produced from actual35.	source-implicit	Authored carrier and map-integration adapter is explicit. GaussianReal variance1; N0 derivative value not forcedzero.
Fullflip-energy4 and GaussianLSI, finite-Hilbert/noncompact actual square-root density, T2/FIRST4.6/main/cost.	Authored compact C2 scalar core: same actual allN Bool count/card/signed sqrt-normalized sum and variance-one Gaussian. Three Gaussian L1 plus allN three actual-count L1 domains and successor mass/log-energy/derivative-square/entropy integral limits are produced internally. No supplied law/domain/limit certificate, normalization or positive mass premise. Fullflip-energy factor4, GaussianLSI, finiteHilbert/noncompact actual sqrtRN cutoff, T2/FIRST4.6/main/work/composition remain open. Focused3162PASS: zero-mass entropy and actual N0 derivative L1/value consumers, three standard3. Independent wholeproof/blind/source/exactcommit and shared publication remain separate.	unresolved	Derivative-observer convergence supplies no fullflip-energy theorem or GaussianLSI. Compact observers do not establish unbounded entropy/cost limits for general laws.

Authored compact C2 scalar core: same actual allN Bool count/card/signed sqrt-normalized sum and variance-one Gaussian. Three Gaussian L1 plus allN three actual-count L1 domains and successor mass/log-energy/derivative-square/entropy integral limits are produced internally. No supplied law/domain/limit certificate, normalization or positive mass premise. Fullflip-energy factor4, GaussianLSI, finiteHilbert/noncompact actual sqrtRN cutoff, T2/FIRST4.6/main/work/composition remain open. Focused3162PASS: zero-mass entropy and actual N0 derivative L1/value consumers, three standard3. Independent wholeproof/blind/source/exactcommit and shared publication 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

Authored compact C2 scalar core: same actual allN Bool count/card/signed sqrt-normalized sum and variance-one Gaussian. Three Gaussian L1 plus allN three actual-count L1 domains and successor mass/log-energy/derivative-square/entropy integral limits are produced internally. No supplied law/domain/limit certificate, normalization or positive mass premise. Fullflip-energy factor4, GaussianLSI, finiteHilbert/noncompact actual sqrtRN cutoff, T2/FIRST4.6/main/work/composition remain open. Focused3162PASS: zero-mass entropy and actual N0 derivative L1/value consumers, three standard3. Independent wholeproof/blind/source/exactcommit and shared publication remain separate.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.balanced_count_sum_tendsto_gaussian

Mathlib API called (external library)

MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto
ofCompactSupport
MeasureTheory.Continuous.integrable_of_hasCompactSupport
MeasureTheory.Integrable.comp_measurable
MeasureTheory.integral_map_of_stronglyMeasurable
HasCompactSupport.deriv
HasCompactSupport.comp_left
ContDiff.continuous_deriv
Real.continuous_mul_log

Mathematical sources

FIRST S4.E6 GaussianLSI background; SLT GaussianPoincare/Limit.lean compact observer and entropy convergence, including L1213-L1234 actual law-to-entropy use; authored literal Bool-count and rootBCF adapter — Authored compact C2 scalar core: same actual allN Bool count/card/signed sqrt-normalized sum and variance-one Gaussian. Three Gaussian L1 plus allN three actual-count L1 domains and successor mass/log-energy/derivative-square/entropy integral limits are produced internally. No supplied law/domain/limit certificate, normalization or positive mass premise. Fullflip-energy factor4, GaussianLSI, finiteHilbert/noncompact actual sqrtRN cutoff, T2/FIRST4.6/main/work/composition remain open. Focused3162PASS: zero-mass entropy and actual N0 derivative L1/value consumers, three standard3. Independent wholeproof/blind/source/exactcommit and shared publication remain separate.
Pinned weak-probability integral characterization — Reused compiled Mathlib primitive, no caller weak-law certificate.

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

Actual compact Gaussian observer and homogeneous entropy limits

Complete source statement (Samplinglib restatement)

Actual compact Gaussian observer and homogeneous entropy limits

Read the formalized proofs

Actual compact Gaussian observer and homogeneous entropy limits

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Use the actual weak probability laws

2. Build the three bounded compact observers

3. Produce genuine integrability and count-map transport

4. Convert weak convergence to the three real integral limits

5. Combine the homogeneous entropy, including zero mass

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?