Reindexing logarithmic sums on squarefree integers

An integer with a selected prime divisor is equivalently a prime and a positive cofactor. Nonnegativity and squarefree support justify the infinite reindexing from a convergent logarithmically weighted series.

def NairTenenbaum.primeFactorCofactorEquiv : (n : ℕ) × ↥n.primeFactors ≃ Nat.Primes × ℕ+

The equivalence splitting an integer into its selected prime factor and cofactor.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.log_eq_sum_primeFactors_of_squarefree {n : ℕ} (hn : Squarefree n) : Real.log ↑n = ∑ p ∈ n.primeFactors, Real.log ↑p

theorem NairTenenbaum.squarefree_log_sum_eq_primeFactors (f : ℕ → ℝ) (hf : ∀ (n : ℕ), ¬Squarefree n → f n = 0) (n : ℕ) : ∑ p ∈ n.primeFactors, f n * Real.log ↑p = f n * Real.log ↑n

theorem NairTenenbaum.summable_squarefree_primeFactors (f : ℕ → ℝ) (hf₀ : ∀ (n : ℕ), 0 ≤ f n) (hf : ∀ (n : ℕ), ¬Squarefree n → f n = 0) (hs : Summable fun (n : ℕ) => f n * Real.log ↑n) : Summable fun (x : (n : ℕ) × ↥n.primeFactors) => f x.fst * Real.log ↑↑x.snd

theorem NairTenenbaum.summable_squarefree_prime_cofactors (f : ℕ → ℝ) (hf₀ : ∀ (n : ℕ), 0 ≤ f n) (hf : ∀ (n : ℕ), ¬Squarefree n → f n = 0) (hs : Summable fun (n : ℕ) => f n * Real.log ↑n) : Summable fun (x : Nat.Primes × ℕ+) => f (↑x.1 * ↑x.2) * Real.log ↑↑x.1

theorem NairTenenbaum.tsum_squarefree_log_eq_prime_cofactors (f : ℕ → ℝ) (hf₀ : ∀ (n : ℕ), 0 ≤ f n) (hf : ∀ (n : ℕ), ¬Squarefree n → f n = 0) (hs : Summable fun (n : ℕ) => f n * Real.log ↑n) : ∑' (n : ℕ), f n * Real.log ↑n = ∑' (p : Nat.Primes) (m : ℕ+), f (↑p * ↑m) * Real.log ↑↑p