MatrixPathPairings.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.Pairings.matrixPathLabelsEquiv line 14
Source documentation
Apply a representation equivalence independently to the four paths.
```
def matrixPathLabelsEquiv (e : α ≃ β) : Labels α ≃ Labels β where
…
```
Mentions: OAI.Problem335.Pairings.Labels
def OAI.Problem335.Pairings.matrixPathFunctionEquiv line 21
Source documentation
Transpose four vertex functions into four labels at each vertex.
```
def matrixPathFunctionEquiv (d : ℕ) : Labels (Fin d → α) ≃ (Fin d → Labels α) where
…
```
Mentions: OAI.Problem335.Pairings.Labels
def OAI.Problem335.Pairings.quadruplePathIndexEquiv line 29
Source documentation
Quadruples of exact enumerated matrix paths have the internal-label representation used by RelaxedPaths and CompatiblePaths.
```
def quadruplePathIndexEquiv [Fintype α] [DecidableEq α] (d : ℕ)
    (labels : Fin (d + 1) → σ) (a : α) :
    (Fin d → Labels α) ≃ Labels (Fin (matrixEntryPaths (List.ofFn labels) a a).length) :=
…
```
Mentions: OAI.Problem335.Pairings.Labels, OAI.Problem335.matrixEntryPaths
theorem OAI.Problem335.Pairings.quadruplePathIndexEquiv_get_p line 35
theorem OAI.Problem335.Pairings.quadruplePathIndexEquiv_get_q line 41
theorem OAI.Problem335.Pairings.quadruplePathIndexEquiv_get_r line 47
theorem OAI.Problem335.Pairings.quadruplePathIndexEquiv_get_s line 53
theorem OAI.Problem335.Pairings.project_closePaths line 60
Source documentation
Coordinate projections commute with adjoining the fixed external vertices.
```
theorem project_closePaths (d : ℕ) (a : α) (x : Fin d → Labels α)
    (proj : Labels α → α) (hp : ∀ a, proj (constantLabels a) = a) :
    (fun t => proj (closePaths a x t)) =
      Fin.cons a (Fin.snoc (fun t => proj (x t)) a) := by
…
```
Mentions: OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.constantLabels, OAI.Problem335.Pairings.closePaths

theorem OAI.Problem335.Pairings.internalPathEdges_project_closePaths line 72

Source documentation

Exact ordered edges after projecting any of the four closed coordinate paths.

theorem internalPathEdges_project_closePaths (d : ℕ)
    (labels : Fin (d + 1) → σ) (a : α) (x : Fin d → Labels α)
    (proj : Labels α → α) (hp : ∀ a, proj (constantLabels a) = a) :
    internalPathEdges labels a a (fun t => proj (x t)) =
      List.ofFn (fun t : Fin (d + 1) =>
        (labels t, proj (closePaths a x t.castSucc), proj (closePaths a x t.succ))) := by
…

Mentions: OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.constantLabels, OAI.Problem335.internalPathEdges, OAI.Problem335.Pairings.closePaths

def OAI.Problem335.Pairings.matrixPathLabelsProdEquiv line 89
Source documentation
The four-field record is a nested Cartesian product.
```
def matrixPathLabelsProdEquiv : Labels α ≃ α × α × α × α where
…
```
Mentions: OAI.Problem335.Pairings.Labels

theorem OAI.Problem335.Pairings.sum_matrixPathLabels line 96

Source documentation

A sum over four-field records is precisely the iterated fourfold sum.

theorem sum_matrixPathLabels [Fintype α] {R : Type*} [AddCommMonoid R]
    (f : Labels α → R) :
    (∑ x : Labels α, f x) = ∑ p : α, ∑ q : α, ∑ r : α, ∑ s : α, f ⟨p,q,r,s⟩ := by
…

Mentions: OAI.Problem335.Pairings.Labels

theorem OAI.Problem335.Pairings.sum_four_matrixEntryPaths_eq line 104

Source documentation

Reindex the complete four-path sum into the exact internal-label space used by pairing classification. No positivity or compatibility premise is required.

theorem sum_four_matrixEntryPaths_eq [Fintype α] [DecidableEq α]
    {R : Type*} [AddCommMonoid R] (d : ℕ)
    (labels : Fin (d + 1) → σ) (a : α)
    (f : List (σ × α × α) → List (σ × α × α) →
      List (σ × α × α) → List (σ × α × α) → R) :
    (∑ p : Fin (matrixEntryPaths (List.ofFn labels) a a).length,
      ∑ q : Fin (matrixEntryPaths (List.ofFn labels) a a).length,
      ∑ r : Fin (matrixEntryPaths (List.ofFn labels) a a).length,
      ∑ s : Fin (matrixEntryPaths (List.ofFn labels) a a).length,
        f ((matrixEntryPaths (List.ofFn labels) a a).get p)
          ((matrixEntryPaths (List.ofFn labels) a a).get q)
          ((matrixEntryPaths (List.ofFn labels) a a).get r)
…

Mentions: OAI.Problem335.matrixEntryPaths