Dilation.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Finite multiplicative expansion of a dilation

This is the arithmetic content of manuscript Lemma lem:affine-dilation. The equality is asserted for positive arguments, the domain relevant to ordinary multiplicative functions. No complete multiplicativity is used.

def OAI.TwoPointCorrelations.dilate line 18
Source documentation
Extend f(m/a) by zero away from multiples of a.
```
noncomputable def dilate (a : ℕ) (f : ℕ → ℂ) (m : ℕ) : ℂ :=
…
```
def OAI.TwoPointCorrelations.dilationLocal line 21
def OAI.TwoPointCorrelations.dilationB line 24
def OAI.TwoPointCorrelations.dilationC line 27
def OAI.TwoPointCorrelations.dilationComponent line 30
theorem OAI.TwoPointCorrelations.dilationLocal_eq_sub line 33
theorem OAI.TwoPointCorrelations.dilate_eq_local_product line 43
theorem OAI.TwoPointCorrelations.dilate_eq_sum_components line 94
Source documentation
A fixed dilation is a finite signed sum of normalized ordinary multiplicative functions, even at arguments with nonunit residue classes.
```
theorem dilate_eq_sum_components (a : ℕ) (f : ℕ → ℂ)
    (ha : 0 < a) (hf : Multiplicative f) (h1 : f 1 = 1)
    {n : ℕ} (hn : 0 < n) :
    dilate a f n = ∑ E ∈ a.primeFactors.powerset,
      (-1 : ℂ) ^ E.card * dilationComponent a f E n := by
…
```
Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.dilate, OAI.TwoPointCorrelations.dilationComponent
theorem OAI.TwoPointCorrelations.dilationComponent_multiplicative line 107
theorem OAI.TwoPointCorrelations.dilationComponent_one line 111
theorem OAI.TwoPointCorrelations.dilationB_bound line 115
theorem OAI.TwoPointCorrelations.dilationComponent_oneBounded line 124
theorem OAI.TwoPointCorrelations.dilationComponent_nonpretentious line 132
theorem OAI.TwoPointCorrelations.dilationComponent_prime_pow line 143
Source documentation
Outside the dilation primes, the components keep the full prime-power sequence of the original function.
```
theorem dilationComponent_prime_pow (a : ℕ) (f : ℕ → ℂ) (E : Finset ℕ)
    (h1 : f 1 = 1) {p : ℕ} (hp : p.Prime) (hpA : p ∉ a.primeFactors) (k : ℕ) :
    dilationComponent a f E (p ^ k) = f (p ^ k) := by
…
```
Mentions: OAI.TwoPointCorrelations.dilationComponent