The prime-by-prime bound, equation (14)

def NairTenenbaum.primePart {k : ℕ} (n : Tuple k) (p : ℕ) : Tuple k

The tuple of p-parts of the coordinates; nonprimes give the unit tuple.

Equations

• NairTenenbaum.primePart n p j = if hp : Nat.Prime p then ⟨p, ⋯⟩ ^ (↑(n j)).factorization p else 1

theorem NairTenenbaum.primePart_coe {k : ℕ} (n : Tuple k) {p : ℕ} (hp : Nat.Prime p) (j : Fin k) : ↑(primePart n p j) = p ^ (↑(n j)).factorization p

theorem NairTenenbaum.coordinate_dvd_mass {k : ℕ} (n : Tuple k) (j : Fin k) : ↑(n j) ∣ mass n

theorem NairTenenbaum.prod_primePart {k : ℕ} (n : Tuple k) : ∏ p ∈ (mass n).primeFactors, primePart n p = n

theorem NairTenenbaum.primePart_coprime {k : ℕ} (n : Tuple k) {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (hpq : p ≠ q) : Coprime (primePart n p) (primePart n q)

theorem NairTenenbaum.mass_primePart {k : ℕ} (n : Tuple k) {p : ℕ} (hp : Nat.Prime p) : mass (primePart n p) = p ^ (mass n).factorization p

theorem NairTenenbaum.Admissible.minimalMajorant_prod_le {k : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) {ι : Type u_1} (s : Finset ι) (a : ι → Tuple k) (ha : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Coprime (a i) (a j)) : minimalMajorant F (∏ i ∈ s, a i) ≤ ∏ i ∈ s, minimalMajorant F (a i)

noncomputable def NairTenenbaum.primeMajorant (A B ε : ℝ) (N : ℕ) : ℝ

The right hand side of equation (14).

Equations

• NairTenenbaum.primeMajorant A B ε N = ∏ p ∈ N.primeFactors, min (A ^ N.factorization p) (B * ↑p ^ (↑(N.factorization p) * ε))

theorem NairTenenbaum.Admissible.minimalMajorant_le_primeMajorant {k : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) (n : Tuple k) : minimalMajorant F n ≤ primeMajorant A B ε (mass n)

Equation (14), with the full multivariable majorant.