OAI/NumberTheory/Ostmann/Characters/PivotRowPhase.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.character_zpow_norm_le_one line 11
2. def OAI.Ostmann.pivotLocalRow line 21
3. theorem OAI.Ostmann.pivotLocalRow_norm_le_one line 25
4. theorem OAI.Ostmann.pivotLocalRow_eq line 35

   Source documentation

   The complete outgoing local pivot factor sees the other active product H only through u = v/H.

   theorem pivotLocalRow_eq {p : ℕ} [Fact p.Prime] (χ : DirichletCharacter ℂ p)
       (κ : ℂ) (t D Y H v u : ZMod p) (ε : ℤ)
       (hD : D ≠ 0) (hY : Y ≠ 0) (hH : H ≠ 0) (hu : u ≠ 0) (hv : v = u * H) :
       ZMod.stdAddChar (t * (v / (D * Y * H))) * κ *
         (χ v ^ (-ε) * χ (D * Y * H) ^ ε) = pivotLocalRow χ κ t D Y u ε := by
   …

   Mentions: OAI.Ostmann.pivotLocalRow

5. def OAI.Ostmann.pivotTupleRow line 52
6. theorem OAI.Ostmann.pivotTupleRow_norm_le_one line 57