Smooth tails for general scalar admissible weights

This extends the root-vector smooth-tail bound to the scalar class M in Lemma 2. The proof lifts the weights into additional arithmetic coordinates, squares the weighted mass, and halves the decay parameter.

noncomputable def NairTenenbaum.generalSmoothTailBound {k r : ℕ} (A B T κ : ℝ) (γ : Fin k → Fin r → ℕ) (G : ℕ) : ℝ

Uniform constant in the smooth-tail estimate for a general admissible weight.

Equations

• NairTenenbaum.generalSmoothTailBound A B T κ γ G = NairTenenbaum.rootSmoothTailBound A (B * T ^ r) (κ / 2) (NairTenenbaum.liftedExponents γ) (fun (x : Fin r) => 1) (2 * G)

theorem NairTenenbaum.generalSmoothTailBound_pos {k r : ℕ} {A B T κ : ℝ} (hB : 0 ≤ B) (hT : 0 ≤ T) (γ : Fin k → Fin r → ℕ) (G : ℕ) : 0 < generalSmoothTailBound A B T κ γ G

theorem NairTenenbaum.general_weight_smooth_tail_finite {k r : ℕ} {A B T ε κ z x : ℝ} {F : ArithmeticMap k} {θ : Fin r → ℕ → ℝ} (hF : Admissible A B ε F) (hθ : ∀ (i : Fin r), Admissible A T ε fun (n : Tuple 1) => θ i ↑(n 0)) (hA : 1 ≤ A) (hB : 1 ≤ B) (hT : 1 ≤ T) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hx : 0 < x) (γ : 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) (hzκ : 4 ^ (↑G * κ) ≤ z) (D : ℕ) (N : ℕ+) : ∑ m ∈ Finset.Icc 1 N with ↑m ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊) ∧ x < ↑↑m, weight γ D F θ m ≤ generalSmoothTailBound A B T κ γ G * Real.exp (-κ * Real.log x / Real.log z) * ∑ m ∈ positiveUpTo z, weight γ D F θ m

Finite general-weight smooth tail, with the same cutoff and decay as in Lemma 2. Its slightly stronger growth bound is implied by Theorem 1's parameters.

theorem NairTenenbaum.general_weight_smooth_tail {k r : ℕ} {A B T ε κ z x : ℝ} {F : ArithmeticMap k} {θ : Fin r → ℕ → ℝ} (hF : Admissible A B ε F) (hθ : ∀ (i : Fin r), Admissible A T ε fun (n : Tuple 1) => θ i ↑(n 0)) (hA : 1 ≤ A) (hB : 1 ≤ B) (hT : 1 ≤ T) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hx : 0 < x) (γ : 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) (hzκ : 4 ^ (↑G * κ) ≤ z) (D : ℕ) : 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 ≤ generalSmoothTailBound A B T κ γ G * Real.exp (-κ * Real.log x / Real.log z) * ∑ m ∈ positiveUpTo z, weight γ D F θ m

The convergent infinite tail for arbitrary scalar admissible weights.