OAI/NumberTheory/Ostmann/Arithmetic/MovingSpectatorModulus.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A concrete modulus for arithmetic support and all spectator trees

  1. def OAI.Ostmann.movingSpectatorModulus line 11
  2. theorem OAI.Ostmann.movingSpectatorModulus_pos line 17
  3. theorem OAI.Ostmann.movingTopPeriod_dvd_spectatorModulus line 26
  4. theorem OAI.Ostmann.spectator_dvd_movingSpectatorModulus line 34
  5. theorem OAI.Ostmann.movingSpectatorModulus_bound line 46
  6. theorem OAI.Ostmann.small_spectator_product_bound line 63

    Source documentation

    This bound applies to a fixed finite set of distinct spectator primes using only their upper endpoint. No prime number theorem is required.

    theorem small_spectator_product_bound (S : Finset ℕ) (R : ℕ)
    (hS : ∀ q ∈ S, 0 < q ∧ q ≤ R) : ∏ q ∈ S, q ≤ R ^ R := by
…
  7. theorem OAI.Ostmann.small_spectator_product_exp line 80
  8. theorem OAI.Ostmann.movingSpectatorModulus_exp line 93