OAI/NumberTheory/JointDickman/Amplification/UniformPrefixGrid.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform prefix control from a finite mesh of counting endpoints

  1. lemma OAI.JointDickman.norm_prefix_interval_le line 11
  2. theorem OAI.JointDickman.prefix_grid_uniform_bound line 22

    Source documentation

    No positivity of the coefficients is needed: bounded increments and a finite mesh suffice for uniformity of their complex prefix sums.

    theorem prefix_grid_uniform_bound (f : ℕ → ℂ) {C d D : ℝ} (N : ℕ)
    (hC : 0 ≤ C) (hf : ∀ n, ‖f n‖ ≤ C) (hd : 0 < d)
    (hgrid : ∀ j ≤ N, ‖∑ n ∈ Ioc 0 ⌊(j : ℝ) * d⌋₊, f n‖ ≤ D)
    {u : ℝ} (hu : u ∈ Set.Icc 0 ((N : ℝ) * d)) :
    ‖∑ n ∈ Ioc 0 ⌊u⌋₊, f n‖ ≤ D + C * (d + 1) := by
…