TailSpectatorFamily.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual spectator data used in the arithmetic comparisons

structure OAI.Ostmann.TailSpectatorFamily line 15
Source documentation
Every field refers to the same selected prime family and the original tail masks. The tolerance is available both for Fourier factors and for all translated nonprincipal characters.
```
structure TailSpectatorFamily (A : Set ℕ) (N k : ℕ) (L ε : ℝ)
    (cutoff : ℕ) (deleted : Finset ℕ) where
…
```
theorem OAI.Ostmann.EventuallyPrimeSumset.tail_spectator_family line 38
theorem OAI.Ostmann.TailSpectatorFamily.comparison_upper line 78

theorem OAI.Ostmann.eventual_tail_spectator_moduli line 86

Source documentation

The same selected spectators work for every bounded frequency array; the modulus and its coprimality are derived from the actual array.

theorem eventual_tail_spectator_moduli (n k : ℕ) (Aexp : ℝ) (hAexp : 0 ≤ Aexp) :
    ∀ᶠ L : ℝ in atTop, ∀ (A : Set ℕ) (N cutoff : ℕ) (ε : ℝ) (D : Finset ℕ)
      (F : TailSpectatorFamily A N k L ε cutoff D)
      (σ : Type) (T : Bool → MovingSlotData σ n) (bound : ℕ),
      (∀ b, (T b).Frequencies (· ≠ 0)) →
      (∀ b, (T b).Frequencies (fun s => s.natAbs ≤ bound)) →
      (bound : ℝ) ≤ Real.exp (Aexp * spectatorBulkCount k L) →
      let r := movingPairFrequencyModulus T
…

Mentions: OAI.Ostmann.TailSpectatorFamily, OAI.Ostmann.MovingSlotData, OAI.Ostmann.spectatorBulkCount, OAI.Ostmann.movingPairFrequencyModulus