Lax Lean Archive

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

Bounded descriptions of large matrix kernels

Lax342547.KernelWitness · concepts/Lax342547/KernelWitness.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 large sum of kernel dimensions has a certificate using a bounded number of coefficient columns per component. Enumerating these matrices costs only an exponential in their coefficient dimensions.

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

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

    1 coefficient_count proven

    2 exists_family_witness proven

    3 exists_kernel_witness proven

    4 kernel_event_bound proven

    Lean source view on GitHub

    1import Lax342547.MomentSpace
    2import Mathlib.LinearAlgebra.Matrix.Rank
    3import Mathlib.Probability.ProbabilityMassFunction.Basic
    4
    5/-!
    6---
    7title: Bounded descriptions of large matrix kernels
    8type: theorem
    9---
    10A large sum of kernel dimensions has a certificate using a bounded
    11number of coefficient columns per component. Enumerating these matrices
    12costs only an exponential in their coefficient dimensions.
    13-/
    14
    15namespace Lax342547.KernelWitness
    16
    17open Lax342547.MomentSpace
    18open scoped ENNReal
    19
    20axiom exists_kernel_witness {I N : Type} [Fintype I] [Fintype N]
    21 (A : Matrix N I Binary) (q : ℕ) :
    22 ∃ C : Matrix I (Fin q) Binary, A * C = 0 ∧
    23 min q (Module.finrank Binary (LinearMap.ker A.mulVecLin)) ≤ C.rank
    24
    25axiom exists_family_witness {Comp I N : Type} [Fintype Comp] [Fintype I] [Fintype N]
    26 (A : Comp → Matrix N I Binary) (q : ℕ)
    27 (hq : q ≤ ∑ e, Module.finrank Binary (LinearMap.ker (A e).mulVecLin)) :
    28 ∃ C : Comp → Matrix I (Fin q) Binary, (∀ e, A e * C e = 0) ∧ q ≤ ∑ e, (C e).rank
    29
    30axiom coefficient_count {Comp I : Type} [Fintype Comp] [Fintype I] (q : ℕ) :
    31 Nat.card (Comp → Matrix I (Fin q) Binary) = 2 ^ (Fintype.card Comp * Fintype.card I * q)
    32
    33axiom kernel_event_bound {Ω Comp I N : Type}
    34 [Fintype Ω] [Fintype Comp] [Fintype I] [Fintype N]
    35 (p : PMF Ω) (A : Ω → Comp → Matrix N I Binary) (q : ℕ) (cap : ℝ≥0∞)
    36 (hcap : ∀ C : Comp → Matrix I (Fin q) Binary, q ≤ (∑ e, (C e).rank) →
    37 p.toOuterMeasure {o | ∀ e, A o e * C e = 0} ≤ cap) :
    38 p.toOuterMeasure {o | q ≤ ∑ e, Module.finrank Binary (LinearMap.ker (A o e).mulVecLin)} ≤
    39 (2 : ℝ≥0∞) ^ (Fintype.card Comp * Fintype.card I * q) * cap
    40
    41end Lax342547.KernelWitness
    42
    Show ProofShow 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…