AffineTransfer.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact progression and affine endpoint identities

These finite identities implement the endpoint step of §8 of the manuscript. They include nonunit residue classes and do not assume any cancellation theorem.

def OAI.TwoPointCorrelations.residuePrefix line 20
Source documentation
A prefix sum on any residue class, without a coprimality assumption.
```
def residuePrefix (u : ℕ → ℂ) (l b N : ℕ) : ℂ :=
…
```
lemma OAI.TwoPointCorrelations.progression_interval_image line 23
theorem OAI.TwoPointCorrelations.affine_sum_eq_residue_prefix line 49
Source documentation
Exact extraction of an affine subsequence from two progression prefixes.
```
theorem affine_sum_eq_residue_prefix (u : ℕ → ℂ) (l b N : ℕ) (hl : 0 < l) :
    (∑ n ∈ Finset.Icc 1 N, u (l * n + b)) =
      residuePrefix u l b (l * N + b) - residuePrefix u l b b := by
…
```
Mentions: OAI.TwoPointCorrelations.residuePrefix

theorem OAI.TwoPointCorrelations.liouville_affine_sum_endpoints line 67

Source documentation

The ordered Liouville affine sum has exactly the progression endpoints specified in the manuscript, with no condition on the residue class.

theorem liouville_affine_sum_endpoints (a₁ a₂ b₁ b₂ N : ℕ)
    (ha₁ : 0 < a₁) (ha₂ : 0 < a₂) (horder : a₂ * b₁ ≤ a₁ * b₂) :
    affineSum liouville liouville a₁ a₂ b₁ b₂ N =
      liouville (a₁ * a₂) *
        (residuePrefix (fun m => liouville m * liouville (m + (a₁ * b₂ - a₂ * b₁)))
            (a₁ * a₂) (a₂ * b₁) (a₁ * a₂ * N + a₂ * b₁) -
          residuePrefix (fun m => liouville m * liouville (m + (a₁ * b₂ - a₂ * b₁)))
            (a₁ * a₂) (a₂ * b₁) (a₂ * b₁)) := by
…

Mentions: OAI.TwoPointCorrelations.affineSum, OAI.TwoPointCorrelations.residuePrefix

theorem OAI.TwoPointCorrelations.affineSum_swap line 85
Source documentation
Swapping the two factors does not alter an affine correlation.
```
theorem affineSum_swap (f g : ℕ → ℂ) (a₁ a₂ b₁ b₂ N : ℕ) :
    affineSum f g a₁ a₂ b₁ b₂ N = affineSum g f a₂ a₁ b₂ b₁ N := by
…
```
Mentions: OAI.TwoPointCorrelations.affineSum
theorem OAI.TwoPointCorrelations.liouville_affine_sum_endpoints_all line 93
Source documentation
The exact endpoint formula with either determinant sign.
```
theorem liouville_affine_sum_endpoints_all (a₁ a₂ b₁ b₂ N : ℕ)
    (ha₁ : 0 < a₁) (ha₂ : 0 < a₂) :
    let l := a₁ * a₂
…
```

theorem OAI.TwoPointCorrelations.affine_mean_tendsto_zero line 111

Source documentation

Passage from a vanishing progression mean to its affine subsequence.

theorem affine_mean_tendsto_zero (u : ℕ → ℂ) (l b : ℕ) (hl : 0 < l)
    (hp : Filter.Tendsto (fun M : ℕ => residuePrefix u l b M / (M : ℂ))
      Filter.atTop (nhds 0)) :
    Filter.Tendsto (fun N : ℕ => (∑ n ∈ Finset.Icc 1 N, u (l * n + b)) / (N : ℂ))
      Filter.atTop (nhds 0) := by
…

Mentions: OAI.TwoPointCorrelations.residuePrefix