Finite power sums detect the modulus of every root

This supplies the growth-to-root-modulus implication used on page 1 of Harcos, Weil's bound for Kloosterman sums (pages/harcos-weil-01.png). Cesàro averages isolate all copies of a maximal-modulus root simultaneously; their positive multiplicity prevents cancellation. No distinctness is needed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_cesaro_powers_tendsto_zero {z : ℂ} (hz : ‖z‖ ≤ 1) (hz1 : z ≠ 1) : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ k ∈ Finset.range n, z ^ k) Filter.atTop (nhds 0)

Away from 1, the Cesàro averages of powers in the closed unit disk tend to zero.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_cesaro_powers_tendsto {z : ℂ} (hz : ‖z‖ ≤ 1) : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ k ∈ Finset.range n, z ^ k) Filter.atTop (nhds (if z = 1 then 1 else 0))

Cesàro averaging retains precisely the copies of the root 1.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_norm_le_of_finset_power_sum_bound {ι : Type u_1} (s : Finset ι) (z : ι → ℂ) {R C : ℝ} (hR : 0 < R) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, ‖∑ i ∈ s, z i ^ n‖ ≤ C * R ^ n) (i : ι) : i ∈ s → ‖z i‖ ≤ R

A geometric bound on all sufficiently large power sums bounds every root. The indexing map may have repetitions: maximal equal roots contribute their positive integer multiplicity to a Cesàro limit, rather than canceling.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_norm_le_of_power_sum_growth {ι : Type u_1} [Fintype ι] (z : ι → ℂ) {R : ℝ} (hR : 0 < R) (hgrowth : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ‖∑ i : ι, z i ^ n‖ ≤ C * R ^ n) (i : ι) : ‖z i‖ ≤ R

Existential growth formulation for an arbitrary finite indexed family, with no injectivity or distinctness hypothesis.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_norm_le_of_power_sum_bound_from_four {ι : Type u_1} [Fintype ι] (z : ι → ℂ) {R C : ℝ} (hR : 0 < R) (hbound : ∀ (n : ℕ), 4 ≤ n → ‖∑ i : ι, z i ^ n‖ ≤ C * R ^ n) (i : ι) : ‖z i‖ ≤ R

The Harcos application only needs powers of degree at least four.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_pair_norm_le_of_power_sum_bound_from_four {ι : Type u_1} [Fintype ι] (α β : ι → ℂ) {R C : ℝ} (hR : 0 < R) (hbound : ∀ (n : ℕ), 4 ≤ n → ‖∑ i : ι, (α i ^ n + β i ^ n)‖ ≤ C * R ^ n) (i : ι) : ‖α i‖ ≤ R ∧ ‖β i‖ ≤ R

The paired-root form of Harcos's trace: no separation between the two families, or between roots within either family, is assumed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_pair_norm_eq_of_power_sum_bound_from_four {ι : Type u_1} [Fintype ι] (α β : ι → ℂ) {R C : ℝ} (hR : 0 < R) (hprod : ∀ (i : ι), α i * β i = ↑(R ^ 2)) (hbound : ∀ (n : ℕ), 4 ≤ n → ‖∑ i : ι, (α i ^ n + β i ^ n)‖ ≤ C * R ^ n) (i : ι) : ‖α i‖ = R ∧ ‖β i‖ = R

A reciprocal product upgrades the individual upper bounds to equality.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_two_mul_sub_one_roots_norm_le (p : ℕ) (z : Fin (2 * (p - 1)) → ℂ) {R C : ℝ} (hR : 0 < R) (hbound : ∀ (n : ℕ), 4 ≤ n → ‖∑ i : Fin (2 * (p - 1)), z i ^ n‖ ≤ C * R ^ n) (i : Fin (2 * (p - 1))) : ‖z i‖ ≤ R

Exactly 2 * (p - 1) indexed roots, retaining the n ≥ 4 hypothesis.