OAI/NumberTheory/Ostmann/Quadratic/QuadraticDifferencing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

One differencing step for the actual quadratic exponential sum

  1. theorem OAI.Ostmann.real_part_sum line 12
  2. theorem OAI.Ostmann.norm_add_sq_real line 19
  3. theorem OAI.Ostmann.sum_norm_sq_triangle line 25
  4. theorem OAI.Ostmann.triangle_sum_by_gap line 39
  5. theorem OAI.Ostmann.quadratic_differencing_bound line 78

    Source documentation

    The linear coefficient disappears after taking absolute values of the shift correlations. No rational-approximation estimate is assumed here.

    theorem quadratic_differencing_bound (α β : ℝ) (N : ℕ) :
    ‖∑ j ∈ Finset.range N, realQuadraticPhase α β j‖ ^ 2 ≤
      (N : ℝ) + 2 * ∑ h ∈ Finset.range N,
        ‖∑ j ∈ Finset.range (N - (h + 1)), realAdditivePhase (2 * α * (h + 1)) ^ j‖ := by
…

    Mentions: OAI.Ostmann.realQuadraticPhase, OAI.Ostmann.realAdditivePhase