OAI/NumberTheory/TwoPoint/AffineDeduction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.ProgressionCorrectedElliott line 12
2. theorem OAI.TwoPointCorrelations.Multiplicative.one_eq_zero_or_one line 20
3. theorem OAI.TwoPointCorrelations.Multiplicative.zero_of_one_eq_zero line 31
4. lemma OAI.TwoPointCorrelations.residuePrefix_congr line 35
5. lemma OAI.TwoPointCorrelations.residuePrefix_sum line 42
6. lemma OAI.TwoPointCorrelations.residuePrefix_const_mul line 51
7. theorem OAI.TwoPointCorrelations.finite_expansion_progression_zero line 60

   Source documentation

   Finite signed local expansions preserve an established progression limit.

   theorem finite_expansion_progression_zero {ι κ : Type*}
       (s : Finset ι) (t : Finset κ) (c : ι → ℂ) (d : κ → ℂ)
       (F : ι → ℕ → ℂ) (G : κ → ℕ → ℂ) (u v : ℕ → ℂ)
       (hu : ∀ n, 0 < n → u n = ∑ i ∈ s, c i * F i n)
       (hv : ∀ n, 0 < n → v n = ∑ j ∈ t, d j * G j n)
       (h l b : ℕ)
       (hz : ∀ i ∈ s, ∀ j ∈ t,
         Tendsto (fun N : ℕ => residuePrefix (fun n => F i n * G j (n + h)) l b N /
           (N : ℂ)) atTop (nhds 0)) :
       Tendsto (fun N : ℕ => residuePrefix (fun n => u n * v (n + h)) l b N /
         (N : ℂ)) atTop (nhds 0) := by
   …

   Mentions: OAI.TwoPointCorrelations.residuePrefix

8. theorem OAI.TwoPointCorrelations.ProgressionCorrectedElliott.dilations line 97
9. theorem OAI.TwoPointCorrelations.affine_ordered_zero line 121
10. theorem OAI.TwoPointCorrelations.ProgressionCorrectedElliott.affine line 153

    Source documentation

    The manuscript's affine reduction, conditional here on its internal progression theorem. This is not the published-input conditional main result.

    theorem ProgressionCorrectedElliott.affine (hprog : ProgressionCorrectedElliott) :
        AffineCorrectedElliott := by
    …

    Mentions: OAI.TwoPointCorrelations.ProgressionCorrectedElliott, OAI.TwoPointCorrelations.AffineCorrectedElliott