Smooth moments and tails in the paper's weight notation

Exact reindexing of weighted-mass fibers identifies the smooth dagger-tuple bounds with bounds for the one-variable weight (16). No tuple is discarded, and no prime-support condition is weakened.

theorem NairTenenbaum.coordinate_dvd_weightedMass {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (n : Tuple r) (i : Fin r) : ↑(n i) ∣ weightedMass γ n

theorem NairTenenbaum.weightedMass_mem_factoredNumbers_iff {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (n : Tuple r) (s : Finset ℕ) : weightedMass γ n ∈ Nat.factoredNumbers s ↔ ∀ (i : Fin r), ↑(n i) ∈ Nat.factoredNumbers s

theorem NairTenenbaum.sum_weight_mul_eq_sum_weightUpTo {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (D : ℕ) (F : ArithmeticMap k) (θ : Fin r → ℕ → ℝ) (φ : ℕ+ → ℝ) (N : ℕ+) : ∑ m ∈ Finset.Icc 1 N, φ m * weight γ D F θ m = ∑ n ∈ weightUpTo γ D N, φ ⟨weightedMass γ n, ⋯⟩ * (pullback γ F n * ∏ i : Fin r, θ i ↑(n i) / ↑↑(n i))

A scalar multiplier may depend arbitrarily on the weighted mass.

theorem NairTenenbaum.sum_weight_filter_eq {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (D : ℕ) (F : ArithmeticMap k) (θ : Fin r → ℕ → ℝ) (P : ℕ+ → Prop) [DecidablePred P] (N : ℕ+) : ∑ m ∈ Finset.Icc 1 N with P m, weight γ D F θ m = ∑ n ∈ weightUpTo γ D N with P ⟨weightedMass γ n, ⋯⟩, pullback γ F n * ∏ i : Fin r, θ i ↑(n i) / ↑↑(n i)

Reindexing with an arbitrary scalar predicate on the weighted mass.

theorem NairTenenbaum.sum_smooth_weight_eq {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (D : ℕ) (F : ArithmeticMap k) (Q : Fin r → Polynomial ℤ) (s : Finset ℕ) (N : ℕ+) : ∑ m ∈ Finset.Icc 1 N with ↑m ∈ Nat.factoredNumbers s, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) m = ∑ n ∈ smoothWeightUpTo γ D s N, rootTupleWeight γ F Q n

The smooth restriction in the scalar weight is exactly coordinatewise smoothness on its dagger tuples.

theorem NairTenenbaum.sum_smooth_weight_tail_eq {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (D : ℕ) (F : ArithmeticMap k) (Q : Fin r → Polynomial ℤ) (s : Finset ℕ) (N : ℕ+) (x : ℝ) : ∑ m ∈ Finset.Icc 1 N with ↑m ∈ Nat.factoredNumbers s ∧ x < ↑↑m, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) m = ∑ n ∈ smoothWeightUpTo γ D s N with x < ↑(weightedMass γ n), rootTupleWeight γ F Q n

The same exact reindexing with a lower bound for the tail.

theorem NairTenenbaum.PolynomialSystem.weight_smooth_tail_bound {k r : ℕ} (P : PolynomialSystem k r) {A B ε κ z x : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hx : 0 < x) (hzκ : 4 ^ (↑P.total.natDegree * κ) ≤ z) (hεγ : ∀ (i : Fin r), ↑(totalExponent P.exponent i) * ε ≤ 1 / 8) (N : ℕ+) : ∑ m ∈ Finset.Icc 1 N with ↑m ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊) ∧ x < ↑↑m, P.weight F m ≤ Real.exp (-κ * Real.log x / Real.log z) * ((∏ i : Fin r, Real.exp (momentPrimeBound A B κ (7 / 8) (totalExponent P.exponent i) (max (P.R i).natDegree (P.badDiscriminant ^ 3)))) * ∑ m ∈ Finset.Icc 1 N with ↑m ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊), P.weight F m)

The root-weighted Rankin bound in the paper's one-variable notation. The smooth sum on the right still runs up to N; shrinking it to z is a separate step in Lemma 2.