OAI/NumberTheory/Ostmann/QuadraticCenter/UniformPhaseGrid.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform harmonic control of an arbitrarily translated frequency grid

  1. theorem OAI.Ostmann.centered_grid_separation line 11
  2. theorem OAI.Ostmann.uniform_phase_grid_bound line 45

    Source documentation

    No Diophantine approximation of the offset α is required. A closest frequency costs N; all remaining frequencies cost the harmonic sum.

    theorem uniform_phase_grid_bound (q : ℕ) [NeZero q] (α : ℝ) (N : ℕ) :
    (∑ i : Fin q, ‖∑ n ∈ Finset.range N,
      realAdditivePhase (α + (i.val : ℝ) / q) ^ n‖) ≤
      2 * ((N : ℝ) + q * (1 + Real.log q)) := by
…

    Mentions: OAI.Ostmann.realAdditivePhase