CharacterTwists.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Dirichlet character twists preserve uniform nonpretentiousness

Characters with different moduli are multiplied after changing both levels to the product modulus. The resulting character equals the pointwise product on every natural number, including the nonunit classes. This gives an exact identity of pretentious distances and preserves the original height cutoff.

def OAI.TwoPointCorrelations.productCharacters line 21

Source documentation

Product of two characters, viewed at their common product modulus.

noncomputable def productCharacters {q r : ℕ} (χ : DirichletCharacter ℂ q)
    (ψ : DirichletCharacter ℂ r) : DirichletCharacter ℂ (q * r) :=
…

def OAI.TwoPointCorrelations.conjugateCharacter line 26
Source documentation
Conjugation of the values of a Dirichlet character.
```
def conjugateCharacter {q : ℕ} (χ : DirichletCharacter ℂ q) : DirichletCharacter ℂ q :=
…
```
lemma OAI.TwoPointCorrelations.conjugateCharacter_apply line 29
lemma OAI.TwoPointCorrelations.productCharacters_apply_nat line 34
Source documentation
Changing both character levels to their product preserves their pointwise product, even when the argument is not a unit modulo the product.
```
lemma productCharacters_apply_nat {q r : ℕ} (χ : DirichletCharacter ℂ q)
    (ψ : DirichletCharacter ℂ r) (n : ℕ) :
    productCharacters χ ψ (n : ZMod (q * r)) = χ (n : ZMod q) * ψ (n : ZMod r) := by
…
```
Mentions: OAI.TwoPointCorrelations.productCharacters

def OAI.TwoPointCorrelations.twistByCharacter line 60

Source documentation

Multiplication by a fixed Dirichlet character.

noncomputable def twistByCharacter {q : ℕ} (f : ℕ → ℂ)
    (χ : DirichletCharacter ℂ q) (n : ℕ) : ℂ := f n * χ (n : ZMod q)

lemma OAI.TwoPointCorrelations.characterTwist_productCharacters line 63

lemma OAI.TwoPointCorrelations.squaredDistance_twistByCharacter line 73

Source documentation

The same real twist height appears on both sides, including at primes dividing either character modulus.

lemma squaredDistance_twistByCharacter {q r : ℕ} (f : ℕ → ℂ)
    (ψ : DirichletCharacter ℂ r) (χ : DirichletCharacter ℂ q) (t : ℝ) (N : ℕ) :
    squaredDistance (TwoPointCorrelations.twistByCharacter f ψ) (characterTwist χ t) N =
      squaredDistance f (characterTwist (productCharacters χ (conjugateCharacter ψ)) t) N := by
…

Mentions: OAI.TwoPointCorrelations.twistByCharacter, OAI.TwoPointCorrelations.productCharacters, OAI.TwoPointCorrelations.conjugateCharacter

lemma OAI.TwoPointCorrelations.UniformlyNonpretentious.twistByCharacter line 86
lemma OAI.TwoPointCorrelations.OneBounded.twistByCharacter line 96
lemma OAI.TwoPointCorrelations.Multiplicative.twistByCharacter line 104