OAI/NumberTheory/Ostmann/Construction/TransferLocalPhases.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.transfer_left_division line 12
2. theorem OAI.Ostmann.transfer_outside_division line 21
3. theorem OAI.Ostmann.transfer_left_additive line 31

   Source documentation

   At a left-slot prime the right branch survives modulo p.

   theorem transfer_left_additive {p : ℕ} [Fact p.Prime]
       (P R D v s t : ZMod p) (hP : P ≠ 0) (hR : R ≠ 0) (hD : D ≠ 0)
       (hrel : v * R = s * P) :
       ZMod.stdAddChar (t * (v / (P * D))) =
         ZMod.stdAddChar (t * (s / (R * D))) := by
   …

4. theorem OAI.Ostmann.transfer_right_additive line 39

   Source documentation

   At a right-slot prime conjugation supplies the minus sign.

   theorem transfer_right_additive {p : ℕ} [Fact p.Prime]
       (P L D w s t : ZMod p) (hP : P ≠ 0) (hL : L ≠ 0) (hD : D ≠ 0)
       (hrel : -w * L = s * P) :
       conj (ZMod.stdAddChar (t * (w / (P * D)))) =
         ZMod.stdAddChar (t * (s / (L * D))) := by
   …

5. theorem OAI.Ostmann.transfer_outside_additive line 50

   Source documentation

   Outside slots occur in both branches and their translation differences combine at the new signed frequency.

   theorem transfer_outside_additive {p : ℕ} [Fact p.Prime]
       (P L R D v w s t : ZMod p)
       (hP : P ≠ 0) (hL : L ≠ 0) (hR : R ≠ 0) (hD : D ≠ 0)
       (hrel : v * R - w * L = s * P) :
       ZMod.stdAddChar (t * (v / (P * L * D))) *
           conj (ZMod.stdAddChar (t * (w / (P * R * D)))) =
         ZMod.stdAddChar (t * (s / (L * R * D))) := by
   …

6. theorem OAI.Ostmann.mulChar_div line 60
7. theorem OAI.Ostmann.transfer_left_character line 65

   Source documentation

   The incoming pivot column becomes a cross-branch character factor.

   theorem transfer_left_character {p : ℕ} [Fact p.Prime]
       (χ : DirichletCharacter ℂ p) (P R v s : ZMod p) (hs : s ≠ 0)
       (hrel : v * R = s * P) : χ P = χ (v / s) * χ R := by
   …

8. theorem OAI.Ostmann.transfer_regular_unary line 76

   Source documentation

   Frequency factors cancel in every regular outgoing row, for either sign.

   theorem transfer_regular_unary {p : ℕ} [Fact p.Prime]
       (χ : DirichletCharacter ℂ p) (v s : ZMod p) (hv : v ≠ 0) (ε : ℤ) :
       χ v ^ (-ε) * χ (v / s) ^ ε = χ s ^ (-ε) := by
   …

9. theorem OAI.Ostmann.character_product_power line 83
10. theorem OAI.Ostmann.conjugate_character_power line 88
11. theorem OAI.Ostmann.transfer_incoming_character line 93
12. theorem OAI.Ostmann.transfer_left_regular_factor line 99
13. theorem OAI.Ostmann.transfer_right_regular_factor line 108

    Source documentation

    The new right unary has the reversed frequency exponent; its extra minus-one factor is independent of every frequency.

    theorem transfer_right_regular_factor {p : ℕ} [Fact p.Prime]
        (χ : DirichletCharacter ℂ p) (P L w s : ZMod p) (hw : w ≠ 0) (hs : s ≠ 0)
        (hrel : -w * L = s * P) (ε : ℤ) :
        conj (χ w ^ (-ε) * χ P ^ ε) =
          χ (-1) ^ (-ε) * χ s ^ ε * χ L ^ (-ε) := by
    …