Smooth tails with the totient correction

The corrected comparison for tilted weights, followed by the root-weighted moment and truncation estimates, proves the version of the smooth tail needed for the sieve correction. The right side uses the unmodified root weight.

theorem NairTenenbaum.smooth_totient_moment_le {k r : ℕ} {A B ε κ σ z : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hσ : σ < 1) (hz : 2 ≤ z) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (hshift : ∀ (i : Fin r), ↑(totalExponent γ i) * (ε + κ / Real.log z) ≤ σ) (Q : Fin r → Polynomial ℤ) (C : Fin r → ℕ) (hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i) (g D : ℕ) (N : ℕ+) : ∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊z⌋₊) N, (rootTupleWeight γ F Q n * ∏ i : Fin r, totientTwist g ↑(n i)) * ↑(weightedMass γ n) ^ (κ / Real.log z) ≤ ((∏ i : Fin r, tiltedTotientBound B σ g (C i)) * ∏ i : Fin r, Real.exp (momentPrimeBound A B κ σ (totalExponent γ i) (C i))) * ∑ n ∈ smoothWeightUpTo γ D (Finset.Icc 0 ⌊z⌋₊) N, rootTupleWeight γ F Q n

The totient-modified moment is bounded by an untwisted smooth sum.

theorem NairTenenbaum.sum_smooth_totient_weight_tail_eq {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (D : ℕ) (F : ArithmeticMap k) (Q : Fin r → Polynomial ℤ) (g : ℕ) (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) * totientTwist g m) m = ∑ n ∈ smoothWeightUpTo γ D s N with x < ↑(weightedMass γ n), rootTupleWeight γ F Q n * ∏ i : Fin r, totientTwist g ↑(n i)

The scalar tail with the totient twist is exactly its dagger-tuple sum.

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

Uniform constant for the totient-modified smooth-tail estimate.

Equations

• NairTenenbaum.totientSmoothTailBound A B κ γ C G g = (∏ i : Fin r, NairTenenbaum.tiltedTotientBound B (7 / 8) g (C i)) * NairTenenbaum.rootSmoothTailBound A B κ γ C G

theorem NairTenenbaum.totient_weight_smooth_tail_finite {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) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (hγε : ∀ (i : Fin r), ↑(totalExponent γ i) * ε ≤ 1 / 8) (Q : Fin r → Polynomial ℤ) (C : Fin r → ℕ) (hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i) (G : ℕ) (hG : ∀ (i : Fin r), totalExponent γ i ≤ G) (hzκ : 4 ^ (↑G * κ) ≤ z) (g D : ℕ) (N : ℕ+) : ∑ m ∈ Finset.Icc 1 N with ↑m ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊) ∧ x < ↑↑m, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m) * totientTwist g m) m ≤ totientSmoothTailBound A B κ γ C G g * Real.exp (-κ * Real.log x / Real.log z) * ∑ m ∈ positiveUpTo z, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) m

Finite smooth tail with the sieve's totient correction, bounded by a truncated sum of the original root weight.

theorem NairTenenbaum.totient_weight_smooth_tail {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) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (hγε : ∀ (i : Fin r), ↑(totalExponent γ i) * ε ≤ 1 / 8) (Q : Fin r → Polynomial ℤ) (C : Fin r → ℕ) (hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i) (G : ℕ) (hG : ∀ (i : Fin r), totalExponent γ i ≤ G) (hzκ : 4 ^ (↑G * κ) ≤ z) (g D : ℕ) : have f := fun (m : ℕ+) => if ↑m ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊) ∧ x < ↑↑m then weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m) * totientTwist g m) m else 0; Summable f ∧ ∑' (m : ℕ+), f m ≤ totientSmoothTailBound A B κ γ C G g * Real.exp (-κ * Real.log x / Real.log z) * ∑ m ∈ positiveUpTo z, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) m

Infinite smooth tail for the totient-modified root vector. Convergence is proved from the uniform finite bound, and the right side is untwisted.

theorem NairTenenbaum.PolynomialSystem.totient_smooth_tail {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) (g : ℕ) : have f := fun (m : ℕ+) => if ↑m ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊z⌋₊) ∧ x < ↑↑m then NairTenenbaum.weight P.exponent P.discriminant F (fun (i : Fin r) (m : ℕ) => P.rootVector i m * totientTwist g m) m else 0; Summable f ∧ ∑' (m : ℕ+), f m ≤ totientSmoothTailBound A B κ P.exponent (fun (i : Fin r) => max (P.R i).natDegree (P.badDiscriminant ^ 3)) P.total.natDegree g * Real.exp (-κ * Real.log x / Real.log z) * ∑ m ∈ positiveUpTo z, P.weight F m

The totient-modified smooth tail needed by the main proof, for an actual polynomial system and with all root-count assumptions discharged.