ResidueExpansion.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Residue classes as finite multiplicative expansions

The character identity in manuscript Lemma lem:affine-residue includes nonunit residue classes. Dividing by the gcd reduces to a unit class, so the standard character orthogonality relation applies even when the reduced modulus is one. Each resulting dilation has the finite expansion already proved in Dilation.

def OAI.TwoPointCorrelations.naturalCharacter line 25
Source documentation
A character evaluated on the natural numbers, with its usual zeros.
```
noncomputable def naturalCharacter {q : ℕ} (χ : DirichletCharacter ℂ q) (n : ℕ) : ℂ :=
…
```
lemma OAI.TwoPointCorrelations.naturalCharacter_multiplicative line 28
lemma OAI.TwoPointCorrelations.naturalCharacter_oneBounded line 33
lemma OAI.TwoPointCorrelations.naturalCharacter_one line 38

lemma OAI.TwoPointCorrelations.character_conj_unit line 42

Source documentation

The inverse-value form of conjugation on a unit residue.

lemma character_conj_unit {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q)
    {a : ZMod q} (ha : IsUnit a) : conj (χ a) = χ a⁻¹ := by
…

lemma OAI.TwoPointCorrelations.residue_character_orthogonality line 48
lemma OAI.TwoPointCorrelations.scaled_residue_iff line 65
lemma OAI.TwoPointCorrelations.dvd_of_scaled_residue line 71
theorem OAI.TwoPointCorrelations.residue_indicator_eq_character_dilations line 82
Source documentation
Gcd reduction followed by character orthogonality, valid also for b = 0 and for reduced modulus one. No assumption that the original class is a unit is present.
```
theorem residue_indicator_eq_character_dilations (l b n : ℕ) (hl : 0 < l) :
    (if n % l = b % l then (1 : ℂ) else 0) =
      ((l / b.gcd l).totient : ℂ)⁻¹ *
        ∑ χ : DirichletCharacter ℂ (l / b.gcd l),
          conj (naturalCharacter χ (b / b.gcd l)) *
            dilate (b.gcd l) (naturalCharacter χ) n := by
…
```
Mentions: OAI.TwoPointCorrelations.naturalCharacter, OAI.TwoPointCorrelations.dilate

theorem OAI.TwoPointCorrelations.residue_indicator_eq_components line 115

Source documentation

Every residue indicator is an explicit finite sum of bounded normalized multiplicative functions.

theorem residue_indicator_eq_components (l b n : ℕ) (hl : 0 < l) (hn : 0 < n) :
    (if n % l = b % l then (1 : ℂ) else 0) =
      ((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) *
              dilationComponent (b.gcd l) (naturalCharacter χ) E n := by
…

Mentions: OAI.TwoPointCorrelations.naturalCharacter, OAI.TwoPointCorrelations.dilationComponent

lemma OAI.TwoPointCorrelations.Multiplicative.mul line 133
lemma OAI.TwoPointCorrelations.OneBounded.mul line 140

def OAI.TwoPointCorrelations.residueComponent line 148

Source documentation

The multiplicative pieces of a function restricted to a residue class.

noncomputable def residueComponent {q : ℕ} (f : ℕ → ℂ) (d : ℕ)
    (χ : DirichletCharacter ℂ q) (E : Finset ℕ) (n : ℕ) : ℂ :=
…

lemma OAI.TwoPointCorrelations.residueComponent_multiplicative line 152
lemma OAI.TwoPointCorrelations.residueComponent_oneBounded line 157
lemma OAI.TwoPointCorrelations.residueComponent_nonpretentious line 166
Source documentation
Restriction to a nonunit progression modifies the character twist only at primes dividing the fixed gcd. Hence every multiplicative piece preserves the original uniformly nonpretentious factor.
```
lemma residueComponent_nonpretentious {q : ℕ} (f : ℕ → ℂ) (d : ℕ)
    (χ : DirichletCharacter ℂ q) (E : Finset ℕ) (hq : 0 < q)
    (hf : OneBounded f) (hfnp : UniformlyNonpretentious f) :
    UniformlyNonpretentious (residueComponent f d χ E) := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.UniformlyNonpretentious, OAI.TwoPointCorrelations.residueComponent

theorem OAI.TwoPointCorrelations.residue_weight_eq_components line 179

Source documentation

An explicit expansion after multiplication by the original first factor.

theorem residue_weight_eq_components (f : ℕ → ℂ) (l b n : ℕ)
    (hl : 0 < l) (hn : 0 < n) :
    (if n % l = b % l then f n else 0) =
      ((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) *
              residueComponent f (b.gcd l) χ E n := by
…

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