Lax Lean Archive

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

Random sharp-block forms and their alternating parity

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

    The sharp part of the self-Gram form at distinct labels is a nonzero linear combination of independently uniform matrices. It is uniform. Although its sum with its transpose is alternating, any block on disjoint row and column index sets is uniform and supplies the required rank bound.

    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 alternating_block_uniform proven

    2 alternating_low_rank_bound proven

    3 label_parity_low_rank_bounds proven

    4 label_weighted_uniform proven

    5 selfGram_free_block proven

    6 selfGram_sharp_block proven

    Lean source view on GitHub

    1import Lax342547.AtomDirections
    2import Lax342547.FiniteLinearLaw
    3import Lax342547.LowRankCounting
    4
    5/-!
    6---
    7title: Random sharp-block forms and their alternating parity
    8type: lemma
    9---
    10The sharp part of the self-Gram form at distinct labels is a nonzero
    11linear combination of independently uniform matrices. It is uniform.
    12Although its sum with its transpose is alternating, any block on disjoint
    13row and column index sets is uniform and supplies the required rank bound.
    14-/
    15
    16namespace Lax342547.SharpMixerLaw
    17
    18variable {K A I N P : Type} [Field K] [Fintype A]
    19
    20def weighted (c : A → K) : (A → Matrix I I K) →ₗ[K] Matrix I I K where
    21 toFun M := ∑ a, c a • M a
    22 map_add' M L := by simp [smul_add, Finset.sum_add_distrib]
    23 map_smul' r M := by simp [smul_smul, Finset.smul_sum, mul_comm]
    24
    25def alternatingBlock (c : N → I) (d : P → I) : Matrix I I K →ₗ[K] Matrix N P K where
    26 toFun M i j := M (c i) (d j) + M (d j) (c i)
    27 map_add' M L := by
    28 ext i j
    29 change (M (c i) (d j) + L (c i) (d j)) + (M (d j) (c i) + L (d j) (c i)) =
    30 (M (c i) (d j) + M (d j) (c i)) + (L (c i) (d j) + L (d j) (c i))
    31 exact add_add_add_comm _ _ _ _
    32 map_smul' a M := by
    33 ext i j
    34 change a * M (c i) (d j) + a * M (d j) (c i) = a * (M (c i) (d j) + M (d j) (c i))
    35 exact (mul_add _ _ _).symm
    36
    37open Lax342547.MomentSpace Lax342547.ConcreteGeometry Lax342547.AtomDirections
    38open scoped ENNReal
    39
    40axiom label_weighted_uniform {b n : ℕ} (s t : Fin b → Binary) (hst : s ≠ t) :
    41 (PMF.uniformOfFintype (Fin b → Matrix (Fin n) (Fin n) Binary)).map
    42 (weighted (fun a => s a + t a)) = PMF.uniformOfFintype (Matrix (Fin n) (Fin n) Binary)
    43
    44axiom selfGram_sharp_block {k n b degree r : ℕ} (hr : 2 * r ≤ n) (hd : 1 ≤ degree)
    45 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (s t : Fin b → Binary) :
    46 (blockDirections (k := k) (degree := degree) s sharp).transpose * selfGram hr hd M *
    47 blockDirections t sharp = weighted (fun a => s a + t a) M
    48
    49axiom selfGram_free_block {k n b degree r : ℕ} (hr : 2 * r ≤ n) (hd : 1 ≤ degree)
    50 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (s t : Fin b → Binary) :
    51 (blockDirections (k := k) (degree := degree) s free).transpose * selfGram hr hd M *
    52 blockDirections t free = (0 : Matrix (Fin n) (Fin n) Binary)
    53
    54axiom alternating_block_uniform {I N P : Type} [Fintype I] [Fintype N] [Fintype P]
    55 [DecidableEq I] [DecidableEq N] [DecidableEq P]
    56 (c : N → I) (d : P → I) (hc : Function.Injective c) (hd : Function.Injective d)
    57 (hcd : ∀ i j, c i ≠ d j) :
    58 (PMF.uniformOfFintype (Matrix I I Binary)).map (alternatingBlock c d) =
    59 PMF.uniformOfFintype (Matrix N P Binary)
    60
    61axiom alternating_low_rank_bound (n r : ℕ) :
    62 (PMF.uniformOfFintype (Matrix (Fin n) (Fin n) Binary)).toOuterMeasure
    63 {M | (M + M.transpose).rank ≤ r} ≤
    64 (2 : ℝ≥0∞) ^ ((n / 2 + n / 2) * r) / 2 ^ ((n / 2) * (n / 2))
    65
    66axiom label_parity_low_rank_bounds {b n : ℕ} (s t : Fin b → Binary) (hst : s ≠ t) (r : ℕ) :
    67 let A := weighted (I := Fin n) (fun a => s a + t a)
    68 let μ := PMF.uniformOfFintype (Fin b → Matrix (Fin n) (Fin n) Binary)
    69 μ.toOuterMeasure {M | (A M).rank ≤ r} ≤ (2 : ℝ≥0∞) ^ ((n + n) * r) / 2 ^ (n * n) ∧
    70 μ.toOuterMeasure {M | (A M).transpose.rank ≤ r} ≤ (2 : ℝ≥0∞) ^ ((n + n) * r) / 2 ^ (n * n) ∧
    71 μ.toOuterMeasure {M | (A M + (A M).transpose).rank ≤ r} ≤
    72 (2 : ℝ≥0∞) ^ ((n / 2 + n / 2) * r) / 2 ^ ((n / 2) * (n / 2))
    73
    74end Lax342547.SharpMixerLaw
    75
    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…