OAI/NumberTheory/Ostmann/Arithmetic/FrozenSpectatorGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.exists_frozenSpectatorGain line 12

   Source documentation

   The tolerance and threshold depend only on the fixed depth and the requested exponential saving. All base values, sample trees, matchings and bulk lengths remain variable.

   theorem exists_frozenSpectatorGain (n : ℕ) (C D : ℝ) :
       ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 ∧ ∃ N : ℕ, 3 ≤ N ∧
         ∀ (q : ℕ) [Fact q.Prime], N ≤ q →
         ∀ (σ : Type*) (base : σ → ℕ) (m : ℕ), 0 < m →
         ∀ (t : Bool → FrequencyTree ℤ (n + 2))
           (small : Bool → TreeLeafTuple (List σ) (n + 2))
           (samples : Bool → MovingSampleSlots σ (n + 2)),
         (∀ b, movingGiantFrequencyUnits q (n + 2) (t b)) →
         (∀ b, ((treeLeafProduct (n + 2) (movingSlotValues base (n + 2) (small b)) : ℕ) :
           ZMod q) ≠ 0) →
         (∀ b, ((samples b).values base).UnitsAt q) →
         ∀ (twist : Bool → (ZMod q)ˣ) (e : Equiv.Perm (TreeLeafIndex (n + 2) × Fin m)),
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingGiantFrequencyUnits, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.movingSlotValues, OAI.Ostmann.TreeLeafIndex