OAI/NumberTheory/Ostmann/Arithmetic/MovingFullSpectator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_full_coefficient_spectator_diagram line 13

   Source documentation

   The diagram is fixed before the bulk values and giants are supplied. Its equality with the full coefficient is proved from the recursive weight, including every original cutoff and the compensation divisibility tests.

   theorem moving_full_coefficient_spectator_diagram {σ : 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)
       (n : ℕ) (t : FrequencyTree ℤ n) (small : TreeLeafTuple (List σ) n)
       (samples : MovingSampleSlots σ n)
       (hfreq : movingGiantFrequencyUnits q n t)
       (hsmall : ((treeLeafProduct n (movingSlotValues value n small) : ℕ) : ZMod q) ≠ 0)
       (hsamples : (samples.values value).UnitsAt q) :
       ∃ (C : (ZMod q)ˣ) (R : RationalTreeData (ZMod q)ˣ n C),
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.historyPivot, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingGiantFrequencyUnits, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.movingSlotValues, OAI.Ostmann.RationalTreeData