OAI/NumberTheory/Ostmann/Construction/CopyScheduleUnary.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.copyScheduleUnary line 14
2. theorem OAI.Ostmann.copyScheduleUnary_norm_le_one line 31
3. theorem OAI.Ostmann.copyScheduleUnary_update line 53

   Source documentation

   The local unary produced by the proved transfer is the restriction of this single recursively defined schedule unary.

   theorem copyScheduleUnary_update {I : Type*} (role : I → CopyScheduleRole)
       (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
       (g : I → I → ℤ) (pivot : ℕ → I) (initial : I → ℤ → ℕ → ℂ)
       (n : ℕ) (t : FrequencyTree ℤ (n + 1))
       (q : (Bool × CopyScheduleH role n) ⊕ CopyScheduleY role n → ℕ)
       [∀ i, Fact (q i).Prime]
       (i : (Bool × CopyScheduleH role n) ⊕ CopyScheduleY role n) :
       copiedSlotUnary q (fun h => χ (copyScheduleOrigin n h.val))
         (scheduledRetainedGraph role g pivot n)
         (fun h => copyScheduleUnary χ g pivot initial n t.2.1 h.val (q (.inl (true, h))))
         (fun h => copyScheduleUnary χ g pivot initial n t.2.2 h.val (q (.inl (false, h))))
         (fun y => copyScheduleUnary χ g pivot initial n t.2.1 y.val (q (.inr y)))
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FrequencyTree, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.copiedSlotUnary, OAI.Ostmann.copyScheduleOrigin, OAI.Ostmann.scheduledRetainedGraph, OAI.Ostmann.copyScheduleUnary