Actual finite-count Rademacher sums converge weakly to the unit Gaussian

Mathlib Thomas Zhu and Etienne Marion scalar CLT; ASTIS-authored actual count-law/zero-index adapter. Independent source-first exact StatementSeal; Gaussian function entropy and full flip-energy limits remain separate.

Complete source statement (Samplinglib restatement)

There exists a family of real probability laws lambda_N, for every natural N, equal to the actual pushforward of normalized counting measure on all Fin N -> Bool configurations by the signed sum divided by sqrt(N). The true sign is +1 and the false sign is -1. Its zero law is dirac0, and the successor sequence lambda_(N+1) converges weakly to gaussianReal0,1 (mean0, variance1). No law, normalization, moment, independence or CLT certificate is supplied.

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 finite-count Rademacher sums converge weakly to the unit Gaussian

AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.balanced_count_sum_tendsto_gaussian · theorem · Teaching coverage

Read this first

Mathematical statement

There exists a family of real probability laws lambda_N, for every natural N, equal to the actual pushforward of normalized counting measure on all Fin N → Bool configurations by the signed sum divided by sqrt(N). The true sign is +1 and the false sign is -1. Its zero law is dirac0, and the successor sequence lambda_(N+1) converges weakly to gaussianReal0,1 (mean0, variance1). No law, normalization, moment, independence or CLT certificate is supplied.

