OAI/NumberTheory/Ostmann/Arithmetic/SampledSpectatorComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sampled_good_spectator_comparison line 14

   Source documentation

   The actual sampled small data produce fixed diagrams, the exact supported integer coefficient, and the good-matching decay for their uniform residues.

   theorem sampled_good_spectator_comparison {q : ℕ} [Fact q.Prime] (hq : 3 ≤ q)
       (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₁ t₂ : FrequencyTree ℤ (n + 2))
       (small₁ small₂ : TreeLeafTuple ℕ (n + 2))
       (samples₁ samples₂ : MovingGiantSamples (n + 2))
       (hfreq₁ : movingGiantFrequencyUnits q (n + 2) t₁)
       (hfreq₂ : movingGiantFrequencyUnits q (n + 2) t₂)
       (hsmall₁ : ((treeLeafProduct (n + 2) small₁ : ℕ) : ZMod q) ≠ 0)
       (hsmall₂ : ((treeLeafProduct (n + 2) small₂ : ℕ) : ZMod q) ≠ 0)
   …

   Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.arrangementGraph, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingGiantSamples, OAI.Ostmann.movingGiantFrequencyUnits, OAI.Ostmann.treeLeafProduct