QuadPathReindex.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.Pairings.gatherPaths line 11
Source documentation
Zip four independently indexed paths into one path of quadruple labels.
```
def gatherPaths {ι α : Type*} (p q r s : ι → α) : ι → Labels α :=
…
```
Mentions: OAI.Problem335.Pairings.Labels
def OAI.Problem335.Pairings.quadPathsEquiv line 15
Source documentation
Four paths and a single quadruple-labelled path contain exactly the same data.
```
def quadPathsEquiv (ι α : Type*) :
    ((ι → α) × (ι → α) × (ι → α) × (ι → α)) ≃ (ι → Labels α) where
…
```
Mentions: OAI.Problem335.Pairings.Labels

theorem OAI.Problem335.Pairings.sum_quadPaths line 24

Source documentation

Reindex the four finite path loops without changing any weight.

theorem sum_quadPaths {ι α R : Type*} [Fintype ι] [DecidableEq ι] [Fintype α]
    [AddCommMonoid R] (F : (ι → Labels α) → R) :
    (∑ p : ι → α, ∑ q : ι → α, ∑ r : ι → α, ∑ s : ι → α,
      F (gatherPaths p q r s)) = ∑ x : ι → Labels α, F x := by
…

Mentions: OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.gatherPaths

theorem OAI.Problem335.Pairings.sum_quadPaths_subtype line 35

Source documentation

Reindex a restricted four-path sum as a sum over the corresponding subtype.

theorem sum_quadPaths_subtype {ι α R : Type*} [Fintype ι] [DecidableEq ι]
    [Fintype α] [AddCommMonoid R] (P : (ι → Labels α) → Prop)
    [DecidablePred P] (F : (ι → Labels α) → R) :
    (∑ p : ι → α, ∑ q : ι → α, ∑ r : ι → α, ∑ s : ι → α,
      if P (gatherPaths p q r s) then F (gatherPaths p q r s) else 0) =
      ∑ x : {x : ι → Labels α // P x}, F x.1 := by
…

Mentions: OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.gatherPaths

def OAI.Problem335.Pairings.closePath line 46
Source documentation
A single path with its two external vertices fixed at a.
```
def closePath {α : Type*} {L : ℕ} (a : α) (p : Fin L → α) :
    Fin (L + 2) → α :=
…
```
theorem OAI.Problem335.Pairings.closePath_zero line 50
theorem OAI.Problem335.Pairings.closePath_last line 53
theorem OAI.Problem335.Pairings.closePath_internal line 57
theorem OAI.Problem335.Pairings.closePaths_gather_p line 62
theorem OAI.Problem335.Pairings.closePaths_gather_q line 69
theorem OAI.Problem335.Pairings.closePaths_gather_r line 76
theorem OAI.Problem335.Pairings.closePaths_gather_s line 83

theorem OAI.Problem335.Pairings.layerLabels_gatherPaths line 91

Source documentation

The canonical layer labels are exactly the coordinates of the four closed paths.

theorem layerLabels_gatherPaths {α : Type*} {L : ℕ}
    (a : α) (p q r s : Fin L → α) (t : Fin (L + 1)) :
    layerLabels a (gatherPaths p q r s) t =
      ⟨edgeCoordinates (closePath a p) t, edgeCoordinates (closePath a q) t,
        edgeCoordinates (closePath a r) t, edgeCoordinates (closePath a s) t⟩ := by
…

Mentions: OAI.Problem335.Pairings.layerLabels, OAI.Problem335.Pairings.gatherPaths, OAI.Problem335.Pairings.edgeCoordinates, OAI.Problem335.Pairings.closePath