OAI/NumberTheory/TwoPoint/ShortIntervals/MRTQuadraticKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The elementary exponential smoothing remainder. Its monotonicity makes the error in a periodic-character convolution bounded independently of the smoothing scale.

  1. def OAI.TwoPointCorrelations.mrtQuadraticRemainder line 16
  2. lemma OAI.TwoPointCorrelations.mrt_quadratic_remainder_nonneg line 19
  3. lemma OAI.TwoPointCorrelations.mrt_quadratic_remainder_le_inv line 24
  4. lemma OAI.TwoPointCorrelations.mrt_quadratic_remainder_le_one line 29
  5. lemma OAI.TwoPointCorrelations.mrt_quadratic_exponential_square line 45
  6. lemma OAI.TwoPointCorrelations.mrt_quadratic_remainder_hasDeriv line 70
  7. lemma OAI.TwoPointCorrelations.mrt_quadratic_remainder_deriv_nonpos line 81
  8. lemma OAI.TwoPointCorrelations.mrt_quadratic_remainder_antitone line 88
  9. lemma OAI.TwoPointCorrelations.mrt_quadratic_remainder_tendsto line 96
  10. lemma OAI.TwoPointCorrelations.mrt_antitone_weighted_prefix line 104

    Source documentation

    Finite Dirichlet summation with a nonnegative decreasing weight.

    lemma mrt_antitone_weighted_prefix (a : ℕ → ℂ) (b : ℕ → ℝ) {Q : ℝ}
    (hQ : 0 ≤ Q) (hA : ∀ n, ‖∑ i ∈ range n, a i‖ ≤ Q)
    (hb : ∀ n, 0 ≤ b n) (hanti : Antitone b) (N : ℕ) :
    ‖∑ i ∈ range N, (b i : ℂ) * a i‖ ≤ Q * b 0 := by
…
  11. lemma OAI.TwoPointCorrelations.mrt_quadratic_remainder_weighted_prefix line 134