OAI/NumberTheory/Ostmann/Arithmetic/MovingFullPair.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingSampleBaseWeight line 11
2. def OAI.Ostmann.movingSampleFullWeight line 19
3. theorem OAI.Ostmann.moving_sample_full_weight_factor line 28
4. theorem OAI.Ostmann.moving_full_pair_good_comparison line 46

   Source documentation

   The quartet bound is now attached to the actual full coefficient, with its original arithmetic and smooth support retained in the scalar factor.

   theorem moving_full_pair_good_comparison {σ : Type*} {q : ℕ} [Fact q.Prime] (hq : 3 ≤ q)
       (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ)
       (F : Bool → MovingSlotState σ → ℤ → ℂ)
       (extra : Bool → MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (hextra : ∀ b x s v w, extra b x s v w ≠ 0 →
         (historyPivot (movingSlotSystem value childBound pivotBound) x s v w : ZMod q) ≠ 0)
       (n m : ℕ) (hm : 0 < m) (e : Equiv.Perm (TreeLeafIndex (n + 2) × Fin m))
       (hgood : 4 * Fintype.card (arrangementGraph m e).ConnectedComponent ≤
         3 * Fintype.card (TreeLeafIndex (n + 2)))
       (t : Bool → FrequencyTree ℤ (n + 2)) (small : Bool → TreeLeafTuple (List σ) (n + 2))
       (samples : Bool → MovingSampleSlots σ (n + 2))
       (hfreq : ∀ b, movingGiantFrequencyUnits q (n + 2) (t b))
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.historyPivot, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.arrangementGraph, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingGiantFrequencyUnits