Uniform coefficient bounds for the root/ideal convolution correction

theorem NairTenenbaum.idealNormArithmetic_prime_pow_exponential_bound (K : Type u_1) [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : |(idealNormArithmetic K) (p ^ k)| ≤ (2 ^ Module.finrank ℚ K) ^ k

theorem NairTenenbaum.idealNormInverse_prime_pow_exponential_bound (K : Type u_1) [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : |(idealNormInverse K) (p ^ k)| ≤ (2 * 2 ^ Module.finrank ℚ K) ^ k

theorem NairTenenbaum.squarefreeRootArithmetic_prime_pow_exponential_bound {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : |(squarefreeRootArithmetic Q) (p ^ k)| ≤ (↑Q.natDegree + 1) ^ k

noncomputable def NairTenenbaum.rootIdealCorrectionGrowthConstant (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) : ℝ

A uniform growth constant for the root/ideal correction coefficients.

Equations

• NairTenenbaum.rootIdealCorrectionGrowthConstant K Q = 2 * max (↑Q.natDegree + 1) (2 * 2 ^ Module.finrank ℚ K)

theorem NairTenenbaum.rootIdealCorrectionGrowthConstant_pos (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) : 0 < rootIdealCorrectionGrowthConstant K Q

theorem NairTenenbaum.rootIdealCorrection_prime_pow_exponential_bound (K : Type u_1) [Field K] [NumberField K] {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : |(rootIdealCorrection K Q) (p ^ k)| ≤ rootIdealCorrectionGrowthConstant K Q ^ k