An exponential Euler bound for squarefree prime products

The finite bound uses the injection from squarefree integers to their prime factor sets. Passing to all integers proves convergence as well as the bound.

theorem NairTenenbaum.prime_finset_sum_le_tsum (a : ℕ → ℝ) (ha : ∀ (p : ℕ), Nat.Prime p → 0 ≤ a p) (hs : Summable fun (p : Nat.Primes) => a ↑p) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : ∑ p ∈ S, a p ≤ ∑' (p : Nat.Primes), a ↑p

noncomputable def NairTenenbaum.squarefreePrimeProduct (a : ℕ → ℝ) (n : ℕ) : ℝ

The product of the primes in a finite support.

Equations

• NairTenenbaum.squarefreePrimeProduct a n = if Squarefree n then ∏ p ∈ n.primeFactors, a p else 0

theorem NairTenenbaum.squarefreePrimeProduct_nonneg {a : ℕ → ℝ} (ha : ∀ (p : ℕ), Nat.Prime p → 0 ≤ a p) (n : ℕ) : 0 ≤ squarefreePrimeProduct a n

theorem NairTenenbaum.squarefreePrimeProduct_sum_le_prod {a : ℕ → ℝ} (ha : ∀ (p : ℕ), Nat.Prime p → 0 ≤ a p) (T S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (hTS : ∀ n ∈ T, Squarefree n → n.primeFactors ⊆ S) : ∑ n ∈ T, squarefreePrimeProduct a n ≤ ∏ p ∈ S, (1 + a p)

theorem NairTenenbaum.summable_and_tsum_squarefreePrimeProduct_le_exp {a : ℕ → ℝ} (ha : ∀ (p : ℕ), Nat.Prime p → 0 ≤ a p) (hs : Summable fun (p : Nat.Primes) => a ↑p) : Summable (squarefreePrimeProduct a) ∧ ∑' (n : ℕ), squarefreePrimeProduct a n ≤ Real.exp (∑' (p : Nat.Primes), a ↑p)