OAI/NumberTheory/Ostmann/Arithmetic/MovingSlotSpectator.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingSlotModulus line 11
2. def OAI.Ostmann.movingSlotSpectator line 17
3. theorem OAI.Ostmann.movingSlotWeight_spectator line 30

   Source documentation

   The full smooth/guarded coefficient factors by the actual spectator history. All original cutoffs stay in the first factor.

   theorem movingSlotWeight_spectator {σ : Type*} {q : ℕ} [Fact q.Prime]
       (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ)
       (F : MovingSlotState σ → ℤ → ℂ)
       (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (hextra : ∀ x s v w, extra x s v w ≠ 0 →
         (historyPivot (movingSlotSystem value childBound pivotBound) x s v w : ZMod q) ≠ 0)
       (g : ZMod q → ℂ) (D : (ZMod q)ˣ)
       {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
       (XL XR : ℕ) :
       recursiveTransferWeight (movingSlotSystem value childBound pivotBound)
           (fun x s => F x s * spectatorHistoryLeaf (movingSlotModulus value) g D x s)
           (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t =
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.historyPivot, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.spectatorHistoryLeaf, OAI.Ostmann.movingSlotModulus, OAI.Ostmann.movingSlotCutoff