Lax Lean Archive

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

Joint minus images after exposing several plus frames

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

    After exposing all plus frames, their common annihilator loses at most one full-frame dimension per draw. Every affine minus column contains this translation space. Independent nominal tuples mixing all draws therefore retain the stated number of uniform image bits, at any rank.

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

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

    1 affine_image_bound proven

    2 completion_image_bound proven

    Lean source view on GitHub

    1import Lax342547.ProductImages
    2import Lax342547.ConditionalMinus
    3
    4/-!
    5---
    6title: Joint minus images after exposing several plus frames
    7type: lemma
    8---
    9After exposing all plus frames, their common annihilator loses at most
    10one full-frame dimension per draw. Every affine minus column contains
    11this translation space. Independent nominal tuples mixing all draws
    12therefore retain the stated number of uniform image bits, at any rank.
    13-/
    14
    15namespace Lax342547.ProductMinusImages
    16
    17open Lax342547.MomentSpace Lax342547.ConditionalMinus Lax342547.ProductImages
    18open scoped ENNReal
    19
    20variable {Draw B H T N : Type} [Fintype Draw] [Fintype B] [Fintype H] [Fintype T] [Fintype N]
    21
    22def images {E : Matrix B B Binary} {P : Draw → Matrix N B Binary} {X : Draw → Matrix N H Binary}
    23 (C : Matrix (Draw × (B ⊕ H)) T Binary) (z : ∀ i, ColumnProduct E (P i) (X i)) : Matrix N T Binary :=
    24 jointMatrix (fun i => Matrix.fromCols (z i).1.val (z i).2.val) * C
    25
    26axiom affine_image_bound [DecidableEq Draw] [DecidableEq B] [DecidableEq H] [DecidableEq N]
    27 (E : Matrix B B Binary) (P : Draw → Matrix N B Binary) (X : Draw → Matrix N H Binary)
    28 (hPX : ∀ i, Function.Injective (Matrix.fromCols (P i) (X i)).mulVec)
    29 [∀ i, Nonempty (ColumnProduct E (P i) (X i))]
    30 (C : Matrix (Draw × (B ⊕ H)) T Binary) (hC : Function.Injective C.mulVec) (y : Matrix N T Binary) :
    31 (PMF.uniformOfFintype (∀ i, ColumnProduct E (P i) (X i))).map (images C) y ≤
    32 1 / (2 : ℝ≥0∞) ^ (Fintype.card T *
    33 (Fintype.card N - Fintype.card Draw * (Fintype.card B + Fintype.card H)))
    34
    35axiom completion_image_bound [DecidableEq Draw] [DecidableEq B] [DecidableEq H] [DecidableEq N]
    36 (E : Matrix B B Binary) (P : Draw → Matrix N B Binary) (X : Draw → Matrix N H Binary)
    37 (hPX : ∀ i, Function.Injective (Matrix.fromCols (P i) (X i)).mulVec)
    38 [∀ i, Nonempty (ColumnProduct E (P i) (X i))] [∀ i, Nonempty (Completion E (P i) (X i))]
    39 (hN : 2 * (Fintype.card B + Fintype.card H) + 1 ≤ Fintype.card N)
    40 (C : Matrix (Draw × (B ⊕ H)) T Binary) (hC : Function.Injective C.mulVec) (y : Matrix N T Binary) :
    41 (PMF.uniformOfFintype (∀ i, Completion E (P i) (X i))).map
    42 (fun z => images C (fun i => (z i).val)) y ≤
    43 (2 : ℝ≥0∞) ^ Fintype.card Draw / 2 ^ (Fintype.card T *
    44 (Fintype.card N - Fintype.card Draw * (Fintype.card B + Fintype.card H)))
    45
    46end Lax342547.ProductMinusImages
    47
    Show 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…