The finite averaging step in the Corvaja--Zannier Hasse--Weil argument

The Galois-closure argument produces finitely many twisted fixed-point error terms. Every twist has the same upper bound, while their sum is small. The elementary lemma below converts those facts into a two-sided bound for each individual twist.

theorem BGS.HasseWeil.abs_le_of_uniform_upper_and_abs_sum_le {ι : Type u_1} [Fintype ι] (E : ι → ℝ) (i : ι) (A B : ℝ) (hB : 0 ≤ B) (hupper : ∀ (j : ι), E j ≤ B) (hsum : |∑ j : ι, E j| ≤ A) : |E i| ≤ A + ↑(Fintype.card ι - 1) * B

If every term in a nonempty finite family is at most B and the total sum has absolute value at most A, then every term has a two-sided bound. This is the numerical core of the Galois-twist averaging step.

theorem BGS.HasseWeil.abs_twistError_le_geometric_of_uniform_upper_and_abs_sum_le {ι : Type u_1} [Fintype ι] (E : ℕ → ι → ℝ) (i : ι) (A B rho : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hrho : 1 ≤ rho) (hupper : ∀ (n : ℕ) (j : ι), E n j ≤ B * rho ^ n) (hsum : ∀ (n : ℕ), |∑ j : ι, E n j| ≤ A) (n : ℕ) : |E n i| ≤ (A + ↑(Fintype.card ι - 1) * B) * rho ^ n

Sequence form of Galois averaging. A uniform B * rho ^ n upper bound for all twists, together with a bounded total error, gives the same geometric growth rate as a two-sided bound for every twist.

theorem BGS.HasseWeil.twistError_isBigO_geometric_of_uniform_upper_and_abs_sum_le {ι : Type u_1} [Fintype ι] (E : ℕ → ι → ℝ) (i : ι) (A B rho : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hrho : 1 ≤ rho) (hupper : ∀ (n : ℕ) (j : ι), E n j ≤ B * rho ^ n) (hsum : ∀ (n : ℕ), |∑ j : ι, E n j| ≤ A) : (fun (n : ℕ) => E n i) =O[Filter.atTop] fun (n : ℕ) => rho ^ n

The finite averaging estimate gives the geometric O(rho ^ n) bound needed by the zeta-function power-sum argument.

theorem BGS.HasseWeil.abs_base_sub_center_le_of_average_and_pointwise {ι : Type u_1} [Fintype ι] [Nonempty ι] (x : ι → ℝ) (base center A B : ℝ) (_hA : 0 ≤ A) (_hB : 0 ≤ B) (haverage : |∑ i : ι, x i - ↑(Fintype.card ι) * base| ≤ A) (hpointwise : ∀ (i : ι), |x i - center| ≤ B) : |base - center| ≤ A + ↑(Fintype.card ι) * B

If a nonempty finite family is uniformly close to center and its sum is close to card · base, then base is close to center. The deliberately division-free bound is convenient for integral point counts and is uniform when the family cardinality is fixed.