Growth of finite weighted power sums

This file formalizes the elementary power-sum lemma used in the Corvaja--Zannier passage from even-extension point-count estimates to bounds on Frobenius parameters.

For a finite set s of distinct complex numbers and nonzero weights, an O(ρ ^ n) bound on the weighted power sum forces every member of s to have norm at most ρ. The proof uses an isolation polynomial: applying a polynomial that vanishes at all the other members of s expresses the chosen geometric progression as a fixed linear combination of shifted power sums.

def BGS.HasseWeil.weightedPowerSum (s : Finset ℂ) (weight : ℂ → ℂ) (n : ℕ) : ℂ

The finite power sum with base set s and coefficient function weight.

Equations

• BGS.HasseWeil.weightedPowerSum s weight n = ∑ z ∈ s, weight z * z ^ n

theorem BGS.HasseWeil.norm_le_of_pow_isBigO {z : ℂ} {ρ : ℝ} (hρ : 0 ≤ ρ) (h : (fun (n : ℕ) => z ^ n) =O[Filter.atTop] fun (n : ℕ) => ρ ^ n) : ‖z‖ ≤ ρ

A single complex geometric progression can be O(ρ ^ n) only when its base has norm at most the nonnegative real number ρ.

theorem BGS.HasseWeil.norm_le_of_mem_of_weightedPowerSum_isBigO {s : Finset ℂ} {weight : ℂ → ℂ} {ρ : ℝ} (hρ : 0 ≤ ρ) (hweight : ∀ z ∈ s, weight z ≠ 0) (hO : weightedPowerSum s weight =O[Filter.atTop] fun (n : ℕ) => ρ ^ n) {z : ℂ} (hz : z ∈ s) : ‖z‖ ≤ ρ

If a finite weighted power sum is O(ρ ^ n) and every coefficient is nonzero, then each base occurring in the sum has norm at most ρ.

Distinctness is encoded by s being a Finset. No nonzero assumption on the bases is needed: zero bases satisfy the conclusion automatically.

theorem BGS.HasseWeil.weightedPowerSum_base_norm_le {s : Finset ℂ} {weight : ℂ → ℂ} {ρ : ℝ} (hρ : 0 ≤ ρ) (hweight : ∀ z ∈ s, weight z ≠ 0) (hO : weightedPowerSum s weight =O[Filter.atTop] fun (n : ℕ) => ρ ^ n) (z : ℂ) : z ∈ s → ‖z‖ ≤ ρ

Simultaneous form of norm_le_of_mem_of_weightedPowerSum_isBigO.