LocalExpansion.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite local expansions

The local sequences in manuscript Lemma lem:affine-dilation have value zero at exponent zero. A difference of two normalized local sequences represents such a sequence. Expansion over subsets then produces ordinary multiplicative components that retain the original prime values outside the fixed finite set.

def OAI.TwoPointCorrelations.localComponent line 22
Source documentation
A normalized multiplicative component with one of two local choices at each prime in P.
```
noncomputable def localComponent (f : ℕ → ℂ) (B C : ℕ → ℕ → ℂ)
    (P E : Finset ℕ) : ℕ → ℂ :=
…
```
theorem OAI.TwoPointCorrelations.localComponent_multiplicative line 26
theorem OAI.TwoPointCorrelations.localComponent_oneBounded line 30
theorem OAI.TwoPointCorrelations.localComponent_prime line 42

theorem OAI.TwoPointCorrelations.fromPrimePowers_split line 49

Source documentation

Expanding the support of a prime-power product is valid when the additional local factors have value one at exponent zero.

theorem fromPrimePowers_split (F : ℕ → ℕ → ℂ) (P : Finset ℕ)
    (hF : ∀ p, F p 0 = 1) (n : ℕ) :
    fromPrimePowers F n =
      (∏ p ∈ P, F p (n.factorization p)) *
        ∏ p ∈ n.primeFactors \ P, F p (n.factorization p) := by
…

Mentions: OAI.TwoPointCorrelations.fromPrimePowers

theorem OAI.TwoPointCorrelations.localComponent_split line 60

theorem OAI.TwoPointCorrelations.local_difference_expansion line 86

Source documentation

Exact finite expansion with one normalized multiplicative component for each subset of the exceptional primes.

theorem local_difference_expansion (f : ℕ → ℂ) (B C : ℕ → ℕ → ℂ)
    (P : Finset ℕ) (hf : f 1 = 1)
    (hB : ∀ p, B p 0 = 1) (hC : ∀ p, C p 0 = 1) (n : ℕ) :
    (∏ p ∈ P, (B p (n.factorization p) - C p (n.factorization p))) *
        (∏ p ∈ n.primeFactors \ P, f (p ^ n.factorization p)) =
      ∑ E ∈ P.powerset, (-1 : ℂ) ^ E.card * localComponent f B C P E n := by
…

Mentions: OAI.TwoPointCorrelations.localComponent

theorem OAI.TwoPointCorrelations.localComponent_nonpretentious line 100
Source documentation
Every bounded component inherits nonpretentiousness from the original factor. This uses only changes at the fixed finite prime set.
```
theorem localComponent_nonpretentious (f : ℕ → ℂ) (B C : ℕ → ℕ → ℂ)
    (P E : Finset ℕ) (hfnp : UniformlyNonpretentious f) (hf : OneBounded f)
    (hB : ∀ p k, p ∈ P → 0 < k → ‖B p k‖ ≤ 1)
    (hC : ∀ p k, p ∈ P → 0 < k → ‖C p k‖ ≤ 1) :
    UniformlyNonpretentious (localComponent f B C P E) := by
…
```
Mentions: OAI.TwoPointCorrelations.UniformlyNonpretentious, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.localComponent