OAI/NumberTheory/Ostmann/Construction/ScheduleWordUnary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.initialRegularUnary line 11
2. theorem OAI.Ostmann.copyScheduleUnary_word line 17

   Source documentation

   All frequency dependence in an actual regular word slot is exactly its current root character power. The remaining multiplier depends on its copy path.

   theorem copyScheduleUnary_word {I : Type*} (role : I → CopyScheduleRole)
       (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p) (κ : I → ℕ → ℂ)
       (pivot : ℕ → I) (hpivot : ∀ k, role (pivot k) = .pivot k)
       (i : I) (hi : role i = .word) (p : ℕ) [Fact p.Prime]
       (n : ℕ) (t : FrequencyTree ℤ n) (path : Fin n → Bool)
       (hfreq : ∀ s ∈ allFrequencyList n t, (s : ZMod p) ≠ 0) :
       copyScheduleUnary χ initialCompleteGraph pivot (initialRegularUnary χ κ) n t
           (copySchedulePath n path i) p =
         regularUnary (χ i p) (scheduledWordMultiplier (χ i p) (κ i p) n path)
           (finalCopyParity path) ((frequencyRoot n t : ℤ) : ZMod p) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FrequencyTree, OAI.Ostmann.allFrequencyList, OAI.Ostmann.copyScheduleUnary, OAI.Ostmann.initialCompleteGraph, OAI.Ostmann.initialRegularUnary, OAI.Ostmann.copySchedulePath, OAI.Ostmann.regularUnary, OAI.Ostmann.scheduledWordMultiplier, OAI.Ostmann.finalCopyParity, OAI.Ostmann.frequencyRoot