TransferGraphRows.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The row products of the actual transferred directed graph

def OAI.Ostmann.transferredLabels line 12

theorem OAI.Ostmann.transferredGraph_left_row line 19

Source documentation

This is the full left row, including the harmless zero diagonal exponent. The cross-copy row is exactly the old incoming pivot column.

theorem transferredGraph_left_row {H Y : Type*} [Fintype H] [Fintype Y]
    {p : ℕ} (χ : DirichletCharacter ℂ p)
    (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ)
    (L R : H → ZMod p) (U : Y → ZMod p) (h : H) :
    (∏ j, χ (transferredLabels L R U j) ^ transferredGraph b (.inl (true, h)) j) =
      (∏ k, χ (L k) ^ b (some (.inl h)) (some (.inl k))) *
      (∏ k, χ (R k) ^ b (some (.inl h)) none) *
      (∏ y, χ (U y) ^ b (some (.inl h)) (some (.inr y))) := by
…

Mentions: OAI.Ostmann.transferredLabels, OAI.Ostmann.transferredGraph

theorem OAI.Ostmann.transferredGraph_right_row line 33

Source documentation

The conjugated right row has precisely the negated same-copy and incoming-pivot exponents.

theorem transferredGraph_right_row {H Y : Type*} [Fintype H] [Fintype Y]
    {p : ℕ} (χ : DirichletCharacter ℂ p)
    (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ)
    (L R : H → ZMod p) (U : Y → ZMod p) (h : H) :
    (∏ j, χ (transferredLabels L R U j) ^ transferredGraph b (.inl (false, h)) j) =
      (∏ k, χ (L k) ^ (-b (some (.inl h)) none)) *
      (∏ k, χ (R k) ^ (-b (some (.inl h)) (some (.inl k)))) *
      (∏ y, χ (U y) ^ (-b (some (.inl h)) (some (.inr y)))) := by
…

Mentions: OAI.Ostmann.transferredLabels, OAI.Ostmann.transferredGraph

theorem OAI.Ostmann.transferredGraph_outside_row line 46

Source documentation

Shared outside rows lose every shared-to-shared edge.

theorem transferredGraph_outside_row {H Y : Type*} [Fintype H] [Fintype Y]
    {p : ℕ} (χ : DirichletCharacter ℂ p)
    (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ)
    (L R : H → ZMod p) (U : Y → ZMod p) (y : Y) :
    (∏ j, χ (transferredLabels L R U j) ^ transferredGraph b (.inr y) j) =
      (∏ k, χ (L k) ^ b (some (.inr y)) (some (.inl k))) *
      (∏ k, χ (R k) ^ (-b (some (.inr y)) (some (.inl k)))) := by
…

Mentions: OAI.Ostmann.transferredLabels, OAI.Ostmann.transferredGraph