OAI/Algebra/DepthFive/MatrixPathSemantics.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.map_finRange_get_eq line 14

   Source documentation

   Replace a list by its enumeration through finite indices, under an arbitrary map.

   theorem map_finRange_get_eq {α β : Type*} (xs : List α) (f : α → β) :
       ((List.finRange xs.length).map (fun k => f (xs.get k))) = xs.map f := by
   …

2. theorem OAI.Problem335.matrixEntryPaths_get_sum_prod line 20

   Source documentation

   Matrix-path expansion in the finite-index form used by circuit input lists.

   theorem matrixEntryPaths_get_sum_prod [Fintype ι] [DecidableEq ι] [Semiring R]
       (A : σ → Matrix ι ι R) (labels : List σ) (i j : ι) :
       ((List.finRange (matrixEntryPaths labels i j).length).map
         (fun k => (((matrixEntryPaths labels i j).get k).map
           (fun e => A e.1 e.2.1 e.2.2)).prod)).sum =
         ((labels.map A).prod) i j := by
   …

   Mentions: OAI.Problem335.matrixEntryPaths

3. theorem OAI.Problem335.matrixEntryPaths_fin_sum_prod line 31

   Source documentation

   The same expansion as a finite sum, convenient for finite-type gate constructors.

   theorem matrixEntryPaths_fin_sum_prod [Fintype ι] [DecidableEq ι] [Semiring R]
       (A : σ → Matrix ι ι R) (labels : List σ) (i j : ι) :
       (∑ k : Fin (matrixEntryPaths labels i j).length,
         (((matrixEntryPaths labels i j).get k).map
           (fun e => A e.1 e.2.1 e.2.2)).prod) =
         ((labels.map A).prod) i j := by
   …

   Mentions: OAI.Problem335.matrixEntryPaths

4. theorem OAI.Problem335.matrixEntryPaths_get_weight_sum line 46

   Source documentation

   Every finite-indexed path contributes its label's declared degree exactly once.

   theorem matrixEntryPaths_get_weight_sum [Fintype ι] [DecidableEq ι]
       (labels : List σ) (i j : ι) (w : σ → ℕ)
       (k : Fin (matrixEntryPaths labels i j).length) :
       ((((matrixEntryPaths labels i j).get k).map (fun e => w e.1)).sum) =
         (labels.map w).sum := by
   …

   Mentions: OAI.Problem335.matrixEntryPaths

5. theorem OAI.Problem335.matrixEntryPaths_get_sum_monomial line 56

   Source documentation

   Each block-entry middle gate sums precisely the variable monomials of its matrix product.

   theorem matrixEntryPaths_get_sum_monomial (K : Type*) [CommSemiring K] (n : ℕ)
       (labels : List (Fin n)) (i j : Fin n) :
       ((List.finRange (matrixEntryPaths labels i j).length).map
         (fun k => (((matrixEntryPaths labels i j).get k).map
           (fun e => (MvPolynomial.X e : MvPolynomial (Fin n × Fin n × Fin n) K))).prod)).sum =
         ((labels.map (immLayer K n)).prod) i j := by
   …

   Mentions: OAI.Problem335.matrixEntryPaths, OAI.Problem335.immLayer