PretentiousDistance.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The pretentious distance used in ordinary two-point correlations

These definitions use the prime cutoff and the twist-height cutoff at the same integer scale. The finite-prime perturbation estimate below is Lemma lem:finite-prime-stability of Ordinary two-point correlations of multiplicative functions (24 September 2026). It is elementary and does not assume any analytic input.

def OAI.TwoPointCorrelations.primesUpTo line 23
Source documentation
The primes not exceeding an integer cutoff.
Also declared: ComparatorChallenges/OrdinaryTwoPointCorrelations.lean:24 (same declaration text), OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:23 (same declaration text).
```
def primesUpTo (N : ℕ) : Finset ℕ := (Finset.range (N + 1)).filter Nat.Prime
```
def OAI.TwoPointCorrelations.squaredDistance line 26
Source documentation
The square of the pretentious distance; the second sequence can be any twist.
Distinct definitions of this name: ComparatorChallenges/OrdinaryTwoPointCorrelations.lean:26 (different declaration text), OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:26 (same declaration text). Qualify references as OAI.TwoPointCorrelations.squaredDistance@path.
```
noncomputable def squaredDistance (f g : ℕ → ℂ) (N : ℕ) : ℝ :=
…
```
def OAI.TwoPointCorrelations.characterTwist line 30
Source documentation
The sequence χ(n) n^(it), with the value at zero immaterial to the prime sum.
Distinct definitions of this name: ComparatorChallenges/OrdinaryTwoPointCorrelations.lean:29 (different declaration text), OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:30 (same declaration text). Qualify references as OAI.TwoPointCorrelations.characterTwist@path.
```
noncomputable def characterTwist {q : ℕ} (χ : DirichletCharacter ℂ q)
    (t : ℝ) (n : ℕ) : ℂ :=
…
```
def OAI.TwoPointCorrelations.UniformlyNonpretentious line 40
Source documentation
Uniform nonpretentiousness against every fixed Dirichlet character.
The quantifier over all real lower bounds expresses divergence of the squared distance uniformly over |t| ≤ N. As the distance is nonnegative, this is exactly the divergence of the distance appearing in the manuscript.
Also declared: ComparatorChallenges/OrdinaryTwoPointCorrelations.lean:33 (same declaration text), OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:40 (same declaration text).
```
def UniformlyNonpretentious (f : ℕ → ℂ) : Prop :=
…
```
lemma OAI.TwoPointCorrelations.characterTwist_norm_le_one line 45
Also declared: OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:45 (same declaration text).
lemma OAI.TwoPointCorrelations.squaredDistance_nonneg line 50
Also declared: OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:50 (same declaration text).
lemma OAI.TwoPointCorrelations.squaredDistance_conj line 64
Also declared: OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:64 (same declaration text).
lemma OAI.TwoPointCorrelations.characterTwist_conj line 75
Source documentation
Conjugating a character and reversing the height conjugates its twist.
Also declared: OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:75 (same declaration text).
```
lemma characterTwist_conj {q : ℕ} (χ : DirichletCharacter ℂ q)
    (t : ℝ) (n : ℕ) :
    characterTwist (χ.ringHomComp (starRingEnd ℂ)) (-t) n =
      conj (characterTwist χ t n) := by
…
```
lemma OAI.TwoPointCorrelations.UniformlyNonpretentious.conj line 85
Source documentation
Uniform nonpretentiousness is invariant under complex conjugation.
Also declared: OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:85 (same declaration text).
```
lemma UniformlyNonpretentious.conj {f : ℕ → ℂ}
    (hf : UniformlyNonpretentious f) :
    UniformlyNonpretentious (fun n => conj (f n)) := by
…
```
Mentions: OAI.TwoPointCorrelations.UniformlyNonpretentious

lemma OAI.TwoPointCorrelations.squaredDistance_finite_prime_change line 102

Source documentation

Altering a fixed finite set of prime values changes the square of the pretentious distance by at most twice their reciprocal sum.

Also declared: OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:102 (same declaration text).

lemma squaredDistance_finite_prime_change (f b g : ℕ → ℂ) (N : ℕ)
    (P : Finset ℕ) (hf : ∀ n, 0 < n → ‖f n‖ ≤ 1) (hb : ∀ n, 0 < n → ‖b n‖ ≤ 1)
    (hg : ∀ n, 0 < n → ‖g n‖ ≤ 1)
    (heq : ∀ p, Nat.Prime p → p ∉ P → b p = f p) :
    |squaredDistance b g N - squaredDistance f g N| ≤
      2 * ∑ p ∈ P, (1 : ℝ) / (p : ℝ) := by
…

lemma OAI.TwoPointCorrelations.UniformlyNonpretentious.finite_prime_change line 161
Source documentation
The bound is uniform over the changing twist and finite modifications.
Also declared: OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:161 (same declaration text).
```
lemma UniformlyNonpretentious.finite_prime_change {f b : ℕ → ℂ}
    (hfnp : UniformlyNonpretentious f) (P : Finset ℕ)
    (hf : ∀ n, 0 < n → ‖f n‖ ≤ 1) (hb : ∀ n, 0 < n → ‖b n‖ ≤ 1)
    (heq : ∀ p, Nat.Prime p → p ∉ P → b p = f p) :
    UniformlyNonpretentious b := by
…
```
Mentions: OAI.TwoPointCorrelations.UniformlyNonpretentious

lemma OAI.TwoPointCorrelations.UniformlyNonpretentious.finite_family line 179

Source documentation

One lower bound works for every member of a fixed finite character family, and for every bounded sequence whose prime values are changed only in P. This is the uniformity needed when taking the short-interval theorem at a fixed auxiliary graph scale.

Also declared: OAI/NumberTheory/TwoPoint/PretentiousDistance.lean:179 (same declaration text).

lemma UniformlyNonpretentious.finite_family {ι : Type*} [Finite ι]
    {f : ℕ → ℂ} (hfnp : UniformlyNonpretentious f) (hf : ∀ n, 0 < n → ‖f n‖ ≤ 1)
    (P : Finset ℕ) (q : ι → ℕ) (hq : ∀ i, 0 < q i)
    (χ : ∀ i, DirichletCharacter ℂ (q i)) (K : ℝ) :
    ∀ᶠ N : ℕ in atTop, ∀ i (b : ℕ → ℂ),
      (∀ n, 0 < n → ‖b n‖ ≤ 1) →
      (∀ p, Nat.Prime p → p ∉ P → b p = f p) →
      ∀ t : ℝ, |t| ≤ (N : ℝ) → K ≤ squaredDistance b (characterTwist (χ i) t) N := by
…

Mentions: OAI.TwoPointCorrelations.UniformlyNonpretentious