RoughShiftBoundary.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The endpoint error in the rough-shift averaging argument

These are finite identities and bounds from the proof of (q:rough-shifts) in quantitative/03-analytic.tex. No short-sum or sieve estimate is assumed. The averages below use the positive integers 1,...,Y and translations 1,...,D; the resulting error is at most 2D/Y times the total weight.

def OAI.TwoPointCorrelations.positivePrefix line 20
Source documentation
A positive prefix, also when its length is zero.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughShiftBoundary.lean:20 (same declaration text).
```
def positivePrefix (u : ℕ → ℂ) (Y : ℕ) : ℂ :=
…
```
def OAI.TwoPointCorrelations.translatedPrefixAverage line 24
Source documentation
The average of the D translated positive prefixes.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughShiftBoundary.lean:24 (same declaration text).
```
noncomputable def translatedPrefixAverage (u : ℕ → ℂ) (Y D : ℕ) : ℂ :=
…
```
theorem OAI.TwoPointCorrelations.positivePrefix_translate_identity line 27
Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughShiftBoundary.lean:27 (same declaration text).
theorem OAI.TwoPointCorrelations.norm_positivePrefix_le line 43
Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughShiftBoundary.lean:43 (same declaration text).
theorem OAI.TwoPointCorrelations.norm_positivePrefix_translate_sub_le line 53
Source documentation
Translating by m loses at most m terms at each endpoint. No relation between the prefix length and the translation is needed.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughShiftBoundary.lean:53 (same declaration text).
```
theorem norm_positivePrefix_translate_sub_le (u : ℕ → ℂ) (Y m : ℕ) (B : ℝ)
    (hu : ∀ n, 0 < n → ‖u n‖ ≤ B) :
    ‖positivePrefix (fun n => u (n + m)) Y - positivePrefix u Y‖ ≤ 2 * m * B := by
…
```
Mentions: OAI.TwoPointCorrelations.positivePrefix
theorem OAI.TwoPointCorrelations.norm_translatedPrefixAverage_sub_le line 66
Source documentation
Averaging positive translations has the same finite endpoint bound.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughShiftBoundary.lean:66 (same declaration text).
```
theorem norm_translatedPrefixAverage_sub_le (u : ℕ → ℂ) (Y D : ℕ)
    (hD : 0 < D) (B : ℝ) (hB : 0 ≤ B)
    (hu : ∀ n, 0 < n → ‖u n‖ ≤ B) :
    ‖translatedPrefixAverage u Y D - positivePrefix u Y‖ ≤ 2 * D * B := by
…
```
Mentions: OAI.TwoPointCorrelations.translatedPrefixAverage, OAI.TwoPointCorrelations.positivePrefix
theorem OAI.TwoPointCorrelations.norm_normalized_translation_error line 96
Source documentation
The normalized endpoint error, in exactly the D/Y scale used in the rough-shift lemma.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughShiftBoundary.lean:96 (same declaration text).
```
theorem norm_normalized_translation_error (u : ℕ → ℂ) (Y D : ℕ)
    (hY : 0 < Y) (hD : 0 < D) (B : ℝ) (hB : 0 ≤ B)
    (hu : ∀ n, 0 < n → ‖u n‖ ≤ B) :
    ‖(translatedPrefixAverage u Y D - positivePrefix u Y) / (Y : ℂ)‖ ≤
      2 * (D : ℝ) / Y * B := by
…
```
Mentions: OAI.TwoPointCorrelations.translatedPrefixAverage, OAI.TwoPointCorrelations.positivePrefix
def OAI.TwoPointCorrelations.weightedShiftProfile line 108
Source documentation
The actual weighted progression-correlation profile.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughShiftBoundary.lean:108 (same declaration text).
```
def weightedShiftProfile {ι : Type*} (Z : Finset ι) (w : ι → ℂ) (shift : ι → ℕ)
    (f g : ℕ → ℂ) (l b n : ℕ) : ℂ :=
…
```
theorem OAI.TwoPointCorrelations.norm_weightedShiftProfile_le line 112
Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughShiftBoundary.lean:112 (same declaration text).
theorem OAI.TwoPointCorrelations.weighted_rough_shift_boundary line 127
Also declared: OAI/NumberTheory/TwoPoint/Bounds/RoughShiftBoundary.lean:127 (same declaration text).