Auxiliary series with a fractional denominator

The least common multiple of r coordinates is at least the r-th root of their product. Dividing each auxiliary by a small positive power therefore provides a separable majorant for the contribution of bad-prime valuations.

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

Auxiliary weight with a fractional-power denominator.

Equations

• NairTenenbaum.fractionalAuxiliary A B ε α γ n = NairTenenbaum.auxiliary A B ε γ n / ↑n ^ α

@[simp]

theorem NairTenenbaum.fractionalAuxiliary_one (A B ε α : ℝ) (γ : ℕ) : fractionalAuxiliary A B ε α γ 1 = 1

theorem NairTenenbaum.fractionalAuxiliary_nonneg {A B ε α : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (γ n : ℕ) : 0 ≤ fractionalAuxiliary A B ε α γ n

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

theorem NairTenenbaum.fractionalAuxiliary_prime_pow_le {A B ε α : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : ℕ) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : fractionalAuxiliary A B ε α γ (p ^ ν) ≤ B * (↑p ^ (↑γ * ε - α)) ^ ν

Prime-power values are bounded by a geometric series with exponent γ ε - α.

theorem NairTenenbaum.fractionalAuxiliary_prime_pow_le_uniform {A B ε α σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 0) (γ : ℕ) (hγ : ↑γ * ε - α ≤ σ) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : fractionalAuxiliary A B ε α γ (p ^ ν) ≤ B * (2 ^ σ) ^ ν

A fixed negative exponent gives a uniform ratio at every prime.

theorem NairTenenbaum.fractionalAuxiliary_prime_pow_summable {A B ε α σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 0) (γ : ℕ) (hγ : ↑γ * ε - α ≤ σ) {p : ℕ} (hp : Nat.Prime p) : Summable fun (ν : ℕ) => fractionalAuxiliary A B ε α γ (p ^ ν)

theorem NairTenenbaum.fractionalAuxiliary_local_tsum_le {A B ε α σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 0) (γ : ℕ) (hγ : ↑γ * ε - α ≤ σ) {p : ℕ} (hp : Nat.Prime p) : ∑' (ν : ℕ), fractionalAuxiliary A B ε α γ (p ^ ν) ≤ B / (1 - 2 ^ σ)

theorem NairTenenbaum.fractionalAuxiliary_smooth_hasSum {A B ε α σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 0) (γ : ℕ) (hγ : ↑γ * ε - α ≤ σ) (s : Finset ℕ) : HasSum (fun (n : ↑(Nat.factoredNumbers s)) => fractionalAuxiliary A B ε α γ ↑n) (∏ p ∈ s with Nat.Prime p, ∑' (ν : ℕ), fractionalAuxiliary A B ε α γ (p ^ ν))

theorem NairTenenbaum.fractionalAuxiliary_sum_le {A B ε α σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 0) (γ : ℕ) (hγ : ↑γ * ε - α ≤ σ) (s : Finset ℕ) (T : Finset ℕ+) (hT : ∀ n ∈ T, ↑n ∈ Nat.factoredNumbers s) : ∑ n ∈ T, fractionalAuxiliary A B ε α γ ↑n ≤ (B / (1 - 2 ^ σ)) ^ (Finset.filter Nat.Prime s).card

A coefficient-independent bound for every finite sum on fixed prime support.