OAI/NumberTheory/Ostmann/Arithmetic/BulkSpectatorPageBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.normalized_bulk_spectator_mean_le line 13

   Source documentation

   The numerical quartet estimate gives the local hypothesis of bulk_residue_page_bound, for the actual balanced residue transform.

   theorem normalized_bulk_spectator_mean_le {p : ℕ} [Fact p.Prime]
       (hp : 3 ≤ p) (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)))
       (S : Finset (ZMod p)) (hlo : (1 / 3 : ℝ) ≤ residueDensity S)
       (hhi : residueDensity S ≤ 2 / 3) (hS : S.Nonempty) (hSp : S.card < p)
       (β ε : ℝ) (hε : 0 ≤ ε) (hε1 : ε ≤ 1)
       (hprincipal : 3 / Real.sqrt (p : ℝ) ≤ ε) (hβ : 2 * β ≤ ε)
       (hbias : ∀ (χ : MulChar (ZMod p) ℂ), χ ≠ 1 → ∀ a : ZMod p,
         ‖(S.card : ℂ)⁻¹ * ∑ x ∈ S, χ⁻¹ (-a - x)‖ ≤ β)
       (d₁ d₂ : SpectatorDiagram p (n + 2)) (cL cR : TreeLeafIndex n → Bool)
   …

   Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.arrangementGraph, OAI.Ostmann.residueDensity, OAI.Ostmann.SpectatorDiagram