Lax Lean Archive

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

The row-corank bound for a uniform binary matrix

Lax342547.CorankCounting · concepts/Lax342547/CorankCounting.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

    Theorem

    A matrix with row corank at least s admits s independent row relations. Count the relation matrix first, then require every column to lie in its kernel. This gives the sharper 2^(ms-sn) probability bound used for the bounded row lists in Lemma 5.5, written as a ratio of nonnegative powers.

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

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

    1 card_corank proven

    2 exists_row_relations proven

    3 uniform_corank_bound proven

    Lean source view on GitHub

    1import Lax342547.LowRankCounting
    2
    3/-!
    4---
    5title: The row-corank bound for a uniform binary matrix
    6type: theorem
    7---
    8A matrix with row corank at least s admits s independent row relations.
    9Count the relation matrix first, then require every column to lie in its
    10kernel. This gives the sharper 2^(ms-sn) probability bound used for the
    11bounded row lists in Lemma 5.5, written as a ratio of nonnegative powers.
    12-/
    13
    14namespace Lax342547.CorankCounting
    15
    16axiom exists_row_relations {K I J : Type} [Field K] [Fintype I] [Fintype J]
    17 (M : Matrix I J K) (s : ℕ) (hs : M.rank + s ≤ Fintype.card I) :
    18 ∃ C : Matrix (Fin s) I K, Function.Surjective C.mulVec ∧ C * M = 0
    19
    20open Lax342547.MomentSpace
    21open scoped ENNReal
    22
    23axiom card_corank {I J : Type} [Fintype I] [Fintype J] (s : ℕ) :
    24 Nat.card {M : Matrix I J Binary // M.rank + s ≤ Fintype.card I} ≤
    25 2 ^ (s * Fintype.card I + (Fintype.card I - s) * Fintype.card J)
    26
    27axiom uniform_corank_bound {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
    28 (s : ℕ) :
    29 (PMF.uniformOfFintype (Matrix I J Binary)).toOuterMeasure {M | M.rank + s ≤ Fintype.card I} ≤
    30 (2 : ℝ≥0∞) ^ (s * Fintype.card I) / 2 ^ (s * Fintype.card J)
    31
    32end Lax342547.CorankCounting
    33
    Show ProofShow ProofShow 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…