OAI/NumberTheory/Ostmann/Arithmetic/MovingBulkPageBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulk_prime_density_norm line 12
2. theorem OAI.Ostmann.normalized_transfer_bulk_mean line 40

   Source documentation

   The conjugations proved for the original moving slot diagrams give the required quartet conjugations without any further combinatorial hypothesis.

   theorem normalized_transfer_bulk_mean {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))
   …

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