ShortSumSampling.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Sampling the published short-interval estimate

For integral short lengths, a moving short sum is constant on each unit cell of its origin. Thus its published integral controls the actual finite sum of integer origins, with outer cutoff Y+1. The progression restriction is an average of fixed frequencies and has total coefficient mass one.

lemma OAI.TwoPointCorrelations.shortExponentialSum_on_unit_cell line 19
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:19 (same declaration text).
lemma OAI.TwoPointCorrelations.shortExponentialSum_unit_integrable line 28
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:28 (same declaration text).
lemma OAI.TwoPointCorrelations.integral_shortExponentialSum_unit line 37
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:37 (same declaration text).
theorem OAI.TwoPointCorrelations.shortExponentialIntegral_eq_sum line 48
Source documentation
Exact unit-cell decomposition, with no endpoint error.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:48 (same declaration text).
```
theorem shortExponentialIntegral_eq_sum (b : ℕ → ℂ) (X D : ℕ) (α : ℝ) :
    shortExponentialIntegral b X D α =
      ∑ v ∈ range X, ‖shortExponentialSum b D α v‖ := by
…
```
Mentions: OAI.TwoPointCorrelations.shortExponentialIntegral, OAI.TwoPointCorrelations.shortExponentialSum
theorem OAI.TwoPointCorrelations.sum_positive_shortExponentialSum_le line 69
Source documentation
The positive integer origins used in the manuscript occupy all but the first unit cell of the published integral.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:69 (same declaration text).
```
theorem sum_positive_shortExponentialSum_le (b : ℕ → ℂ) (Y D : ℕ) (α : ℝ) :
    (∑ v ∈ range Y, ‖shortExponentialSum b D α (v + 1 : ℕ)‖) ≤
      shortExponentialIntegral b (Y + 1) D α := by
…
```
Mentions: OAI.TwoPointCorrelations.shortExponentialSum, OAI.TwoPointCorrelations.shortExponentialIntegral
lemma OAI.TwoPointCorrelations.sum_Icc_shift line 75
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:75 (same declaration text).
lemma OAI.TwoPointCorrelations.shortExponentialSum_at_nat line 94
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:94 (same declaration text).
lemma OAI.TwoPointCorrelations.additiveCharacter_nat_add line 100
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:100 (same declaration text).
lemma OAI.TwoPointCorrelations.norm_additiveCharacter line 108
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:108 (same declaration text).
def OAI.TwoPointCorrelations.shortWindowSum line 112
Source documentation
The short Fourier polynomial indexed by increments 1,...,D.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:112 (same declaration text).
```
noncomputable def shortWindowSum (b : ℕ → ℂ) (D : ℕ) (α : ℝ) (v : ℕ) : ℂ :=
…
```
lemma OAI.TwoPointCorrelations.shortExponentialSum_eq_window line 115
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:115 (same declaration text).
lemma OAI.TwoPointCorrelations.norm_shortExponentialSum_eq_window line 125
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:125 (same declaration text).
theorem OAI.TwoPointCorrelations.progression_short_sum_from_integral line 131
Source documentation
A uniform fixed-frequency integral bound controls every progression class of actual discrete windows, including nonunit classes.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:131 (same declaration text).
```
theorem progression_short_sum_from_integral (b : ℕ → ℂ) (D Y l : ℕ)
    [NeZero l] (a : ZMod l) (α K : ℝ)
    (hK : ∀ β : ℝ, shortExponentialIntegral b (Y + 1) D β ≤ K) :
    (∑ v ∈ range Y, ‖∑ n ∈ Icc (v + 2) (v + 1 + D),
      if (n : ZMod l) = a then b n * additiveCharacter α n else 0‖) ≤ K := by
…
```
Mentions: OAI.TwoPointCorrelations.shortExponentialIntegral, OAI.TwoPointCorrelations.additiveCharacter

theorem OAI.TwoPointCorrelations.MRTLiouvilleShortInput.progression_integer_windows line 160

Source documentation

Published MRT Theorem 1.3 applied to the actual progression windows.

Also declared: OAI/NumberTheory/TwoPoint/Bounds/ShortSumSampling.lean:160 (same declaration text).

theorem MRTLiouvilleShortInput.progression_integer_windows
    (hMRT : MRTLiouvilleShortInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ (Y D l : ℕ), 10 ≤ D → D ≤ Y + 1 →
      ∀ [NeZero l] (a : ZMod l) (α : ℝ),
        (∑ v ∈ range Y, ‖∑ n ∈ Icc (v + 2) (v + 1 + D),
          if (n : ZMod l) = a then liouville n * additiveCharacter α n else 0‖) ≤
          C * (D : ℝ) * (Y + 1 : ℕ) * mrtShortError (Y + 1) D := by
…

Mentions: OAI.TwoPointCorrelations.MRTLiouvilleShortInput, OAI.TwoPointCorrelations.additiveCharacter, OAI.TwoPointCorrelations.mrtShortError