Lemma 2: smooth tails with weights in the scalar class M #
The constant precedes the arithmetic function and both real cutoffs. The
statement keeps the paper's sum of factor multiplicities in 4^(γκ) and
covers the full range x > z > 4^(γκ), including z < 2.
theorem
NairTenenbaum.factored_eq_one_of_cutoff_lt_two
{n : ℕ}
{z : ℝ}
(hz : z < 2)
(hn : n ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊))
:
Below two, a smooth positive integer must be one.
theorem
NairTenenbaum.exists_classM_smooth_tail_bound
{k r : ℕ}
{A B ε κ : ℝ}
{θ : Fin r → ℕ → ℝ}
(hθ : ∀ (i : Fin r), ScalarClassM (θ i))
(hA : 1 ≤ A)
(hB : 1 ≤ B)
(hε : 0 < ε)
(hκ : 0 ≤ κ)
(γ : Fin k → Fin r → ℕ)
(hγ : ∀ (i : Fin r), 0 < totalExponent γ i)
(hγε : ∀ (i : Fin r), ↑(totalExponent γ i) * ε ≤ 1 / 16)
(G : ℕ)
(hG : ∀ (i : Fin r), totalExponent γ i ≤ G)
:
∃ (C : ℝ),
0 < C ∧ ∀ (F : ArithmeticMap k),
Admissible A B ε F →
∀ (D : ℕ) (x z : ℝ),
z < x →
4 ^ (↑G * κ) < z →
have f := fun (m : ℕ+) =>
if ↑m ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊) ∧ x < ↑↑m then weight γ D F θ m else 0;
Summable f ∧ ∑' (m : ℕ+), f m ≤ C * Real.exp (-κ * Real.log x / Real.log z) * ∑ m ∈ positiveUpTo z, weight γ D F θ m
A class-M family admits one constant for all admissible F, discriminants,
and cutoffs. The exponent condition is weaker than Theorem 1's hypotheses.
theorem
NairTenenbaum.lemmaTwo_exponent_bound
{g : ℕ}
(hg : 0 < g)
{ε δ : ℝ}
(hε : 0 < ε)
(hεg : ε < 1 / (8 * ↑g ^ 2))
(hδ : 0 < δ)
(hδ₁ : δ ≤ 1)
{a : ℕ}
(ha : a ≤ g)
:
The growth restriction used in the general tail estimate follows from the original parameters of Theorem 1, which are assumed throughout §4.
Lemma 2, equation (26), under the hypotheses stipulated at the start of §4. No multiplicativity is required of the scalar weights.
Equations
- One or more equations did not get rendered due to their size.