Lax Lean Archive

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

Concrete coordinates, quadratic testers, and the self-Gram form

Lax342547.ConcreteGeometry · concepts/Lax342547/ConcreteGeometry.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 coordinate realization of §2.3. The three common blocks are indexed by 0 (S), 1 (#), and 2 (Z). Tester pairs use coordinates 2ρ and 2ρ+1 in zero-based indexing. The self-Gram matrix has the ordered tester part and the selector-dependent # part; it has no Z entries.

    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 2 statements. Each proof establishes one of them relative to its assumptions.

    1 selfGram_changeZ proven

    2 selfGram_moments proven

    Lean source view on GitHub

    1import Lax342547.TagGeometry
    2import Lax342547.GradientForm
    3import Lean.Elab.Tactic.Omega
    4
    5/-!
    6---
    7title: Concrete coordinates, quadratic testers, and the self-Gram form
    8type: lemma
    9---
    10The coordinate realization of §2.3. The three common blocks are indexed
    11by 0 (S), 1 (#), and 2 (Z). Tester pairs use coordinates 2ρ and 2ρ+1
    12in zero-based indexing. The self-Gram matrix has the ordered tester
    13part and the selector-dependent # part; it has no Z entries.
    14-/
    15
    16namespace Lax342547.ConcreteGeometry
    17
    18open Lax342547.MomentSpace Lax342547.TagGeometry
    19
    20abbrev Coordinate (k n b degree : ℕ) := SelectorCoordinates b degree × Option (Base k n)
    21noncomputable instance (k n b degree : ℕ) : DecidableEq (Coordinate k n b degree) := Classical.decEq _
    22abbrev Vector (k n b degree : ℕ) := Coordinate k n b degree → Binary
    23abbrev Moment (k n b degree : ℕ) := Matrix (Coordinate k n b degree) (Coordinate k n b degree) Binary
    24
    25def ordinary {k n : ℕ} (d t : Tag k) (i : Fin n) : Base k n := Sum.inl ((d, t), i)
    26def shared {k n : ℕ} (i : Fin n) : Base k n := Sum.inr (0, i)
    27def sharp {k n : ℕ} (i : Fin n) : Base k n := Sum.inr (1, i)
    28def free {k n : ℕ} (i : Fin n) : Base k n := Sum.inr (2, i)
    29
    30def emptySelector (b degree : ℕ) : SelectorCoordinates b degree := ⟨∅, Nat.zero_le _⟩
    31def bitSelector {b degree : ℕ} (h : 1 ≤ degree) (a : Fin b) : SelectorCoordinates b degree :=
    32 ⟨{a}, by simpa using h⟩
    33
    34def pairLeft {n r : ℕ} (h : 2 * r ≤ n) (ρ : Fin r) : Fin n := ⟨2 * ρ.val, by omega⟩
    35def pairRight {n r : ℕ} (h : 2 * r ≤ n) (ρ : Fin r) : Fin n := ⟨2 * ρ.val + 1, by omega⟩
    36
    37def matrixEntry {I : Type} (i j : I) : Matrix I I Binary →ₗ[Binary] Binary where
    38 toFun w := w i j
    39 map_add' _ _ := rfl
    40 map_smul' _ _ := rfl
    41
    42def blockTester {k n b degree r : ℕ} (h : 2 * r ≤ n) (c : Fin n → Base k n) :
    43 Moment k n b degree →ₗ[Binary] Binary :=
    44 ∑ ρ : Fin r, matrixEntry (emptySelector b degree, some (c (pairLeft h ρ)))
    45 (emptySelector b degree, some (c (pairRight h ρ)))
    46
    47def etaO {k n b degree r : ℕ} (h : 2 * r ≤ n) : Moment k n b degree →ₗ[Binary] Binary :=
    48 ∑ d : Tag k, ∑ t : Tag k, blockTester h (ordinary d t)
    49
    50def eta {k n b degree r : ℕ} (h : 2 * r ≤ n) : Moment k n b degree →ₗ[Binary] Binary :=
    51 etaO h + blockTester h shared
    52
    53def blockForm {k n b degree r : ℕ} (h : 2 * r ≤ n) (c : Fin n → Base k n) :
    54 LinearMap.BilinForm Binary (Vector k n b degree) :=
    55 ∑ ρ : Fin r, GradientForm.rankOne
    56 (LinearMap.proj (emptySelector b degree, some (c (pairLeft h ρ))))
    57 (LinearMap.proj (emptySelector b degree, some (c (pairRight h ρ))))
    58
    59def testerForm {k n b degree r : ℕ} (h : 2 * r ≤ n) :
    60 LinearMap.BilinForm Binary (Vector k n b degree) :=
    61 (∑ d : Tag k, ∑ t : Tag k, blockForm h (ordinary d t)) + blockForm h shared
    62
    63def sharpForm {k n b degree : ℕ} (h : 1 ≤ degree)
    64 (M : Fin b → Matrix (Fin n) (Fin n) Binary) :
    65 LinearMap.BilinForm Binary (Vector k n b degree) :=
    66 ∑ a : Fin b, ∑ i : Fin n, ∑ j : Fin n, M a i j •
    67 (GradientForm.rankOne (LinearMap.proj (bitSelector h a, some (sharp i)))
    68 (LinearMap.proj (emptySelector b degree, some (sharp j))) +
    69 GradientForm.rankOne (LinearMap.proj (emptySelector b degree, some (sharp i)))
    70 (LinearMap.proj (bitSelector h a, some (sharp j))))
    71
    72noncomputable def selfGram {k n b degree r : ℕ} (hr : 2 * r ≤ n) (hd : 1 ≤ degree)
    73 (M : Fin b → Matrix (Fin n) (Fin n) Binary) : Moment k n b degree :=
    74 (testerForm hr + sharpForm hd M).toMatrix'
    75
    76def matrixPair {I : Type} [Fintype I] (E : Matrix I I Binary) :
    77 Matrix I I Binary →ₗ[Binary] Binary :=
    78 ∑ i, ∑ j, E i j • matrixEntry i j
    79
    80/-- The action on all coefficient vectors induced by a common Z-coordinate change. -/
    81def changeZ {k n b degree : ℕ} (A : Matrix (Fin n) (Fin n) Binary) :
    82 Vector k n b degree →ₗ[Binary] Vector k n b degree where
    83 toFun v c := match c.2 with
    84 | some (Sum.inr (q, i)) => if q = 2 then ∑ j, A i j * v (c.1, some (free j)) else v c
    85 | _ => v c
    86 map_add' v w := by
    87 ext ⟨S, c⟩
    88 cases c with
    89 | none => rfl
    90 | some c =>
    91 cases c with
    92 | inl c => rfl
    93 | inr c =>
    94 rcases c with ⟨q, i⟩
    95 by_cases hq : q = 2 <;> simp [hq, mul_add, Finset.sum_add_distrib]
    96 map_smul' a v := by
    97 ext ⟨S, c⟩
    98 cases c with
    99 | none => rfl
    100 | some c =>
    101 cases c with
    102 | inl c => rfl
    103 | inr c =>
    104 rcases c with ⟨q, i⟩
    105 by_cases hq : q = 2 <;> simp [hq, Finset.mul_sum, mul_left_comm]
    106
    107axiom selfGram_moments {k n b degree r : ℕ} (hr : 2 * r ≤ n) (hd : 1 ≤ degree)
    108 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (w : Moment k n b degree)
    109 (hw : w ∈ momentSpace (selectorEval (degree := degree)) Set.univ) :
    110 matrixPair (selfGram hr hd M) w = eta hr w
    111
    112axiom selfGram_changeZ {k n b degree r : ℕ} (hr : 2 * r ≤ n) (hd : 1 ≤ degree)
    113 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (A : Matrix (Fin n) (Fin n) Binary) :
    114 (changeZ A).toMatrix'.transpose * selfGram (k := k) (b := b) hr hd M *
    115 (changeZ A).toMatrix' = selfGram hr hd M
    116
    117end Lax342547.ConcreteGeometry
    118
    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…