A logarithmic cutoff for prime-power divisibility

noncomputable def NairTenenbaum.primePowerLogCutoff (N : ℝ) (p : ℕ) : ℕ

The exponent cutoff used to truncate the prime-power logarithmic expansion.

Equations

• NairTenenbaum.primePowerLogCutoff N p = ⌊Real.log N / Real.log ↑p⌋₊

theorem NairTenenbaum.factorization_le_primePowerLogCutoff {n p : ℕ} (hn : n ≠ 0) (hp : Nat.Prime p) {N : ℝ} (hsize : ↑n ≤ N) : n.factorization p ≤ primePowerLogCutoff N p

theorem NairTenenbaum.primePowerLogCutoff_mul_log_le {N : ℝ} (hN : 1 ≤ N) {p : ℕ} (hp : Nat.Prime p) : ↑(primePowerLogCutoff N p) * Real.log ↑p ≤ Real.log N

theorem NairTenenbaum.smoothLogRootError_le_prime_count (Q : Polynomial ℤ) {N K z : ℝ} (hN : 1 ≤ N) (hK : 0 ≤ K) (hroot : ∀ p ∈ Finset.filter Nat.Prime (Finset.range (⌊z⌋₊ + 1)), ∀ (ν : ℕ), 0 < ν → ↑(rootCount Q (p ^ ν)) ≤ K) : smoothLogRootError Q z (primePowerLogCutoff N) ≤ K * ↑(Finset.filter Nat.Prime (Finset.range (⌊z⌋₊ + 1))).card * Real.log N

theorem NairTenenbaum.polynomialSmoothLogMass_le_log_cutoff (Q : Polynomial ℤ) {x y z N : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) (hQ : ∀ n ∈ shortInterval x y, Polynomial.eval (↑n) Q ≠ 0) (hsize : ∀ n ∈ shortInterval x y, ↑(Polynomial.eval (↑n) Q).natAbs ≤ N) : polynomialSmoothLogMass Q x y z ≤ (y + 1) * smoothLogRootMain Q z (primePowerLogCutoff N) + smoothLogRootError Q z (primePowerLogCutoff N)

The exponent cutoff is supplied by a bound on the actual polynomial values; it is not an extra distributional hypothesis.