Lax Lean Archive

Small-union weighted double-cover estimate

Lax323828.SmallUnionDoubleCovers · concepts/Lax323828/SmallUnionDoubleCovers.lean · lax-323828

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

    If every coefficient is at most δ\delta, double covers of a set of size tt have total weight at most a dimension-independent constant times δm−2t\delta^{m-2t}. This is the estimate in Lemma 4.16. Extract 2t2t positions that still cover every point twice. Each remaining support is one of at most 2t2^t subsets of their union.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax323828.DoubleCoverBounds
    2
    3/-!
    4---
    5title: Small-union weighted double-cover estimate
    6type: theorem
    7---
    8If every coefficient is at most δ\delta, double covers of a set of size
    9tt have total weight at most a dimension-independent constant times
    10δm−2t\delta^{m-2t}. This is the estimate in Lemma 4.16. Extract 2t2t
    11positions that still cover every point twice. Each remaining support is
    12one of at most 2t2^t subsets of their union.
    13-/
    14
    15namespace Lax323828.SmallUnionDoubleCovers
    16
    17open scoped Classical
    18
    19open HigherMoments
    20open scoped BigOperators
    21
    22/-- The total product weight of double-cover tuples whose union has exactly `t` coordinates. -/
    23noncomputable def weight {ι : Type} [Fintype ι] [DecidableEq ι]
    24 (c : Finset ι → ℝ) (m t : ℕ) : ℝ :=
    25 ∑ S : Fin m → Finset ι,
    26 if DoubleCover S ∧ (Finset.univ.biUnion S).card = t then ∏ j, c (S j) else 0
    27
    28axiom bound {ι : Type} [Fintype ι] [DecidableEq ι]
    29 (c : Finset ι → ℝ) (l m t : ℕ) (δ : ℝ)
    30 (hc : ∀ S, 0 ≤ c S) (hsmall : ∀ S, c S ≤ δ) (hδ : 0 ≤ δ)
    31 (hdegree : ∀ S, l < S.card → c S = 0) (henergy : ∑ S, c S ^ 2 ≤ 1)
    32 (hmt : 2 * t ≤ m) :
    33 weight c m t ≤ (2 : ℝ) ^ m * ((2 : ℝ) ^ t * δ) ^ (m - 2 * t) *
    34 (1 + (3 : ℝ) ^ (l * (4 * t + 1) * 2 ^ (2 * t)))
    35
    36end Lax323828.SmallUnionDoubleCovers
    37
    Show Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…