Lax Lean Archive

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

Independent ordered mixer blocks at distinct labels

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

    Two direction spaces with independent combined columns can receive any prescribed forward and reverse bilinear blocks. A uniform ambient matrix therefore induces a uniform pair of blocks; any nonzero ordered parity is itself uniform. This applies to the free Z directions of distinct selector labels in Lemma 5.5.

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

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

    1 atom_orders_uniform proven

    2 family_parity_low_rank_bound proven

    3 family_parity_uniform proven

    4 ordered_parity_uniform proven

    5 orders_surjective proven

    6 orders_uniform proven

    Lean source view on GitHub

    1import Lax342547.AtomDirections
    2import Lax342547.FiniteLinearLaw
    3import Lax342547.LowRankCounting
    4
    5/-!
    6---
    7title: Independent ordered mixer blocks at distinct labels
    8type: lemma
    9---
    10Two direction spaces with independent combined columns can receive any
    11prescribed forward and reverse bilinear blocks. A uniform ambient matrix
    12therefore induces a uniform pair of blocks; any nonzero ordered parity
    13is itself uniform. This applies to the free Z directions of distinct
    14selector labels in Lemma 5.5.
    15-/
    16
    17namespace Lax342547.OrderedMixerLaw
    18
    19variable {K I N P : Type} [Field K] [Fintype I]
    20
    21def orders (D : Matrix I N K) (E : Matrix I P K) :
    22 Matrix I I K →ₗ[K] (Matrix N P K × Matrix P N K) where
    23 toFun L := (D.transpose * L * E, E.transpose * L * D)
    24 map_add' L M := by simp [Matrix.mul_add, Matrix.add_mul]
    25 map_smul' a L := by simp [Matrix.mul_smul, Matrix.smul_mul]
    26
    27def parity (a b : K) : (Matrix N P K × Matrix P N K) →ₗ[K] Matrix N P K where
    28 toFun x := a • x.1 + b • x.2.transpose
    29 map_add' x y := by simp [smul_add, add_add_add_comm]
    30 map_smul' c x := by simp [smul_add, smul_smul, mul_comm]
    31
    32def familyParity {F : Type} [Fintype F] (D : Matrix I N K) (E : Matrix I P K) (a b : F → K) :
    33 (F → Matrix I I K) →ₗ[K] Matrix N P K :=
    34 ∑ j, ((parity (a j) (b j)).comp (orders D E)).comp (LinearMap.proj j)
    35
    36axiom orders_surjective [Fintype N] [Fintype P]
    37 (D : Matrix I N K) (E : Matrix I P K)
    38 (hDE : Function.Injective (Matrix.fromCols D E).mulVec) :
    39 Function.Surjective (orders D E)
    40
    41open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    42open Lax342547.AtomDirections
    43
    44axiom orders_uniform {I N P : Type} [Fintype I] [Fintype N] [Fintype P]
    45 [DecidableEq I] [DecidableEq N] [DecidableEq P]
    46 (D : Matrix I N Binary) (E : Matrix I P Binary)
    47 (hDE : Function.Injective (Matrix.fromCols D E).mulVec) :
    48 (PMF.uniformOfFintype (Matrix I I Binary)).map (orders D E) =
    49 PMF.uniformOfFintype (Matrix N P Binary × Matrix P N Binary)
    50
    51axiom ordered_parity_uniform {I N P : Type} [Fintype I] [Fintype N] [Fintype P]
    52 [DecidableEq I] [DecidableEq N] [DecidableEq P]
    53 (D : Matrix I N Binary) (E : Matrix I P Binary)
    54 (hDE : Function.Injective (Matrix.fromCols D E).mulVec)
    55 (a b : Binary) (hab : a ≠ 0 ∨ b ≠ 0) :
    56 (PMF.uniformOfFintype (Matrix I I Binary)).map ((parity a b).comp (orders D E)) =
    57 PMF.uniformOfFintype (Matrix N P Binary)
    58
    59axiom atom_orders_uniform {k n b degree : ℕ} (hd : 1 ≤ degree)
    60 (s t : Fin b → Binary) (hst : s ≠ t) :
    61 (PMF.uniformOfFintype (Moment k n b degree)).map
    62 (orders (blockDirections s free) (blockDirections t free)) =
    63 PMF.uniformOfFintype (Matrix (Fin n) (Fin n) Binary × Matrix (Fin n) (Fin n) Binary)
    64
    65axiom family_parity_uniform {I N P F : Type} [Fintype I] [Fintype N] [Fintype P] [Fintype F]
    66 [DecidableEq I] [DecidableEq N] [DecidableEq P] [DecidableEq F]
    67 (D : Matrix I N Binary) (E : Matrix I P Binary)
    68 (hDE : Function.Injective (Matrix.fromCols D E).mulVec)
    69 (a b : F → Binary) (hab : ∃ j, a j ≠ 0 ∨ b j ≠ 0) :
    70 (PMF.uniformOfFintype (F → Matrix I I Binary)).map (familyParity D E a b) =
    71 PMF.uniformOfFintype (Matrix N P Binary)
    72
    73open scoped ENNReal
    74
    75axiom family_parity_low_rank_bound {I N P F : Type} [Fintype I] [Fintype N] [Fintype P] [Fintype F]
    76 [DecidableEq I] [DecidableEq N] [DecidableEq P] [DecidableEq F]
    77 (D : Matrix I N Binary) (E : Matrix I P Binary)
    78 (hDE : Function.Injective (Matrix.fromCols D E).mulVec)
    79 (a b : F → Binary) (hab : ∃ j, a j ≠ 0 ∨ b j ≠ 0) (r : ℕ) :
    80 (PMF.uniformOfFintype (F → Matrix I I Binary)).toOuterMeasure
    81 {L | (familyParity D E a b L).rank ≤ r} ≤
    82 (2 : ℝ≥0∞) ^ ((Fintype.card N + Fintype.card P) * r) / 2 ^ (Fintype.card N * Fintype.card P)
    83
    84end Lax342547.OrderedMixerLaw
    85
    Show ProofShow 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…