Lax Lean Archive

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

Constrained key reference spaces have positive density

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

    Independent component Gram constraints have an explicit product lower bound independent of ambient dimension once the slot count fits. The constrained key space has at most two to the number of ambient key bits elements.

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

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

    1 block_reference_lower proven

    2 reference_density_lower proven

    3 space_card_upper proven

    Lean source view on GitHub

    1import Lax342547.GramNormalization
    2
    3/-!
    4---
    5title: Constrained key reference spaces have positive density
    6type: lemma
    7---
    8Independent component Gram constraints have an explicit product lower bound independent of ambient dimension once the slot count fits. The constrained key space has at most two to the number of ambient key bits elements.
    9-/
    10
    11namespace Lax342547.ReferenceKeys
    12
    13open Lax342547.MomentSpace
    14open scoped ENNReal
    15
    16abbrev Tuples (Comp : Type) (Pos : Comp → Type) (N : Type) :=
    17 ∀ e, Matrix N (Pos e) Binary × Matrix N (Pos e) Binary
    18
    19noncomputable def space {Comp : Type} (Pos : Comp → Type) (N : Type)
    20 [∀ e, Fintype (Pos e)] [Fintype N] (G : ∀ e, Matrix (Pos e) (Pos e) Binary) :
    21 Set (Tuples Comp Pos N) := {x | ∀ e, (x e).1.transpose * (x e).2 = G e}
    22
    23axiom space_card_upper {Comp N : Type} [Fintype Comp] [Fintype N]
    24 (Pos : Comp → Type) [∀ e, Fintype (Pos e)]
    25 (G : ∀ e, Matrix (Pos e) (Pos e) Binary) : by
    26 classical
    27 exact Fintype.card (space Pos N G) ≤
    28 2 ^ ((2 * ∑ e, Fintype.card (Pos e)) * Fintype.card N)
    29
    30axiom block_reference_lower {I N : Type} [Fintype I] [Fintype N]
    31 [DecidableEq I] [DecidableEq N] (G : Matrix I I Binary)
    32 (hN : 2 * Fintype.card I + 1 ≤ Fintype.card N) :
    33 1 / (2 : ℝ≥0∞) ^ (Fintype.card I * Fintype.card I + 2) ≤
    34 ((PMF.uniformOfFintype (Matrix N I Binary × Matrix N I Binary)).map
    35 (fun x => x.1.transpose * x.2)) G
    36
    37axiom reference_density_lower {Comp N : Type} [Fintype Comp] [Fintype N]
    38 [DecidableEq Comp] [DecidableEq N]
    39 (Pos : Comp → Type) [∀ e, Fintype (Pos e)] [∀ e, DecidableEq (Pos e)]
    40 (G : ∀ e, Matrix (Pos e) (Pos e) Binary)
    41 (hN : ∀ e, 2 * Fintype.card (Pos e) + 1 ≤ Fintype.card N) :
    42 (∏ e, 1 / (2 : ℝ≥0∞) ^ (Fintype.card (Pos e) * Fintype.card (Pos e) + 2)) ≤
    43 (PMF.uniformOfFintype (Tuples Comp Pos N)).toOuterMeasure (space Pos N G)
    44
    45end Lax342547.ReferenceKeys
    46
    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…