OAI/NumberTheory/Ostmann/QuadraticCenter/RealQuadraticPhase.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Real quadratic phases and their linear correlations

These are the concrete exponential sums used in the inverse quadratic step.

  1. def OAI.Ostmann.realAdditivePhase line 16
  2. theorem OAI.Ostmann.realAdditivePhase_zero line 19
  3. theorem OAI.Ostmann.norm_realAdditivePhase line 22
  4. theorem OAI.Ostmann.realAdditivePhase_add line 25
  5. theorem OAI.Ostmann.realAdditivePhase_nat_mul line 33
  6. theorem OAI.Ostmann.conj_realAdditivePhase line 41
  7. theorem OAI.Ostmann.realAdditivePhase_sub line 50
  8. def OAI.Ostmann.realQuadraticPhase line 54
  9. theorem OAI.Ostmann.realQuadraticPhase_correlation line 57
  10. theorem OAI.Ostmann.norm_quadratic_correlation_sum line 67
  11. theorem OAI.Ostmann.norm_geometric_sum_le line 75

    Source documentation

    The elementary geometric-sum bound, retaining the exact denominator.

    theorem norm_geometric_sum_le (z : ℂ) (N : ℕ) (hz : ‖z‖ = 1) (hz1 : z ≠ 1) :
    ‖∑ j ∈ Finset.range N, z ^ j‖ ≤ min (N : ℝ) (2 / ‖z - 1‖) := by
…