ProgressionDeduction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

From binary cancellation to every progression and affine forms

The character expansion treats all residue classes, while finite-prime stability preserves nonpretentiousness of an original factor.

theorem OAI.TwoPointCorrelations.residuePrefix_eq_component_correlations line 20

Source documentation

The progression sum is a fixed finite linear combination of ordinary binary sums, with no coprimality condition on the residue class.

theorem residuePrefix_eq_component_correlations (f g : ℕ → ℂ) (h l b N : ℕ)
    (hl : 0 < l) :
    residuePrefix (fun n => f n * g (n + h)) l b N =
      ((l / b.gcd l).totient : ℂ)⁻¹ *
        ∑ χ : DirichletCharacter ℂ (l / b.gcd l),
          ∑ E ∈ (b.gcd l).primeFactors.powerset,
            (conj (naturalCharacter χ (b / b.gcd l)) * (-1 : ℂ) ^ E.card) *
              correlationSum (residueComponent f (b.gcd l) χ E) g 0 h N := by
…

Mentions: OAI.TwoPointCorrelations.residuePrefix, OAI.TwoPointCorrelations.naturalCharacter, OAI.TwoPointCorrelations.correlationSum, OAI.TwoPointCorrelations.residueComponent

theorem OAI.TwoPointCorrelations.BinaryCorrectedElliott.progression line 68
Source documentation
Every-residue progression cancellation follows from the binary corrected Elliott statement by finite character expansion.
```
theorem BinaryCorrectedElliott.progression (hbinary : BinaryCorrectedElliott) :
    ProgressionCorrectedElliott := by
…
```
Mentions: OAI.TwoPointCorrelations.BinaryCorrectedElliott, OAI.TwoPointCorrelations.ProgressionCorrectedElliott
theorem OAI.TwoPointCorrelations.BinaryCorrectedElliott.affine line 100
Source documentation
The complete qualitative affine reduction, including nonunit slopes and either original nonpretentious factor, assuming binary cancellation.
```
theorem BinaryCorrectedElliott.affine (hbinary : BinaryCorrectedElliott) :
    AffineCorrectedElliott := hbinary.progression.affine
…
```
Mentions: OAI.TwoPointCorrelations.BinaryCorrectedElliott, OAI.TwoPointCorrelations.AffineCorrectedElliott