Lax Lean Archive

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

Gram-conditioned columns and their rank-failure probability

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

    At an injective plus frame, a prescribed Gram matrix has probability exactly 2^(-pq). Its completions are independent affine columns parallel to the plus annihilator. Their failure of injectivity costs at most 2^(p+q-N), uniformly in the prescribed Gram values.

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

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

    1 conditional_failure proven

    2 extension_failure proven

    3 gram_probability proven

    4 gram_uniform proven

    Lean source view on GitHub

    1import Lax342547.AffineImages
    2
    3/-!
    4---
    5title: Gram-conditioned columns and their rank-failure probability
    6type: lemma
    7---
    8At an injective plus frame, a prescribed Gram matrix has probability
    9exactly 2^(-pq). Its completions are independent affine columns parallel
    10to the plus annihilator. Their failure of injectivity costs at most
    112^(p+q-N), uniformly in the prescribed Gram values.
    12-/
    13
    14namespace Lax342547.GramColumns
    15
    16open Lax342547.MomentSpace
    17open scoped ENNReal
    18
    19variable {I J N : Type} [Fintype I] [Fintype J] [Fintype N]
    20
    21def gramMap (A : Matrix N I Binary) : Matrix N J Binary →ₗ[Binary] Matrix I J Binary where
    22 toFun B := A.transpose * B
    23 map_add' B C := by simp [Matrix.mul_add]
    24 map_smul' c B := by simp [Matrix.mul_smul]
    25
    26abbrev GramFiber (A : Matrix N I Binary) (G : Matrix I J Binary) :=
    27 {B : Matrix N J Binary // A.transpose * B = G}
    28
    29noncomputable instance (A : Matrix N I Binary) (G : Matrix I J Binary) : Fintype (GramFiber A G) := by
    30 classical exact Subtype.fintype _
    31
    32axiom gram_uniform [DecidableEq I] [DecidableEq J] [DecidableEq N]
    33 (A : Matrix N I Binary) (hA : Function.Injective A.mulVec) :
    34 (PMF.uniformOfFintype (Matrix N J Binary)).map (gramMap A) =
    35 PMF.uniformOfFintype (Matrix I J Binary)
    36
    37axiom gram_probability [DecidableEq I] [DecidableEq J] [DecidableEq N]
    38 (A : Matrix N I Binary) (hA : Function.Injective A.mulVec) (G : Matrix I J Binary) :
    39 (PMF.uniformOfFintype (Matrix N J Binary)).toOuterMeasure {B | A.transpose * B = G} =
    40 1 / (2 : ℝ≥0∞) ^ (Fintype.card I * Fintype.card J)
    41
    42axiom conditional_failure [DecidableEq I] [DecidableEq J] [DecidableEq N]
    43 (A : Matrix N I Binary) (hA : Function.Injective A.mulVec) (G : Matrix I J Binary)
    44 [Nonempty (GramFiber A G)] :
    45 (PMF.uniformOfFintype (GramFiber A G)).toOuterMeasure {B | ¬ Function.Injective B.val.mulVec} ≤
    46 (2 : ℝ≥0∞) ^ (Fintype.card I + Fintype.card J) / 2 ^ Fintype.card N
    47
    48axiom extension_failure {K : Type} [Fintype K]
    49 [DecidableEq I] [DecidableEq J] [DecidableEq N]
    50 (P : Matrix N K Binary) (hP : Function.Injective P.mulVec)
    51 (A : Matrix N I Binary) (hA : Function.Injective A.mulVec) (G : Matrix I J Binary)
    52 [Nonempty (GramFiber A G)] :
    53 (PMF.uniformOfFintype (GramFiber A G)).toOuterMeasure
    54 {X | ¬ Function.Injective (fun z : (K → Binary) × (J → Binary) =>
    55 P.mulVec z.1 + X.val.mulVec z.2)} ≤
    56 (2 : ℝ≥0∞) ^ (Fintype.card K + Fintype.card I + Fintype.card J) / 2 ^ Fintype.card N
    57
    58end Lax342547.GramColumns
    59
    Show ProofShow 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…