ScheduledInitialPhase.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The initial Poisson phase is the initial phase of the actual schedule

def OAI.Ostmann.initialSurvivorEquiv line 12
theorem OAI.Ostmann.initialSurvivorPrimeFact line 19
theorem OAI.Ostmann.scheduledPrimePhase_zero line 24

theorem OAI.Ostmann.tupleGraphPhase_eq_regular_directed line 43

Source documentation

The Gauss multipliers are only needed at prime arguments; their values at other natural numbers do not enter the schedule.

theorem tupleGraphPhase_eq_regular_directed {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, NeZero (p i)] (χ : ∀ i, DirichletCharacter ℂ (p i))
    (t : ∀ i, ZMod (p i)) (v : ℤ) :
    tupleGraphPhase p χ t v = directedPrimePhase p χ t
      (fun i => regularUnary (χ i) (primitiveGaussPhase (χ i)) 1 (v : ZMod (p i)))
      initialCompleteGraph v := by
…

Mentions: OAI.Ostmann.tupleGraphPhase, OAI.Ostmann.directedPrimePhase, OAI.Ostmann.regularUnary, OAI.Ostmann.primitiveGaussPhase, OAI.Ostmann.initialCompleteGraph

theorem OAI.Ostmann.tupleGraphPhase_eq_scheduled line 59

Source documentation

The exact level-zero identification used by the initial-amplitude bound.

theorem tupleGraphPhase_eq_scheduled {I : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
    (κ : I → ℕ → ℂ) (pivot : ℕ → I)
    (p : I → ℕ) [∀ i, Fact (p i).Prime] (center : ∀ p : ℕ, ZMod p)
    (hκ : ∀ i, κ i (p i) = primitiveGaussPhase (χ i (p i))) (v : ℤ) :
    letI := initialSurvivorPrimeFact role p
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.primitiveGaussPhase, OAI.Ostmann.initialSurvivorPrimeFact