OAI/NumberTheory/Ostmann/Arithmetic/FrozenSpectatorNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingFieldGiantAmplitude_norm_le line 8
2. theorem OAI.Ostmann.frozenBulkSpectatorPair_norm_le line 29
3. theorem OAI.Ostmann.frozenBulkSpectatorHaar_norm_le line 45

   Source documentation

   The mixed Haar normalization has norm at most one, so the field bound survives without a factor depending on the spectator prime.

   theorem frozenBulkSpectatorHaar_norm_le {σ : Type*} {q : ℕ} [Fact q.Prime]
       (base : σ → ℕ) (n m : ℕ) (t : Bool → FrequencyTree ℤ n)
       (small : Bool → TreeLeafTuple (List σ) n) (samples : Bool → MovingSampleSlots σ n)
       (D : Bool → (ZMod q)ˣ) (e : Equiv.Perm (TreeLeafIndex n × Fin m))
       (g : ZMod q → ℂ) (K : ℝ) (hK : 0 ≤ K) (hg : ∀ x, ‖g x‖ ≤ K)
       (z : TreeLeafIndex n × Fin m → (ZMod q)ˣ) :
       ‖frozenBulkSpectatorHaar base n m t small samples D e g z‖ ≤ K ^ (2 ^ (n + 1)) := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.frozenBulkSpectatorHaar