Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Counting and concentration of uniformly balanced predicates

Lax253009.BalancedPredicates · concepts/Lax253009/BalancedPredicates.lean · lax-253009

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Predicates with exactly nn true values on an NN-element set are counted by (Nn)\binom{N}{n}. When N=2nN=2n, they constitute at least a fraction 1/(N+1)1/(N+1) of all predicates.

    For a fixed sign-valued function GG and a uniform balanced predicate BB, the absolute correlation sum has tail at most 2(N+1)e−t2/(2N)2(N+1)e^{-t^2/(2N)} at t≥0t\geq0, for N>0N>0. This bound is obtained by conditioning independent signs on balance. It has an extra factor N+1N+1 compared with the paper's pairing argument in Lemma 4.7, but gives the same required asymptotic decay at t=N3/4t=N^{3/4} in the soundness proof.

    Concept map
    4 concepts; 7 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 absolute_correlation_tail proven

    2 central_mass proven

    3 count proven

    Lean source view on GitHub

    1import Lax253009.ExponentialBounds
    2import Mathlib.Data.Finset.Powerset
    3import Mathlib.Data.Nat.Choose.Sum
    4
    5/-!
    6---
    7title: Counting and concentration of uniformly balanced predicates
    8type: theorem
    9---
    10Predicates with exactly nn true values on an NN-element set are counted
    11by (Nn)\binom{N}{n}. When N=2nN=2n, they constitute at least a fraction
    121/(N+1)1/(N+1) of all predicates.
    13
    14For a fixed sign-valued function GG and a uniform balanced predicate BB,
    15the absolute correlation sum has tail at most
    162(N+1)e−t2/(2N)2(N+1)e^{-t^2/(2N)} at t≥0t\geq0, for N>0N>0.
    17This bound is obtained by conditioning independent signs on balance.
    18It has an extra factor N+1N+1 compared with the paper's pairing argument
    19in Lemma 4.7, but gives the same required asymptotic decay at
    20t=N3/4t=N^{3/4} in the soundness proof.
    21-/
    22
    23namespace Lax253009.BalancedPredicates
    24
    25open BooleanFourier FiniteProbability
    26open scoped BigOperators
    27
    28def predicates (κ : Type) [Fintype κ] [DecidableEq κ] (n : ℕ) : Finset (Cube κ) :=
    29 Finset.univ.filter fun B ↦ (Finset.univ.filter fun z ↦ B z = true).card = n
    30
    31axiom count {κ : Type} [Fintype κ] [DecidableEq κ] (n : ℕ) :
    32 (predicates κ n).card = (Fintype.card κ).choose n
    33
    34axiom central_mass {κ : Type} [Fintype κ] [DecidableEq κ]
    35 (n : ℕ) (hN : Fintype.card κ = 2 * n) :
    36 Fintype.card (Cube κ) ≤ (Fintype.card κ + 1) * (predicates κ n).card
    37
    38axiom absolute_correlation_tail {κ : Type} [Fintype κ] [DecidableEq κ]
    39 (n : ℕ) (hn : 0 < n) (hN : Fintype.card κ = 2 * n)
    40 (G : Cube κ) (t : ℝ) (ht : 0 ≤ t) :
    41 probability (fun B : predicates κ n ↦ t ≤ |∑ z, sign (G z) * sign (B.val z)|) ≤
    42 2 * (Fintype.card κ + 1 : ℝ) * Real.exp (-t ^ 2 / (2 * Fintype.card κ))
    43
    44end Lax253009.BalancedPredicates
    45
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…