SchedulePivotUnary.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual unary on every still-active pivot constituent

theorem OAI.Ostmann.copyScheduleOrigin_positive line 11

theorem OAI.Ostmann.copyScheduleUnary_pivot line 18

Source documentation

Positive future-pivot copies retain the original multiplier.

theorem copyScheduleUnary_pivot {I : Type*} (role : I → CopyScheduleRole)
    (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p) (κ : I → ℕ → ℂ)
    (pivot : ℕ → I) (hpivot : ∀ k, role (pivot k) = .pivot k)
    (i : I) (k : ℕ) (hi : role i = .pivot k) (p : ℕ) [Fact p.Prime]
    (n : ℕ) (hn : n ≤ k) (t : FrequencyTree ℤ n)
    (hfreq : ∀ s ∈ allFrequencyList n t, (s : ZMod p) ≠ 0) :
    copyScheduleUnary χ initialCompleteGraph pivot (initialRegularUnary χ κ) n t
        (copySchedulePositive n i) p =
      regularUnary (χ i p) (κ i p) 1 ((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.copySchedulePositive, OAI.Ostmann.regularUnary, OAI.Ostmann.frequencyRoot