Theorems · Theorem · number theory

EulerProduct.norm_tsum_factoredNumbers_sub_tsum_lt

∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  Summable f →
    f 0 = 0 →
      ∀ {ε : ℝ},
        0 < ε →
          ∃ N, ∀ (s : Finset ℕ), N.primesBelow ⊆ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m‖ < ε

The following statement says that summing over s-factored numbers such that s contains primesBelow N for large enough N gets us arbitrarily close to the sum over all natural numbers (assuming f is summable and f 0 = 0; the latter since 0 is not s-factored).

Defined in

Mathlib.NumberTheory.EulerProduct.Basic

Cited by

2 results in Mathlib

Foundations

Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedCommRingCompleteSpace