MatrixPathVertices.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.internalPathEdges line 12
Source documentation
Record the edges of a path from its internal vertices and fixed endpoints.
```
def internalPathEdges {d : ℕ} (labels : Fin (d + 1) → σ) (i j : ι)
    (p : Fin d → ι) : List (σ × ι × ι) :=
…
```
theorem OAI.Problem335.internalPathEdges_mem line 17
theorem OAI.Problem335.internalPathEdges_injective line 37

def OAI.Problem335.internalPathIndex line 47

Source documentation

Locate the explicitly described path in the exact list enumeration.

def internalPathIndex [Fintype ι] [DecidableEq ι] {d : ℕ}
    (labels : Fin (d + 1) → σ) (i j : ι) (p : Fin d → ι) :
    Fin (matrixEntryPaths (List.ofFn labels) i j).length :=
…

Mentions: OAI.Problem335.matrixEntryPaths

theorem OAI.Problem335.get_internalPathIndex line 52
theorem OAI.Problem335.internalPathIndex_injective line 58
def OAI.Problem335.internalPathEquiv line 67
Source documentation
The canonical matrix-path list and the tuple of internal vertices enumerate exactly the same paths. The edge list is preserved, not merely its cardinality.
```
def internalPathEquiv [Fintype ι] [DecidableEq ι] (d : ℕ)
    (labels : Fin (d + 1) → σ) (i j : ι) :
    (Fin d → ι) ≃ Fin (matrixEntryPaths (List.ofFn labels) i j).length :=
…
```
Mentions: OAI.Problem335.matrixEntryPaths
theorem OAI.Problem335.get_internalPathEquiv line 76
def OAI.Problem335.EndpointPath line 82
Source documentation
Vertex paths with both external endpoints fixed.
```
def EndpointPath (d : ℕ) (i j : ι) :=
…
```
def OAI.Problem335.endpointPathEquiv line 87
Source documentation
Adjoining the two endpoints identifies arbitrary internal-vertex tuples with endpoint-fixed vertex paths.
```
def endpointPathEquiv (d : ℕ) (i j : ι) : (Fin d → ι) ≃ EndpointPath d i j where
…
```
Mentions: OAI.Problem335.EndpointPath
def OAI.Problem335.endpointPathIndexEquiv line 99
Source documentation
Representation bridge from endpoint-fixed vertices to canonical list-based paths.
```
def endpointPathIndexEquiv [Fintype ι] [DecidableEq ι] (d : ℕ)
    (labels : Fin (d + 1) → σ) (i j : ι) :
    EndpointPath d i j ≃ Fin (matrixEntryPaths (List.ofFn labels) i j).length :=
…
```
Mentions: OAI.Problem335.EndpointPath, OAI.Problem335.matrixEntryPaths

theorem OAI.Problem335.get_endpointPathIndexEquiv line 105

Source documentation

The representation equivalence preserves the exact ordered edge list.

@[simp] theorem get_endpointPathIndexEquiv [Fintype ι] [DecidableEq ι] (d : ℕ)
    (labels : Fin (d + 1) → σ) (i j : ι) (v : EndpointPath d i j) :
    (matrixEntryPaths (List.ofFn labels) i j).get
      (endpointPathIndexEquiv d labels i j v) =
      List.ofFn (fun t : Fin (d + 1) => (labels t, v.1 t.castSucc, v.1 t.succ)) := by
…

Mentions: OAI.Problem335.EndpointPath, OAI.Problem335.matrixEntryPaths, OAI.Problem335.endpointPathIndexEquiv

instance OAI.Problem335.endpointPathFintype line 122
theorem OAI.Problem335.card_endpointPath line 126

theorem OAI.Problem335.sum_matrixEntryPaths_eq_sum_internal line 133

Source documentation

Reindex any path statistic from enumerated paths to internal vertices.

theorem sum_matrixEntryPaths_eq_sum_internal [Fintype ι] [DecidableEq ι]
    {R : Type*} [AddCommMonoid R] (d : ℕ)
    (labels : Fin (d + 1) → σ) (i j : ι) (f : List (σ × ι × ι) → R) :
    (∑ p : Fin (matrixEntryPaths (List.ofFn labels) i j).length,
      f ((matrixEntryPaths (List.ofFn labels) i j).get p)) =
      ∑ p : Fin d → ι, f (internalPathEdges labels i j p) := by
…

Mentions: OAI.Problem335.matrixEntryPaths, OAI.Problem335.internalPathEdges

theorem OAI.Problem335.sum_matrixEntryPaths_eq_sum_vertices line 145

Source documentation

Reindex any path statistic to the endpoint-fixed vertex representation. This can be applied once per path in the four-path trace expansion.

theorem sum_matrixEntryPaths_eq_sum_vertices [Fintype ι] [DecidableEq ι]
    {R : Type*} [AddCommMonoid R] (d : ℕ)
    (labels : Fin (d + 1) → σ) (i j : ι) (f : List (σ × ι × ι) → R) :
    (∑ p : Fin (matrixEntryPaths (List.ofFn labels) i j).length,
      f ((matrixEntryPaths (List.ofFn labels) i j).get p)) =
      ∑ v : EndpointPath d i j,
        f (List.ofFn (fun t : Fin (d + 1) => (labels t, v.1 t.castSucc, v.1 t.succ))) := by
…

Mentions: OAI.Problem335.matrixEntryPaths, OAI.Problem335.EndpointPath

theorem OAI.Problem335.sum_get_endpointPathIndexEquiv line 157

Source documentation

Additive edge statistics, including signed exponent shifts, are preserved.

theorem sum_get_endpointPathIndexEquiv [Fintype ι] [DecidableEq ι]
    {A : Type*} [AddCommMonoid A] (d : ℕ) (labels : Fin (d + 1) → σ)
    (i j : ι) (v : EndpointPath d i j) (f : σ × ι × ι → A) :
    (((matrixEntryPaths (List.ofFn labels) i j).get
      (endpointPathIndexEquiv d labels i j v)).map f).sum =
      ∑ t : Fin (d + 1), f (labels t, v.1 t.castSucc, v.1 t.succ) := by
…

Mentions: OAI.Problem335.EndpointPath, OAI.Problem335.matrixEntryPaths, OAI.Problem335.endpointPathIndexEquiv

theorem OAI.Problem335.prod_get_endpointPathIndexEquiv line 167

Source documentation

Multiplicative edge statistics, including path amplitudes, are preserved.

theorem prod_get_endpointPathIndexEquiv [Fintype ι] [DecidableEq ι]
    {A : Type*} [CommMonoid A] (d : ℕ) (labels : Fin (d + 1) → σ)
    (i j : ι) (v : EndpointPath d i j) (f : σ × ι × ι → A) :
    (((matrixEntryPaths (List.ofFn labels) i j).get
      (endpointPathIndexEquiv d labels i j v)).map f).prod =
      ∏ t : Fin (d + 1), f (labels t, v.1 t.castSucc, v.1 t.succ) := by
…

Mentions: OAI.Problem335.EndpointPath, OAI.Problem335.matrixEntryPaths, OAI.Problem335.endpointPathIndexEquiv