MatrixPaths.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.matrixEntryPaths line 14

Source documentation

All labelled paths through a nonempty sequence of matrix layers. The empty sequence uses the usual identity-matrix path convention.

def matrixEntryPaths [Fintype ι] [DecidableEq ι] :
    List σ → ι → ι → List (List (σ × ι × ι))
  | [], i, j => if i = j then [[]] else []
  | [t], i, j => [[(t, i, j)]]
  | t :: u :: ts, i, j =>
      (Finset.univ.toList).flatMap fun k =>
        (matrixEntryPaths (u :: ts) k j).map fun p => (t, i, k) :: p

theorem OAI.Problem335.list_sum_map_flatMap line 22

theorem OAI.Problem335.matrixEntryPaths_labels line 30

Source documentation

A path through labels chooses exactly one entry in each layer.

theorem matrixEntryPaths_labels [Fintype ι] [DecidableEq ι]
    (labels : List σ) (i j : ι) (p : List (σ × ι × ι))
    (hp : p ∈ matrixEntryPaths labels i j) : p.map Prod.fst = labels := by
…

Mentions: OAI.Problem335.matrixEntryPaths

theorem OAI.Problem335.matrixEntryPaths_path_length line 45

Source documentation

Every enumerated path has one edge per layer.

theorem matrixEntryPaths_path_length [Fintype ι] [DecidableEq ι]
    (labels : List σ) (i j : ι) (p : List (σ × ι × ι))
    (hp : p ∈ matrixEntryPaths labels i j) : p.length = labels.length := by
…

Mentions: OAI.Problem335.matrixEntryPaths

theorem OAI.Problem335.matrixEntryPaths_length line 52

Source documentation

The number of internal-index paths through a nonempty list of layers.

theorem matrixEntryPaths_length [Fintype ι] [DecidableEq ι]
    (labels : List σ) (hne : labels ≠ []) (i j : ι) :
    (matrixEntryPaths labels i j).length = Fintype.card ι ^ (labels.length - 1) := by
…

Mentions: OAI.Problem335.matrixEntryPaths

theorem OAI.Problem335.matrixEntryPaths_sum_prod line 66

Source documentation

Matrix multiplication is the sum of the products along its labelled paths.

theorem matrixEntryPaths_sum_prod [Fintype ι] [DecidableEq ι] [Semiring R]
    (A : σ → Matrix ι ι R) (labels : List σ) (i j : ι) :
    ((matrixEntryPaths labels i j).map
      (fun p => (p.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

theorem OAI.Problem335.sum_fin_succ_functions line 83

Source documentation

Split a finite tuple into its first coordinate and its tail in a finite sum.

theorem sum_fin_succ_functions [Fintype ι] [AddCommMonoid R] {d : ℕ}
    (f : (Fin (d + 1) → ι) → R) :
    (∑ p, f p) = ∑ k : ι, ∑ p : Fin d → ι, f (Fin.cons k p) := by
…

theorem OAI.Problem335.matrix_ofFn_prod_eq_sum_paths line 92

Source documentation

A matrix-product entry expanded over the finite tuple of internal vertices.

theorem matrix_ofFn_prod_eq_sum_paths [Fintype ι] [DecidableEq ι] [Semiring R]
    (d : ℕ) (A : Fin (d + 1) → Matrix ι ι R) (i j : ι) :
    (List.ofFn A).prod i j =
      ∑ p : Fin d → ι,
        (List.ofFn fun t : Fin (d + 1) =>
          A t (Fin.cons (α := fun _ => ι) i p t) (Fin.snoc (α := fun _ => ι) p j t)).prod := by
…

theorem OAI.Problem335.matrixEntryPaths_get_labels line 112

Source documentation

The labels of a path selected by its finite-list index.

theorem matrixEntryPaths_get_labels [Fintype ι] [DecidableEq ι]
    (labels : List σ) (i j : ι) (p : Fin (matrixEntryPaths labels i j).length) :
    ((matrixEntryPaths labels i j).get p).map Prod.fst = labels :=
…

Mentions: OAI.Problem335.matrixEntryPaths

theorem OAI.Problem335.matrixEntryPaths_get_length line 118

Source documentation

Each list-indexed path has exactly as many edges as the list has layers.

theorem matrixEntryPaths_get_length [Fintype ι] [DecidableEq ι]
    (labels : List σ) (i j : ι) (p : Fin (matrixEntryPaths labels i j).length) :
    ((matrixEntryPaths labels i j).get p).length = labels.length :=
…

Mentions: OAI.Problem335.matrixEntryPaths

theorem OAI.Problem335.matrixEntryPaths_sum_get line 124

Source documentation

The entry expansion in the finite-list-index form used by circuit gates.

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

Mentions: OAI.Problem335.matrixEntryPaths

theorem OAI.Problem335.matrix_block_prod line 139

Source documentation

Consecutive blocks may be multiplied before multiplying the whole sequence.

theorem matrix_block_prod [Fintype ι] [DecidableEq ι] [Semiring R]
    (A : σ → Matrix ι ι R) (blocks : List (List σ)) :
    (blocks.map (fun block => (block.map A).prod)).prod =
      (blocks.flatten.map A).prod := by
…

theorem OAI.Problem335.map_block_get_finRange line 146

Source documentation

Enumerating the block-index list and selecting blocks recovers the block list.

theorem map_block_get_finRange {β : Type*} (blocks : List (List σ))
    (f : List σ → β) :
    (List.finRange blocks.length).map (fun b => f (blocks.get b)) = blocks.map f := by
…

theorem OAI.Problem335.matrix_blocks_sum_get line 154

Source documentation

Apply the path expansion to the matrix products of the consecutive blocks.

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

Mentions: OAI.Problem335.matrixEntryPaths