Coprime splitting by prime support

The decompositions used in Lemmas 1 and 2 and in (28)–(30) of the main proof. The same set of primes is used in every coordinate, so the two parts are coprime even across different coordinates. This property survives exponent substitution.

def NairTenenbaum.primeSelect {k : ℕ} (n : Tuple k) (s : Finset ℕ) : Tuple k

Retain the full prime-power parts at the primes in s.

Equations

• NairTenenbaum.primeSelect n s = ∏ p ∈ (NairTenenbaum.mass n).primeFactors with p ∈ s, NairTenenbaum.primePart n p

def NairTenenbaum.primeReject {k : ℕ} (n : Tuple k) (s : Finset ℕ) : Tuple k

Retain the full prime-power parts at the primes outside s.

Equations

• NairTenenbaum.primeReject n s = ∏ p ∈ (NairTenenbaum.mass n).primeFactors with p ∉ s, NairTenenbaum.primePart n p

theorem NairTenenbaum.primeSelect_mul_primeReject {k : ℕ} (n : Tuple k) (s : Finset ℕ) : primeSelect n s * primeReject n s = n

theorem NairTenenbaum.primeSelect_primeReject_coprime {k : ℕ} (n : Tuple k) (s : Finset ℕ) (i j : Fin k) : (↑(primeSelect n s i)).Coprime ↑(primeReject n s j)

Coprimality holds across all pairs of coordinates, not just matching ones.

theorem NairTenenbaum.factorization_prod_primePart {k : ℕ} (n : Tuple k) (T : Finset ℕ) (hT : ∀ q ∈ T, Nat.Prime q) (j : Fin k) (p : ℕ) : (↑((∏ q ∈ T, primePart n q) j)).factorization p = if p ∈ T then (↑(n j)).factorization p else 0

theorem NairTenenbaum.factorization_primeSelect {k : ℕ} (n : Tuple k) (s : Finset ℕ) (j : Fin k) (p : ℕ) : (↑(primeSelect n s j)).factorization p = if p ∈ s then (↑(n j)).factorization p else 0

theorem NairTenenbaum.factorization_primeReject {k : ℕ} (n : Tuple k) (s : Finset ℕ) (j : Fin k) (p : ℕ) : (↑(primeReject n s j)).factorization p = if p ∈ s then 0 else (↑(n j)).factorization p

theorem NairTenenbaum.primeFactors_primeSelect {k : ℕ} (n : Tuple k) (s : Finset ℕ) (j : Fin k) : (↑(primeSelect n s j)).primeFactors = (↑(n j)).primeFactors ∩ s

theorem NairTenenbaum.primeFactors_primeReject {k : ℕ} (n : Tuple k) (s : Finset ℕ) (j : Fin k) : (↑(primeReject n s j)).primeFactors = (↑(n j)).primeFactors \ s

theorem NairTenenbaum.Admissible.pullback_primeSplit_le {k r : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) (γ : Fin k → Fin r → ℕ) (n : Tuple r) (s : Finset ℕ) : pullback γ F n ≤ pullback γ F (primeSelect n s) * pullback γ (minimalMajorant F) (primeReject n s)

Equation (29) for a split at an arbitrary set of primes.

theorem NairTenenbaum.Admissible.pullback_minimalMajorant_le_growth {k r : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 0 ≤ B) (γ : Fin k → Fin r → ℕ) (n : Tuple r) : pullback γ (minimalMajorant F) n ≤ min (A ^ bigOmega (weightedMass γ n)) (B * ↑(weightedMass γ n) ^ ε)

Equation (30), stated for any positive input tuple.