OAI/Algebra/DepthFive/ImmBlocks.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.immBlock line 13

   Source documentation

   Each block of layer labels represents the product of its matrices.

   def immBlock (K : Type*) [CommSemiring K] (n : ℕ) (labels : List (Fin n)) :
       Matrix (Fin n) (Fin n) (MvPolynomial (Fin n × Fin n × Fin n) K) :=
   …

2. theorem OAI.Problem335.imm_eq_blocks_prod line 18

   Source documentation

   Regrouping consecutive layers does not change the iterated matrix product.

   theorem imm_eq_blocks_prod (hn : 0 < n) (blocks : List (List (Fin n)))
       (hblocks : blocks.flatten = List.finRange n) :
       imm K n = ((blocks.map (immBlock K n)).prod) ⟨0, hn⟩ ⟨0, hn⟩ := by
   …

   Mentions: OAI.Problem335.imm, OAI.Problem335.immBlock

3. theorem OAI.Problem335.imm_eq_blocks_path_sum line 34

   Source documentation

   The outer path expansion of the block matrices computes imm.

   theorem imm_eq_blocks_path_sum (hn : 0 < n) (blocks : List (List (Fin n)))
       (hblocks : blocks.flatten = List.finRange n) :
       imm K n =
         ((matrixEntryPaths (List.finRange blocks.length) (⟨0, hn⟩ : Fin n) ⟨0, hn⟩).map
           (fun p => (p.map (fun e =>
             immBlock K n (blocks.get e.1) e.2.1 e.2.2)).prod)).sum := by
   …

   Mentions: OAI.Problem335.imm, OAI.Problem335.matrixEntryPaths, OAI.Problem335.immBlock