OAI/NumberTheory/Ostmann/Construction/TransferGraphPhase.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.retainedGraphRow line 13

   Source documentation

   The erased pivot is represented only by its total integer. Its outgoing row has already been removed by Cauchy--Schwarz.

   noncomputable def retainedGraphRow {I : Type*} [Fintype I] {p : ℕ}
       (χ : DirichletCharacter ℂ p) (b : Option I → Option I → ℤ)
       (i : I) (P : ZMod p) (q : I → ZMod p) : ℂ :=
   …

2. def OAI.Ostmann.updatedGraphRow line 18
3. theorem OAI.Ostmann.transfer_left_graph_factor line 25

   Source documentation

   The complete retained factor at a left-slot prime becomes the left local factor of the updated directed graph.

   theorem transfer_left_graph_factor {H Y : Type*} [Fintype H] [Fintype Y]
       {p : ℕ} [Fact p.Prime] (χ : DirichletCharacter ℂ p)
       (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ) (h : H)
       (P D v s t : ZMod p) (L R : H → ZMod p) (U : Y → ZMod p) (ν : ℂ)
       (hP : P ≠ 0) (hD : D ≠ 0) (hR : (∏ k, R k) ≠ 0) (hs : s ≠ 0)
       (hrel : v * (∏ k, R k) = s * P) :
       ZMod.stdAddChar (t * (v / (P * D))) * ν *
         retainedGraphRow χ b (.inl h) P (Sum.elim L U) =
       ZMod.stdAddChar (t * (s / ((∏ k, R k) * D))) *
         (ν * χ (v / s) ^ b (some (.inl h)) none) *
         updatedGraphRow χ b (.inl (true, h)) L R U := by
   …

   Mentions: OAI.Ostmann.retainedGraphRow, OAI.Ostmann.updatedGraphRow

4. theorem OAI.Ostmann.transfer_right_graph_factor line 49
5. theorem OAI.Ostmann.transfer_common_row_norm_one line 78

   Source documentation

   The common outside row has unit modulus on the actual coprime support; the self-edge is allowed because its exponent is zero.

   theorem transfer_common_row_norm_one {H Y : Type*} [Fintype H] [Fintype Y]
       {p : ℕ} (χ : DirichletCharacter ℂ p)
       (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ) (y : Y)
       (P : ZMod p) (U : Y → ZMod p) (hP : IsUnit P)
       (hU : ∀ z, z ≠ y → IsUnit (U z)) (hb : b (some (.inr y)) (some (.inr y)) = 0) :
       ‖χ P ^ b (some (.inr y)) none *
         ∏ z, χ (U z) ^ b (some (.inr y)) (some (.inr z))‖ = 1 := by
   …

6. theorem OAI.Ostmann.transfer_outside_graph_factor line 98

   Source documentation

   The shared-slot row cancels its entire common part. Its new incoming powers are exactly those prescribed by transferredGraph.

   theorem transfer_outside_graph_factor {H Y : Type*} [Fintype H] [Fintype Y]
       {p : ℕ} [Fact p.Prime] (χ : DirichletCharacter ℂ p)
       (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ) (y : Y)
       (P LP RP D v w s t : ZMod p) (L R : H → ZMod p) (U : Y → ZMod p)
       (νv νw : ℂ) (hP : P ≠ 0) (hL : LP ≠ 0) (hR : RP ≠ 0) (hD : D ≠ 0)
       (hcommon : ‖χ P ^ b (some (.inr y)) none *
         ∏ z, χ (U z) ^ b (some (.inr y)) (some (.inr z))‖ = 1)
       (hrel : v * RP - w * LP = s * P) :
       (ZMod.stdAddChar (t * (v / (P * LP * D))) * νv *
         retainedGraphRow χ b (.inr y) P (Sum.elim L U)) *
         conj (ZMod.stdAddChar (t * (w / (P * RP * D))) * νw *
           retainedGraphRow χ b (.inr y) P (Sum.elim R U)) =
   …

   Mentions: OAI.Ostmann.retainedGraphRow