Finite comparison by whole prime-power splitting

Expanding a product over prime divisors gives coprime complementary factors, so that the growth hypothesis is only used on coprime inputs. This is the finite combinatorial step of the corrected comparison argument.

noncomputable def NairTenenbaum.radicalProduct (l : ℕ → ℝ) (n : ℕ) : ℝ

Product of a prime weight over the distinct prime divisors.

Equations

• NairTenenbaum.radicalProduct l n = ∏ p ∈ n.primeFactors, l p

theorem NairTenenbaum.radicalProduct_nonneg {l : ℕ → ℝ} (hl : ∀ (p : ℕ), 0 ≤ l p) (n : ℕ) : 0 ≤ radicalProduct l n

@[simp]

theorem NairTenenbaum.radicalProduct_one (l : ℕ → ℝ) : radicalProduct l 1 = 1

theorem NairTenenbaum.radicalProduct_mul (l : ℕ → ℝ) {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) (hmn : m.Coprime n) : radicalProduct l (m * n) = radicalProduct l m * radicalProduct l n

def NairTenenbaum.unitaryPart (n : ℕ+) (s : Finset ℕ) : ℕ+

Scalar versions of the existing tuple prime-support splitting.

Equations

• NairTenenbaum.unitaryPart n s = NairTenenbaum.primeSelect (fun (x : Fin 1) => n) s 0

def NairTenenbaum.unitaryRest (n : ℕ+) (s : Finset ℕ) : ℕ+

The complementary whole-prime-power factor after a unitary selection.

Equations

• NairTenenbaum.unitaryRest n s = NairTenenbaum.primeReject (fun (x : Fin 1) => n) s 0

theorem NairTenenbaum.unitaryPart_mul_rest (n : ℕ+) (s : Finset ℕ) : unitaryPart n s * unitaryRest n s = n

theorem NairTenenbaum.unitaryPart_coprime_rest (n : ℕ+) (s : Finset ℕ) : (↑(unitaryPart n s)).Coprime ↑(unitaryRest n s)

theorem NairTenenbaum.unitaryPart_le (n : ℕ+) (s : Finset ℕ) : unitaryPart n s ≤ n

theorem NairTenenbaum.unitaryRest_le (n : ℕ+) (s : Finset ℕ) : unitaryRest n s ≤ n

theorem NairTenenbaum.unitaryPart_primeFactors (n : ℕ+) (s : Finset ℕ) : (↑(unitaryPart n s)).primeFactors = (↑n).primeFactors ∩ s

theorem NairTenenbaum.unitaryPart_support {n : ℕ+} {s : Finset ℕ} (hs : s ⊆ (↑n).primeFactors) : (↑(unitaryPart n s)).primeFactors = s

theorem NairTenenbaum.unitarySplit_injective {n m : ℕ+} {s t : Finset ℕ} (hs : s ⊆ (↑n).primeFactors) (ht : t ⊆ (↑m).primeFactors) (h : (unitaryPart n s, unitaryRest n s) = (unitaryPart m t, unitaryRest m t)) : n = m ∧ s = t

Both the original integer and its selected prime set are recovered from the resulting pair of factors.

theorem NairTenenbaum.unitary_comparison_pointwise {w U : ℕ+ → ℝ} {l : ℕ → ℝ} (hl : ∀ (p : ℕ), 0 ≤ l p) (hw : ∀ (a b : ℕ+), (↑a).Coprime ↑b → w (a * b) ≤ U a * w b) (n : ℕ+) : w n * radicalProduct (fun (p : ℕ) => 1 + l p) ↑n ≤ ∑ s ∈ (↑n).primeFactors.powerset, U (unitaryPart n s) * radicalProduct l ↑(unitaryPart n s) * w (unitaryRest n s)

The prime-product expansion, with the coprime growth inequality applied to every pair of complementary whole prime-power parts.

theorem NairTenenbaum.unitary_comparison_sum {w U : ℕ+ → ℝ} {l : ℕ → ℝ} (hw₀ : ∀ (n : ℕ+), 0 ≤ w n) (hU : ∀ (n : ℕ+), 0 ≤ U n) (hl : ∀ (p : ℕ), 0 ≤ l p) (hw : ∀ (a b : ℕ+), (↑a).Coprime ↑b → w (a * b) ≤ U a * w b) (N : ℕ+) : ∑ n ∈ Finset.Icc 1 N, w n * radicalProduct (fun (p : ℕ) => 1 + l p) ↑n ≤ (∑ a ∈ Finset.Icc 1 N, U a * radicalProduct l ↑a) * ∑ b ∈ Finset.Icc 1 N, w b

Uniform finite-sum comparison: a summable auxiliary convolution kernel can be supplied afterward without changing this combinatorial statement.