Basic.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Ordinary two-point correlations: concrete sums and affine transfer

Definitions follow the introduction of the supplied manuscript Ordinary two-point correlations of multiplicative functions (September 24, 2026). The exact Liouville identities below are the algebraic part of §8. No cancellation estimate is assumed or asserted here.

def OAI.TwoPointCorrelations.liouville line 22
Source documentation
The standard Liouville function, viewed as complex valued. Its value at zero is zero, as in mathlib; only positive arguments occur in the main statements.
Distinct definitions of this name: ComparatorChallenges/OrdinaryTwoPointCorrelations.lean:11 (different declaration text), OAI/NumberTheory/TwoPoint/Basic.lean:22 (same declaration text). Qualify references as OAI.TwoPointCorrelations.liouville@path.
```
noncomputable def liouville (n : ℕ) : ℂ := ArithmeticFunction.liouville n
```
def OAI.TwoPointCorrelations.correlationSum line 25
Source documentation
An ordinary sum, with weight one on each positive integer at most N.
Also declared: ComparatorChallenges/OrdinaryTwoPointCorrelations.lean:13 (same declaration text), OAI/NumberTheory/TwoPoint/Basic.lean:25 (same declaration text).
```
def correlationSum (f g : ℕ → ℂ) (h₁ h₂ N : ℕ) : ℂ :=
…
```
def OAI.TwoPointCorrelations.affineSum line 29
Source documentation
The ordinary affine correlation, allowing nonunit coefficients.
Also declared: ComparatorChallenges/OrdinaryTwoPointCorrelations.lean:16 (same declaration text), OAI/NumberTheory/TwoPoint/Basic.lean:29 (same declaration text).
```
def affineSum (f g : ℕ → ℂ) (a₁ a₂ b₁ b₂ N : ℕ) : ℂ :=
…
```
def OAI.TwoPointCorrelations.progressionSum line 33
Source documentation
The progression sum includes every residue class, including zero.
Also declared: OAI/NumberTheory/TwoPoint/Basic.lean:33 (same declaration text).
```
def progressionSum (f g : ℕ → ℂ) (h l b N : ℕ) : ℂ :=
…
```
def OAI.TwoPointCorrelations.Multiplicative line 38
Source documentation
Ordinary multiplicativity is required only for coprime positive arguments; this also permits the identically zero function, as does the manuscript.
Also declared: ComparatorChallenges/OrdinaryTwoPointCorrelations.lean:19 (same declaration text), OAI/NumberTheory/TwoPoint/Basic.lean:38 (same declaration text).
```
def Multiplicative (f : ℕ → ℂ) : Prop :=
…
```
def OAI.TwoPointCorrelations.OneBounded line 41
Also declared: ComparatorChallenges/OrdinaryTwoPointCorrelations.lean:22 (same declaration text), OAI/NumberTheory/TwoPoint/Basic.lean:41 (same declaration text).
theorem OAI.TwoPointCorrelations.liouville_mul line 43
Also declared: OAI/NumberTheory/TwoPoint/Basic.lean:43 (same declaration text).
theorem OAI.TwoPointCorrelations.liouville_sq line 47
Also declared: OAI/NumberTheory/TwoPoint/Basic.lean:47 (same declaration text).

theorem OAI.TwoPointCorrelations.liouville_affine_dilation line 56

Source documentation

Multiplying the two affine arguments by the opposite slopes gives an exact identity. There is no coprimality restriction on any coefficient.

Also declared: OAI/NumberTheory/TwoPoint/Basic.lean:56 (same declaration text).

theorem liouville_affine_dilation (a₁ a₂ b₁ b₂ n : ℕ)
    (ha₁ : a₁ ≠ 0) (ha₂ : a₂ ≠ 0) :
    liouville (a₁ * n + b₁) * liouville (a₂ * n + b₂) =
      liouville (a₁ * a₂) * liouville (a₂ * (a₁ * n + b₁)) *
        liouville (a₁ * (a₂ * n + b₂)) := by
…

theorem OAI.TwoPointCorrelations.liouville_affine_ordered line 69

Source documentation

The orientation with a₂ b₁ ≤ a₁ b₂; the opposite orientation is obtained by swapping the two factors. This is manuscript equation (q:quant-affine-identity).

Also declared: OAI/NumberTheory/TwoPoint/Basic.lean:69 (same declaration text).

theorem liouville_affine_ordered (a₁ a₂ b₁ b₂ n : ℕ)
    (ha₁ : a₁ ≠ 0) (ha₂ : a₂ ≠ 0) (horder : a₂ * b₁ ≤ a₁ * b₂) :
    liouville (a₁ * n + b₁) * liouville (a₂ * n + b₂) =
      liouville (a₁ * a₂) * liouville (a₁ * a₂ * n + a₂ * b₁) *
        liouville (a₁ * a₂ * n + a₂ * b₁ + (a₁ * b₂ - a₂ * b₁)) := by
…

theorem OAI.TwoPointCorrelations.liouville_multiplicative line 81
Also declared: OAI/NumberTheory/TwoPoint/Basic.lean:81 (same declaration text).
theorem OAI.TwoPointCorrelations.liouville_oneBounded line 85
Also declared: OAI/NumberTheory/TwoPoint/Basic.lean:85 (same declaration text).