OAI/NumberTheory/Ostmann/Construction/ScheduledRegularUnary.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.copyScheduleOrigin line 13

   Source documentation

   Copying never conjugates the underlying Dirichlet character.

   def copyScheduleOrigin {I : Type*} : (n : ℕ) → CopyScheduleVertex I n → I
     | 0, i => i
     | n + 1, .inl (_, i) => copyScheduleOrigin n i
     | n + 1, .inr i => copyScheduleOrigin n i

   Mentions: OAI.Ostmann.CopyScheduleVertex

2. theorem OAI.Ostmann.copyScheduleOrigin_path line 18
3. def OAI.Ostmann.regularUnary line 25

   Source documentation

   All frequency dependence of a regular unary is its current root power.

   noncomputable def regularUnary {p : ℕ} (χ : DirichletCharacter ℂ p)
       (κ : ℂ) (ε : ℤ) (v : ZMod p) : ℂ := κ * χ v ^ (-ε)

4. def OAI.Ostmann.regularCopiedMultiplier line 28
5. theorem OAI.Ostmann.regularUnary_left line 32
6. theorem OAI.Ostmann.regularUnary_right line 39
7. def OAI.Ostmann.scheduledWordMultiplier line 57

   Source documentation

   This multiplier is constructed from the role character, original Gauss multiplier, and copy signs alone; it contains no frequency parameters.

   noncomputable def scheduledWordMultiplier {p : ℕ} (χ : DirichletCharacter ℂ p) (κ : ℂ) :
       (n : ℕ) → (Fin n → Bool) → ℂ
     | 0, _ => κ
     | n + 1, t => regularCopiedMultiplier χ
         (scheduledWordMultiplier χ κ n (fun j => t j.castSucc))
         (finalCopyParity (fun j => t j.castSucc)) (t (Fin.last n))

   Mentions: OAI.Ostmann.regularCopiedMultiplier, OAI.Ostmann.finalCopyParity

8. theorem OAI.Ostmann.scheduledWordMultiplier_snoc line 64
9. theorem OAI.Ostmann.regularCopiedMultiplier_norm line 70
10. theorem OAI.Ostmann.scheduledWordMultiplier_norm line 82
11. theorem OAI.Ostmann.scheduledWordUnary_step line 90

    Source documentation

    The exact regular unary recurrence at every word copy.

    theorem scheduledWordUnary_step {p : ℕ} [Fact p.Prime]
        (χ : DirichletCharacter ℂ p) (κ : ℂ) (n : ℕ) (t : Fin n → Bool)
        (b : Bool) (v w s : ZMod p) (hv : v ≠ 0) (hw : w ≠ 0) :
        (if b then
            regularUnary χ (scheduledWordMultiplier χ κ n t) (finalCopyParity t) v *
              χ (v / s) ^ finalCopyParity t
          else
            conj (regularUnary χ (scheduledWordMultiplier χ κ n t) (finalCopyParity t) w) *
              χ (-w / s) ^ (-finalCopyParity t)) =
          regularUnary χ (scheduledWordMultiplier χ κ (n + 1) (Fin.snoc t b))
            (finalCopyParity (Fin.snoc t b)) s := by
    …

    Mentions: OAI.Ostmann.regularUnary, OAI.Ostmann.scheduledWordMultiplier, OAI.Ostmann.finalCopyParity