summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum

English

Relates the product over primes below N to the sum over N-smooth numbers; equivalently, the same as the standard Euler product but here specialized to primesBelow and smooth numbers.

Русский

Связь произведения по простым до N с суммой по N-умным (N-smooth) числам; аналог Эйлерова произведения, но к указанным множествам.

LaTeX

$$$\\prod_{p\\in N.primesBelow} \\sum_{n\\ge0} f(p^n) = \\sum_{m\\in N.smoothNumbers} f(m).$$$

Lean4

/-- We relate a finite product over primes to an infinite sum over smooth numbers. -/
theorem summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum
    (hsum : ∀ {p : ℕ}, p.Prime → Summable (fun n : ℕ ↦ ‖f (p ^ n)‖)) (N : ℕ) :
    Summable (fun m : N.smoothNumbers ↦ ‖f m‖) ∧
      HasSum (fun m : N.smoothNumbers ↦ f m) (∏ p ∈ N.primesBelow, ∑' n : ℕ, f (p ^ n)) :=
  by
  rw [smoothNumbers_eq_factoredNumbers, primesBelow]
  exact summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum hf₁ hmul hsum _

Похожие утверждения