Lax Lean Archive

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

Uniform injective frames and channel transpose failure

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

    Injectivity of an h-column frame has probability at least one half when N≥h+1, so conditioning costs at most a factor of two on every event. The transpose evaluation on any prescribed independent q-tuple is therefore noninjective with probability at most 2^(q+1-h), as in (4.2).

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

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

    1 injection_event_bound proven

    2 injective_mass_half proven

    3 raw_transpose_failures proven

    4 transpose_failure proven

    5 transpose_uniform proven

    Lean source view on GitHub

    1import Lax342547.FrameSymmetry
    2import Lax342547.GramNormalization
    3
    4/-!
    5---
    6title: Uniform injective frames and channel transpose failure
    7type: theorem
    8---
    9Injectivity of an h-column frame has probability at least one half when
    10N≥h+1, so conditioning costs at most a factor of two on every event.
    11The transpose evaluation on any prescribed independent q-tuple is
    12therefore noninjective with probability at most 2^(q+1-h), as in (4.2).
    13-/
    14
    15namespace Lax342547.InjectiveFrames
    16
    17open Lax342547.MomentSpace Lax342547.FrameSymmetry
    18open scoped ENNReal
    19
    20axiom injective_mass_half {H N : Type} [Fintype H] [Fintype N]
    21 [DecidableEq H] [DecidableEq N] (hN : Fintype.card H + 1 ≤ Fintype.card N) :
    22 (1 / 2 : ℝ≥0∞) ≤ (PMF.uniformOfFintype (Matrix N H Binary)).toOuterMeasure
    23 {A | Function.Injective A.mulVec}
    24
    25axiom injection_event_bound {H N : Type} [Fintype H] [Fintype N]
    26 [DecidableEq H] [DecidableEq N] [Nonempty (Injection H N)]
    27 (hN : Fintype.card H + 1 ≤ Fintype.card N) (S : Set (Matrix N H Binary)) :
    28 (PMF.uniformOfFintype (Injection H N)).toOuterMeasure {A | A.val ∈ S} ≤
    29 2 * (PMF.uniformOfFintype (Matrix N H Binary)).toOuterMeasure S
    30
    31axiom transpose_uniform {I H N : Type} [Fintype I] [Fintype H] [Fintype N]
    32 [DecidableEq I] [DecidableEq H] [DecidableEq N]
    33 (D : Matrix N I Binary) (hD : Function.Injective D.mulVec) :
    34 (PMF.uniformOfFintype (Matrix N H Binary)).map (fun X => X.transpose * D) =
    35 PMF.uniformOfFintype (Matrix H I Binary)
    36
    37axiom transpose_failure {I H N : Type} [Fintype I] [Fintype H] [Fintype N]
    38 [DecidableEq I] [DecidableEq H] [DecidableEq N] [Nonempty (Injection H N)]
    39 (D : Matrix N I Binary) (hD : Function.Injective D.mulVec)
    40 (hN : Fintype.card H + 1 ≤ Fintype.card N) :
    41 (PMF.uniformOfFintype (Injection H N)).toOuterMeasure
    42 {X | ¬ Function.Injective (X.val.transpose * D).mulVec} ≤
    43 (2 : ℝ≥0∞) ^ (Fintype.card I + 1) / 2 ^ Fintype.card H
    44
    45axiom raw_transpose_failures {B I H N : Type}
    46 [Fintype B] [Fintype I] [Fintype H] [Fintype N]
    47 [DecidableEq I] [DecidableEq H] [DecidableEq N]
    48 {E : Matrix B B Binary} [Nonempty (RawFrames.Frame B H N E)]
    49 (D : Matrix N I Binary) (hD : Function.Injective D.mulVec)
    50 (hN : Fintype.card H + 1 ≤ Fintype.card N) :
    51 (PMF.uniformOfFintype (RawFrames.Frame B H N E)).toOuterMeasure
    52 {F | ¬ Function.Injective (F.X.transpose * D).mulVec} ≤
    53 (2 : ℝ≥0∞) ^ (Fintype.card I + 1) / 2 ^ Fintype.card H ∧
    54 (PMF.uniformOfFintype (RawFrames.Frame B H N E)).toOuterMeasure
    55 {F | ¬ Function.Injective (F.Y.transpose * D).mulVec} ≤
    56 (2 : ℝ≥0∞) ^ (Fintype.card I + 1) / 2 ^ Fintype.card H
    57
    58end Lax342547.InjectiveFrames
    59
    Show ProofShow 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…