PathShifts.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.pathShift line 11

Source documentation

The signed occupation shift of a layered path.

def pathShift {α : Type*} {n : ℕ} (sgn : Fin n → ℤ)
    (p : Fin (n + 1) → α) : (Fin n × α × α) →₀ ℤ :=
…

theorem OAI.Problem335.pathShift_apply line 16

Source documentation

A coordinate in one layer can only come from that layer.

theorem pathShift_apply {α : Type*} [DecidableEq α] {n : ℕ} (sgn : Fin n → ℤ)
    (p : Fin (n + 1) → α) (t : Fin n) (a b : α) :
    pathShift sgn p (t, a, b) =
      if (p t.castSucc, p t.succ) = (a, b) then sgn t else 0 := by
…

Mentions: OAI.Problem335.pathShift

theorem OAI.Problem335.pathShift_eq_imp_edges_eq line 29

Source documentation

Nonzero signed shifts remember every edge of their path.

theorem pathShift_eq_imp_edges_eq {α : Type*} {n : ℕ}
    (sgn : Fin n → ℤ) (hs : ∀ t, sgn t ≠ 0)
    {p q : Fin (n + 1) → α} (heq : pathShift sgn p = pathShift sgn q)
    (t : Fin n) :
    (p t.castSucc, p t.succ) = (q t.castSucc, q t.succ) := by
…

Mentions: OAI.Problem335.pathShift

theorem OAI.Problem335.pathShift_eq_imp_eq_of_start_eq line 43

Source documentation

Even a zero-length path is determined by its starting vertex and shift.

theorem pathShift_eq_imp_eq_of_start_eq {α : Type*} {n : ℕ}
    (sgn : Fin n → ℤ) (hs : ∀ t, sgn t ≠ 0)
    {p q : Fin (n + 1) → α} (hstart : p 0 = q 0)
    (heq : pathShift sgn p = pathShift sgn q) : p = q := by
…

Mentions: OAI.Problem335.pathShift

theorem OAI.Problem335.pathShift_injective line 52

Source documentation

For positive length, no endpoint assumption is needed.

theorem pathShift_injective {α : Type*} {n : ℕ} (hn : 0 < n)
    (sgn : Fin n → ℤ) (hs : ∀ t, sgn t ≠ 0) :
    Function.Injective (pathShift (α := α) sgn) := by
…

Mentions: OAI.Problem335.pathShift

theorem OAI.Problem335.translated_pathShift_injective line 61

Source documentation

Translating the path shifts by one input occupation does not merge paths.

theorem translated_pathShift_injective {α : Type*} {n : ℕ} (hn : 0 < n)
    (sgn : Fin n → ℤ) (hs : ∀ t, sgn t ≠ 0)
    (input : (Fin n × α × α) →₀ ℤ) :
    Function.Injective (fun p : Fin (n + 1) → α => input + pathShift sgn p) := by
…

Mentions: OAI.Problem335.pathShift

theorem OAI.Problem335.pathShift_sub_eq_iff line 71

Source documentation

Global compatibility of four path shifts is exactly compatibility in each layer separately. The nonzero signs cancel, so the local condition is independent of whether that layer differentiates or multiplies.

theorem pathShift_sub_eq_iff {α : Type*} {n : ℕ}
    (sgn : Fin n → ℤ) (hs : ∀ t, sgn t ≠ 0)
    (p q r s : Fin (n + 1) → α) :
    pathShift sgn p - pathShift sgn q = pathShift sgn r - pathShift sgn s ↔
      ∀ t : Fin n,
        Finsupp.single (p t.castSucc, p t.succ) (1 : ℤ) -
          Finsupp.single (q t.castSucc, q t.succ) 1 =
        Finsupp.single (r t.castSucc, r t.succ) 1 -
          Finsupp.single (s t.castSucc, s t.succ) 1 := by
…

Mentions: OAI.Problem335.pathShift