Lax Lean Archive

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

A uniform label budget for all sparse pin vectors

Lax342547.SparsePins · concepts/Lax342547/SparsePins.lean · lax-342547

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

    Lemma

    Lemma 5.3. Each projected pin space has dimension at most K. A single set of at most 2 |E| K (R + 14) labels contains the nonzero support of every expansion on at most R + 14 labels in any of these spaces. The hypothesis on selector degree is the one used in the paper's proof.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax342547.MomentSpace
    2import Mathlib.LinearAlgebra.Finsupp.LSum
    3import Mathlib.LinearAlgebra.Dimension.Finite
    4
    5/-!
    6---
    7title: A uniform label budget for all sparse pin vectors
    8type: lemma
    9---
    10Lemma 5.3. Each projected pin space has dimension at most K. A single
    11set of at most 2 |E| K (R + 14) labels contains the nonzero support of
    12every expansion on at most R + 14 labels in any of these spaces.
    13The hypothesis on selector degree is the one used in the paper's proof.
    14-/
    15
    16namespace Lax342547.SparsePins
    17
    18open Lax342547.MomentSpace
    19
    20variable {Label Coord Base : Type}
    21
    22def labelTensor (p : Label → Coord → Binary) (s : Label) :
    23 (Base → Binary) →ₗ[Binary] (Coord × Base → Binary) where
    24 toFun z i := p s i.1 * z i.2
    25 map_add' z w := by ext i; exact mul_add _ _ _
    26 map_smul' a z := by ext i; exact mul_left_comm _ _ _
    27
    28noncomputable def expansion (p : Label → Coord → Binary) :
    29 (Label →₀ (Base → Binary)) →ₗ[Binary] (Coord × Base → Binary) :=
    30 Finsupp.lsum Binary (labelTensor p)
    31
    32axiom sparse_pin_labels {Base Component : Type} [Fintype Base] [Fintype Component]
    33 {b degree K R : ℕ}
    34 (U : Bool → Component → Submodule Binary (SelectorCoordinates b degree × Base → Binary))
    35 (hdim : ∀ sign e, Module.finrank Binary (U sign e) ≤ K)
    36 (hdegree : (K + 1) * (R + 14) ≤ degree + 1) :
    37 ∃ B : Finset (Fin b → Binary),
    38 B.card ≤ 2 * Fintype.card Component * K * (R + 14) ∧
    39 ∀ sign e (c : (Fin b → Binary) →₀ (Base → Binary)),
    40 c.support.card ≤ R + 14 → expansion (selectorEval (degree := degree)) c ∈ U sign e →
    41 c.support ⊆ B
    42
    43end Lax342547.SparsePins
    44
    Show 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…