OAI/NumberTheory/TwoPoint/Bounds/WindowPolynomialBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Concrete Parseval and short-sum bounds for the two window polynomials.

  1. lemma OAI.TwoPointCorrelations.integral_fourierPolynomial_sq_injective line 13
  2. lemma OAI.TwoPointCorrelations.integral_fourierPolynomial_sq_le_card line 27
  3. lemma OAI.TwoPointCorrelations.continuous_forwardWindowPolynomial line 42
  4. lemma OAI.TwoPointCorrelations.continuous_backwardWindowPolynomial line 45
  5. lemma OAI.TwoPointCorrelations.norm_forwardWindowPolynomial_le line 48
  6. lemma OAI.TwoPointCorrelations.norm_backwardWindowPolynomial_le line 59
  7. lemma OAI.TwoPointCorrelations.integral_forwardWindowPolynomial_sq_le line 70
  8. lemma OAI.TwoPointCorrelations.integral_backwardWindowPolynomial_sq_le line 85
  9. lemma OAI.TwoPointCorrelations.fourier_nat_at_real line 99
  10. lemma OAI.TwoPointCorrelations.forwardWindowPolynomial_at_real line 107
  11. def OAI.TwoPointCorrelations.progressionSequence line 115

    Source documentation

    Applying a progression mask to the original values preserves their unit bound.

    noncomputable def progressionSequence (f : ℕ → ℂ) (l : ℕ) [NeZero l]
    (a : ZMod l) (n : ℕ) : ℂ := if (n : ZMod l) = a then f n else 0
  12. lemma OAI.TwoPointCorrelations.OneBounded.progressionSequence line 118
  13. theorem OAI.TwoPointCorrelations.progression_window_sum_from_integral line 128

    Source documentation

    Every circle frequency is represented by a real frequency, and the unimodular origin phase disappears before applying MRT.

    theorem progression_window_sum_from_integral (f : ℕ → ℂ) (D Y l : ℕ)
    [NeZero l] (a : ZMod l) (K : ℝ)
    (hK : ∀ α, shortExponentialIntegral f (Y + 1) D α ≤ K)
    (θ : AddCircle (1 : ℝ)) :
    (∑ v ∈ range Y,
      ‖forwardWindowPolynomial (progressionSequence f l a) D (v + 1) θ‖) ≤ K := by
…

    Mentions: OAI.TwoPointCorrelations.shortExponentialIntegral, OAI.TwoPointCorrelations.forwardWindowPolynomial, OAI.TwoPointCorrelations.progressionSequence

  14. theorem OAI.TwoPointCorrelations.MRTLiouvilleShortInput.progression_window_polynomials line 145