The multiplicative auxiliary functions of §2

The functions f_h immediately preceding equation (17). The local value at exponent zero is one, including for primes below the cutoff.

noncomputable def NairTenenbaum.auxiliaryLocal (A B ε : ℝ) (γ p ν : ℕ) : ℝ

The prescribed prime-power values of f_h, with γ = γ_h.

Equations

• NairTenenbaum.auxiliaryLocal A B ε γ p ν = if ν = 0 then 1 else if A ^ (1 / ε) < ↑p then A ^ (γ * ν) else B * ↑p ^ (↑(γ * ν) * ε)

noncomputable def NairTenenbaum.auxiliary (A B ε : ℝ) (γ n : ℕ) : ℝ

The multiplicative extension of the prescribed prime-power values.

Equations

• NairTenenbaum.auxiliary A B ε γ n = ∏ p ∈ n.primeFactors, NairTenenbaum.auxiliaryLocal A B ε γ p (n.factorization p)

@[simp]

theorem NairTenenbaum.auxiliaryLocal_zero (A B ε : ℝ) (γ p : ℕ) : auxiliaryLocal A B ε γ p 0 = 1

@[simp]

theorem NairTenenbaum.auxiliary_one (A B ε : ℝ) (γ : ℕ) : auxiliary A B ε γ 1 = 1

theorem NairTenenbaum.auxiliaryLocal_nonneg {A B ε : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (γ p ν : ℕ) : 0 ≤ auxiliaryLocal A B ε γ p ν

theorem NairTenenbaum.auxiliary_nonneg {A B ε : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (γ n : ℕ) : 0 ≤ auxiliary A B ε γ n

theorem NairTenenbaum.auxiliary_mul {A B ε : ℝ} (γ : ℕ) {m n : ℕ} (hmn : m.Coprime n) : auxiliary A B ε γ (m * n) = auxiliary A B ε γ m * auxiliary A B ε γ n

The extension is multiplicative on coprime arguments.

theorem NairTenenbaum.auxiliary_prime_pow (A B ε : ℝ) (γ : ℕ) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : auxiliary A B ε γ (p ^ ν) = auxiliaryLocal A B ε γ p ν

The multiplicative extension has precisely the prescribed prime-power values.

theorem NairTenenbaum.auxiliaryLocal_large {A B ε : ℝ} {p : ℕ} (hp : A ^ (1 / ε) < ↑p) (γ ν : ℕ) : auxiliaryLocal A B ε γ p ν = A ^ (γ * ν)

theorem NairTenenbaum.auxiliaryLocal_small {A B ε : ℝ} {p : ℕ} (hp : ¬A ^ (1 / ε) < ↑p) (γ ν : ℕ) : auxiliaryLocal A B ε γ p ν = (if ν = 0 then 1 else B) * (↑p ^ ε) ^ (γ * ν)

theorem NairTenenbaum.auxiliaryLocal_le_geometric {A B ε : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ p ν : ℕ) : auxiliaryLocal A B ε γ p ν ≤ B * min A (↑p ^ ε) ^ (γ * ν)

Geometric control of the local factors, as used in Lemmas 1 and 2.

theorem NairTenenbaum.local_min_le_prod_auxiliary {r : ℕ} {A B ε : ℝ} (hB : 1 ≤ B) (γ ν : Fin r → ℕ) (p : ℕ) : min (A ^ ∑ h : Fin r, γ h * ν h) (B * ↑p ^ (↑(∑ h : Fin r, γ h * ν h) * ε)) ≤ ∏ h : Fin r, auxiliaryLocal A B ε (γ h) p (ν h)

The local inequality used to deduce (17) from (14).

theorem NairTenenbaum.substitute_prod {k r : ℕ} (γ : Fin k → Fin r → ℕ) {ι : Type u_1} (s : Finset ι) (a : ι → Tuple r) : substitute γ (∏ i ∈ s, a i) = ∏ i ∈ s, substitute γ (a i)

Substitution commutes with a finite product.

theorem NairTenenbaum.substitute_primePart_coprime {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (hpq : p ≠ q) : Coprime (substitute γ (primePart n p)) (substitute γ (primePart n q))

Distinct prime parts remain coordinatewise coprime after substitution.

theorem NairTenenbaum.mass_substitute_primePart {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) {p : ℕ} (hp : Nat.Prime p) : mass (substitute γ (primePart n p)) = p ^ ∑ h : Fin r, totalExponent γ h * (↑(n h)).factorization p

theorem NairTenenbaum.auxiliary_eq_prod_mass {r : ℕ} (A B ε : ℝ) (γ : ℕ) (n : Tuple r) (h : Fin r) : auxiliary A B ε γ ↑(n h) = ∏ p ∈ (mass n).primeFactors, auxiliaryLocal A B ε γ p ((↑(n h)).factorization p)

Enlarging the prime support of an auxiliary function inserts only factors one.

theorem NairTenenbaum.Admissible.pullback_minimalMajorant_le_auxiliary {k r : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (γ : Fin k → Fin r → ℕ) (n : Tuple r) : pullback γ (minimalMajorant F) n ≤ ∏ h : Fin r, auxiliary A B ε (totalExponent γ h) ↑(n h)

Equation (17), without a coprimality restriction on the input tuple.