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

Mixed moments of independently sampled balanced predicates

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

proven

Loading review…

Sign in with ORCID

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

    For a fixed tuple of supports with union of size tt, the absolute mixed moment is at most qt+2m2(N+1)e−Nq2/2q^t+2^m 2(N+1)e^{-Nq^2/2}. Here mm is the number of supports and NN is the size of the predicate domain. This is a normalized version of Lemma 4.12, with a nonoptimal concentration factor. Condition on all but one predicate in each nonempty subcollection; a union bound controls their correlations simultaneously. Independence of the coordinate labels then gives one factor qq per point of the union.

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

    Lean source view on GitHub

    1import Lax253009.BalancedPredicates
    2import Lax253009.HigherMoments
    3
    4/-!
    5---
    6title: Mixed moments of independently sampled balanced predicates
    7type: theorem
    8---
    9For a fixed tuple of supports with union of size tt, the absolute mixed
    10moment is at most qt+2m2(N+1)e−Nq2/2q^t+2^m 2(N+1)e^{-Nq^2/2}. Here mm is the number
    11of supports and NN is the size of the predicate domain. This is a
    12normalized version of Lemma 4.12, with a nonoptimal concentration factor.
    13Condition on all but one predicate in each nonempty subcollection; a
    14union bound controls their correlations simultaneously. Independence of
    15the coordinate labels then gives one factor qq per point of the union.
    16-/
    17
    18namespace Lax253009.MixedPredicateMoments
    19
    20open BooleanFourier BalancedPredicates
    21open scoped BigOperators
    22
    23axiom bound {ι κ : Type} [Fintype ι] [DecidableEq ι]
    24 [Fintype κ] [DecidableEq κ] [Nonempty κ]
    25 (n : ℕ) (hn : 0 < n) (hN : Fintype.card κ = 2 * n)
    26 (m : ℕ) (S : Fin m → Finset ι) (q : ℝ) (hq : 0 ≤ q) :
    27 |𝔼 B : Fin m → predicates κ n, 𝔼 f : ι → κ,
    28 ∏ j, ∏ i ∈ S j, sign ((B j).val (f i))| ≤
    29 q ^ (Finset.univ.biUnion S).card + (2 : ℝ) ^ m *
    30 (2 * (Fintype.card κ + 1 : ℝ) * Real.exp (-(Fintype.card κ : ℝ) * q ^ 2 / 2))
    31
    32end Lax253009.MixedPredicateMoments
    33
    Show Proof

    Discussion

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

    Loading discussion…