OAI/NumberTheory/Ostmann/Construction/ScheduledSamplePhase.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduledPrimePhase_congr_labels line 12
2. def OAI.Ostmann.scheduledSamplePhase line 23
3. theorem OAI.Ostmann.scheduledSamplePhase_partition line 34

   Source documentation

   Finite Fubini and the arithmetic transfer evaluate literally the same scheduled phase after the pivot/H/Y reindexing.

   theorem scheduledSamplePhase_partition {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
       (κ : I → ℕ → ℂ) (pivot : ℕ → I) (n r : ℕ)
       (e : Fin r ≃ CurrentPivotConstituent role n) (t : FrequencyTree ℤ n)
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (u : CopyScheduleY role n → P) (x : Fin r → P) (l : CopyScheduleH role n → P)
       (center : ∀ p : ℕ, ZMod p) :
       letI : ∀ h, Fact (l h : ℕ).Prime := fun h => ⟨hP _ (l h).property⟩
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CurrentPivotConstituent, OAI.Ostmann.FrequencyTree, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleH