LocalFactors.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Multiplicative functions from local prime-power factors

The finite local expansions in Part III of the manuscript replace values at primes dividing a fixed dilation. The resulting functions are ordinary multiplicative functions; complete multiplicativity is not required.

def OAI.TwoPointCorrelations.fromPrimePowers line 19
Source documentation
Multiply local factors over the positive exponents in the prime factorization.
Also declared: OAI/NumberTheory/TwoPointCorrelations/LocalFactors.lean:19 (same declaration text).
```
noncomputable def fromPrimePowers (F : ℕ → ℕ → ℂ) (n : ℕ) : ℂ :=
…
```
theorem OAI.TwoPointCorrelations.fromPrimePowers_one line 22
Also declared: OAI/NumberTheory/TwoPointCorrelations/LocalFactors.lean:22 (same declaration text).
theorem OAI.TwoPointCorrelations.fromPrimePowers_multiplicative line 27
Source documentation
Coprime arguments have disjoint prime support, so arbitrary prime-power values give an ordinary multiplicative function.
Also declared: OAI/NumberTheory/TwoPointCorrelations/LocalFactors.lean:27 (same declaration text).
```
theorem fromPrimePowers_multiplicative (F : ℕ → ℕ → ℂ) :
    Multiplicative (fromPrimePowers F) := by
…
```
Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.fromPrimePowers
theorem OAI.TwoPointCorrelations.fromPrimePowers_oneBounded line 35
Also declared: OAI/NumberTheory/TwoPointCorrelations/LocalFactors.lean:35 (same declaration text).
theorem OAI.TwoPointCorrelations.fromPrimePowers_prime line 49
Also declared: OAI/NumberTheory/TwoPointCorrelations/LocalFactors.lean:49 (same declaration text).
theorem OAI.TwoPointCorrelations.fromPrimePowers_eq_at_prime line 54
Source documentation
A change at finitely many prime-power sequences changes only those prime values.
Also declared: OAI/NumberTheory/TwoPointCorrelations/LocalFactors.lean:54 (same declaration text).
```
theorem fromPrimePowers_eq_at_prime (F G : ℕ → ℕ → ℂ) (P : Finset ℕ)
    (hFG : ∀ p, p ∉ P → F p 1 = G p 1) {p : ℕ} (hp : Nat.Prime p) (hpP : p ∉ P) :
    fromPrimePowers F p = fromPrimePowers G p := by
…
```
Mentions: OAI.TwoPointCorrelations.fromPrimePowers
theorem OAI.TwoPointCorrelations.fromPrimePowers_reconstruct line 62
Source documentation
The local construction recovers a normalized multiplicative function on positive integers, without replacing its prime-power values by powers.
Also declared: OAI/NumberTheory/TwoPointCorrelations/LocalFactors.lean:62 (same declaration text).
```
theorem fromPrimePowers_reconstruct (f : ℕ → ℂ) (hf : Multiplicative f)
    (h1 : f 1 = 1) {n : ℕ} (hn : 0 < n) :
    fromPrimePowers (fun p k => f (p ^ k)) n = f n := by
…
```
Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.fromPrimePowers