OAI/NumberTheory/Ostmann/Preliminaries/DivisorPowerBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The elementary divisor bound needed for the frequency moduli

For every fixed power k, the kth power of the divisor count is bounded by a constant times n. The constant is independent of the modulus.

  1. theorem OAI.Ostmann.successor_le_two_pow line 17
  2. theorem OAI.Ostmann.exists_successor_power_bound line 24
  3. theorem OAI.Ostmann.prime_power_divisor_budget line 42
  4. theorem OAI.Ostmann.exists_divisors_power_bound line 56

    Source documentation

    A concrete power version of tau(n) = n^o(1), proved by separating the finitely many primes below 2^k in the factorization.

    theorem exists_divisors_power_bound (k : ℕ) :
    ∃ D : ℕ, 1 ≤ D ∧ ∀ n : ℕ, n ≠ 0 → n.divisors.card ^ k ≤ D * n := by
…