summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum

English

Let f : ℕ → R be a multiplicative function (on coprime arguments), with f(1)=1 and f(0)=0, and assume ∑ ‖f(n)‖ converges. Then for any finite s, the sum over factoredNumbers(s) of f(m) equals the product over primes p in s of ∑'n f(p^n). Moreover, the corresponding norm-sum converges.

Русский

Пусть f: ℕ → R — мультипликативная функция, f(1)=1, f(0)=0, и суммируемость по нормам выполняется. Тогда для любого конечного множества s сумма по m из factoredNumbers(s) равна произведению по p ∈ s, p ров prime, ∑'n f(p^n), и аналогично для норм.

LaTeX

$$$\\forall s:\\ Finset\\mathbb N:\\ Summable_{m\\in\\mathrm{factoredNumbers}(s)} \\|f(m)\\| \\land HasSum_{m\\in\\mathrm{factoredNumbers}(s)} f(m) = \\prod_{p\\in s,\, p\\text{ prime}} \\sum_{n\\ge 0} f(p^n).$$$

Lean4

/-- We relate a finite product over primes in `s` to an infinite sum over `s`-factored numbers. -/
theorem summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum
    (hsum : ∀ {p : ℕ}, p.Prime → Summable (fun n : ℕ ↦ ‖f (p ^ n)‖)) (s : Finset ℕ) :
    Summable (fun m : factoredNumbers s ↦ ‖f m‖) ∧
      HasSum (fun m : factoredNumbers s ↦ f m) (∏ p ∈ s with p.Prime, ∑' n : ℕ, f (p ^ n)) :=
  by
  induction s using Finset.induction with
  | empty =>
    rw [factoredNumbers_empty]
    simp only [notMem_empty, IsEmpty.forall_iff, forall_const, filter_true_of_mem, prod_empty]
    exact ⟨(Set.finite_singleton 1).summable (‖f ·‖), hf₁ ▸ hasSum_singleton 1 f⟩
  | insert p s hp ih =>
    rw [filter_insert]
    split_ifs with hpp
    · constructor
      · simp only [← (equivProdNatFactoredNumbers hpp hp).summable_iff, Function.comp_def,
          equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
        refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_mul_le ..) ?_
        apply Summable.mul_of_nonneg (hsum hpp) ih.1 <;> exact fun n ↦ norm_nonneg _
      · have hp' : p ∉ {p ∈ s | p.Prime} := mt (mem_of_mem_filter p) hp
        rw [prod_insert hp', ← (equivProdNatFactoredNumbers hpp hp).hasSum_iff, Function.comp_def]
        conv =>
          enter [1, x]
          rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
        have : T3Space R := instT3Space
        apply
          (hsum hpp).of_norm.hasSum.mul
            ih.2
              -- `exact summable_mul_of_summable_norm (hsum hpp) ih.1` gives a time-out

        apply summable_mul_of_summable_norm (hsum hpp) ih.1
    · rwa [factoredNumbers_insert s hpp]

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