\[\mu_N=2^{-N}\sum_{\varepsilon\in\{0,1\}^N}\delta_\varepsilon,\quad S_N(\varepsilon)=N^{-1/2}\sum_{j=1}^N\sigma(\varepsilon_j),\quad\lambda_N=(S_N)_\#\mu_N,\quad\lambda_0=\delta_0,\quad\lambda_{N+1}\Rightarrow\mathcal N(0,1).\]

Lean statement · balanced_count_sum_tendsto_gaussian

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 balanced_count_sum_tendsto_gaussian :
    ∃ laws : ℕ → ProbabilityMeasure ℝ,
      (∀ n : ℕ, (laws n : Measure ℝ) =
        (((Fintype.card (Fin n → Bool) : ℝ≥0∞)⁻¹ •
          (Measure.count : Measure (Fin n → Bool))).map
          (fun ε : Fin n → Bool => (Real.sqrt (n : ℝ))⁻¹ *
            ∑ j : Fin n, if ε j then (1 : ℝ) else -1))) ∧
      (laws 0 : Measure ℝ) = Measure.dirac 0 ∧
      Tendsto (fun n : ℕ => laws (n + 1)) atTop
        (𝓝 (⟨gaussianReal 0 1, inferInstance⟩ : ProbabilityMeasure ℝ))

Exact module and namespace context

Proof roadmap

1Build the actual laws, including zero
The finite carrier has positive cardinal2^N. Scaling counting measure by its reciprocal gives mass1. All finite functions are measurable and Bochner integrable; each normalized sum is pushed forward to a genuine probability law. AtN0 the empty sum is0, so its map law is the unit atom at0, without any fallback.
2Produce the single-coordinate moments
Use the actual balanced Bool count law and sigma(true)=1, sigma(false)=-1. The finite integral is the two-value average; hence the coordinate has mean0 and secondmoment1. These moments and measurable sign map are proof ingredients, never target premises.
3Prove the finite characteristic-function product
For every configuration, exp(i t sum sigma_j) is the product of exp(i t sigma_j). Sum over all configurations using Fintype.sum_pow; multiplying by2^-N gives the Nth power of the actual single-coordinate characteristic function. This is an authored count-law adapter, not an assumed independence or copied infinite-iid construction.
4Apply the pinned scalar CLT to the derived moments
Mathlib characteristic-function CLT applies to this actual measurable balanced coordinate with its internally derived mean0 and secondmoment1. It yields convergence of the same Nth-power expression to exp(-t^2/2), the exact characteristic function of mean0 variance1 Gaussian.
5Return weak convergence and the actual successor family
Levy convergence upgrades the pointwise characteristic-function limit of genuine probability measures to weak convergence. Composition with the cofinal n→n+1 sequence gives the sealed positive-index limit. The same family supplies every literal map equality and its zero atom.

Full assumptions and notation

All objects and hypotheses

Closed authored background specialization; no caller mathematical premises.
Actual finite carrier and normalized count law, literal sign true1/false-1, totalized inverse square root and empty zero sum. All probability, measurability and finite moment domains are produced internally.
ProbabilityMeasure Real has the canonical weak law topology. gaussianReal0,1 uses varianceNNReal1. No entropy, energy, W2, LSI, T2 or cost upgrade is implied.

Mathematical proof

1. Build the actual laws, including zero

The finite carrier has positive cardinal2^N. Scaling counting measure by its reciprocal gives mass1. All finite functions are measurable and Bochner integrable; each normalized sum is pushed forward to a genuine probability law. AtN0 the empty sum is0, so its map law is the unit atom at0, without any fallback.

\[\mu_N(\{0,1\}^N)=2^{-N}2^N=1,\qquad S_0=0,\quad\lambda_0=\delta_0.\]

Corresponding Lean step

private countLaw_probability; countLaw_integral; actualLaw; actualLaw_zero

2. Produce the single-coordinate moments

Use the actual balanced Bool count law and sigma(true)=1, sigma(false)=-1. The finite integral is the two-value average; hence the coordinate has mean0 and secondmoment1. These moments and measurable sign map are proof ingredients, never target premises.

\[\mathbb E\sigma=\tfrac12(1-1)=0,\qquad\mathbb E\sigma^2=\tfrac12(1+1)=1.\]

Corresponding Lean step

private sign_mean; sign_second_moment; measurable_of_countable

3. Prove the finite characteristic-function product

For every configuration, exp(i t sum sigma_j) is the product of exp(i t sigma_j). Sum over all configurations using Fintype.sum_pow; multiplying by2^-N gives the Nth power of the actual single-coordinate characteristic function. This is an authored count-law adapter, not an assumed independence or copied infinite-iid construction.

\[\widehat\lambda_N(t)=\left[\tfrac12\sum_{b\in\{0,1\}}\exp(i t\sigma(b)/\sqrt N)\right]^N.\]

Corresponding Lean step

private coordinate_charFun; unscaled_charFun; normalized_charFun; Complex.exp_sum; Fintype.sum_pow

4. Apply the pinned scalar CLT to the derived moments

Mathlib characteristic-function CLT applies to this actual measurable balanced coordinate with its internally derived mean0 and secondmoment1. It yields convergence of the same Nth-power expression to exp(-t^2/2), the exact characteristic function of mean0 variance1 Gaussian.

\[\widehat\lambda_N(t)\longrightarrow\exp(-t^2/2)=\widehat{\mathcal N(0,1)}(t).\]

Corresponding Lean step

ProbabilityTheory.tendsto_charFun_inv_sqrt_mul_pow; ProbabilityTheory.charFun_gaussianReal

5. Return weak convergence and the actual successor family

Levy convergence upgrades the pointwise characteristic-function limit of genuine probability measures to weak convergence. Composition with the cofinal n→n+1 sequence gives the sealed positive-index limit. The same family supplies every literal map equality and its zero atom.

\[\lambda_N\Rightarrow\mathcal N(0,1)\quad\Longrightarrow\quad\lambda_{N+1}\Rightarrow\mathcal N(0,1).\]

Corresponding Lean step

MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun; private actualLaw_tendsto; Filter.tendsto_add_atTop_nat

Lean verification

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

Lean proof · balanced_count_sum_tendsto_gaussian

Build the actual laws, including zero; Produce the single-coordinate moments; Prove the finite characteristic-function product; Apply the pinned scalar CLT to the derived moments; Return weak convergence and the actual successor family

Download module (.lean)

theorem balanced_count_sum_tendsto_gaussian :
    ∃ laws : ℕ → ProbabilityMeasure ℝ,
      (∀ n : ℕ, (laws n : Measure ℝ) =
        (((Fintype.card (Fin n → Bool) : ℝ≥0∞)⁻¹ •
          (Measure.count : Measure (Fin n → Bool))).map
          (fun ε : Fin n → Bool => (Real.sqrt (n : ℝ))⁻¹ *
            ∑ j : Fin n, if ε j then (1 : ℝ) else -1))) ∧
      (laws 0 : Measure ℝ) = Measure.dirac 0 ∧
      Tendsto (fun n : ℕ => laws (n + 1)) atTop
        (𝓝 (⟨gaussianReal 0 1, inferInstance⟩ : ProbabilityMeasure ℝ)) := by
  refine ⟨actualLaw, ?_, actualLaw_zero, ?_⟩
  · intro n
    rfl
  · exact actualLaw_tendsto.comp (tendsto_add_atTop_nat 1)

end AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Pinned scalar characteristic-function CLT requires measurable coordinate, mean0 and secondmoment1.	Closed actual balanced finite-count specialization derives those ingredients internally.	same	No general CLT proof is duplicated and no certificate becomes a public binder; actual finite adapter is disclosed as authored.
Finite Boolean normalized sum and variance-one real Gaussian background.	All N actual map laws; N0 actual dirac0; cofinal successor weak convergence.	source-implicit	The empty finite sum and inverse0 yield the exact degenerate law. No variance-one claim is made atN0.
Gaussian entropy/full-flip-energy limit, LSI, dimension/cutoff extension and Talagrand transport.	Actual finite Bool count/card map for all N, signs true1 false-1, inverse sqrtN; N0 dirac0 and positive successor weak-law Gaussian0,1. No input law/moment/limit certificate. No Gaussian entropy/energy/LSI/T2/paper completion. Focused3160PASS: actual N1 mean0/secondmoment1 and actual N0secondmoment0, three standard3 prints. Independent wholeproof/blind/source/topology/commit admission and shared integration remain separate.	unresolved	Weak convergence is insufficient for unbounded observables, entropy/energy limits or unbounded expected costs; every downstream consumer remains open.

Actual finite Bool count/card map for all N, signs true1 false-1, inverse sqrtN; N0 dirac0 and positive successor weak-law Gaussian0,1. No input law/moment/limit certificate. No Gaussian entropy/energy/LSI/T2/paper completion. Focused3160PASS: actual N1 mean0/secondmoment1 and actual N0secondmoment0, three standard3 prints. Independent wholeproof/blind/source/topology/commit admission and shared integration 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

Actual finite Bool count/card map for all N, signs true1 false-1, inverse sqrtN; N0 dirac0 and positive successor weak-law Gaussian0,1. No input law/moment/limit certificate. No Gaussian entropy/energy/LSI/T2/paper completion. Focused3160PASS: actual N1 mean0/secondmoment1 and actual N0secondmoment0, three standard3 prints. Independent wholeproof/blind/source/topology/commit admission and shared integration remain separate.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.tendsto_charFun_inv_sqrt_mul_pow
MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun
MeasureTheory.charFun_map_mul_comp
Fintype.sum_pow
Complex.exp_sum
MeasureTheory.integral_fintype

Mathematical sources

tendsto_charFun_inv_sqrt_mul_pow L59-L76; LevyConvergence L215; authored actual Bool-count specialization; SPHMC FIRST S4.E6 GaussianLSI omitted background — Actual finite Bool count/card map for all N, signs true1 false-1, inverse sqrtN; N0 dirac0 and positive successor weak-law Gaussian0,1. No input law/moment/limit certificate. No Gaussian entropy/energy/LSI/T2/paper completion. Focused3160PASS: actual N1 mean0/secondmoment1 and actual N0secondmoment0, three standard3 prints. Independent wholeproof/blind/source/topology/commit admission and shared integration remain separate.
Actual SPHMC omitted GaussianLSI background consumer — Not printedFIRST4.6 or GaussianLSI proof.

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 finite-count Rademacher sums converge weakly to the unit Gaussian

Complete source statement (Samplinglib restatement)

Actual finite-count Rademacher sums converge weakly to the unit Gaussian

Read the formalized proofs

Actual finite-count Rademacher sums converge weakly to the unit Gaussian

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Build the actual laws, including zero

2. Produce the single-coordinate moments

3. Prove the finite characteristic-function product

4. Apply the pinned scalar CLT to the derived moments

5. Return weak convergence and the actual successor family

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?