Theorem: tendsto_sum_primesBelow_tsum (EulerProducts/Logarithm.lean)

State before:
R : Type u_1
inst✝⁴ : AddCommGroup R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : CompleteSpace R
inst✝ : T2Space R
f : ℕ → R
hsum : Summable f
⊢ Tendsto (fun n => ∑ p ∈ n.primesBelow, f p) atTop (𝓝 (∑' (p : Nat.Primes), f ↑p))
Tactic:
rw [(show ∑' p : Nat.Primes, f p = ∑' p : {p : ℕ | p.Prime}, f p from rfl)]
State after:
R : Type u_1
inst✝⁴ : AddCommGroup R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : CompleteSpace R
inst✝ : T2Space R
f : ℕ → R
hsum : Summable f
⊢ Tendsto (fun n => ∑ p ∈ n.primesBelow, f p) atTop (𝓝 (∑' (p : ↑{p | p.Prime}), f ↑p))

State before:
R : Type u_1
inst✝⁴ : AddCommGroup R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : CompleteSpace R
inst✝ : T2Space R
f : ℕ → R
hsum : Summable f
⊢ Tendsto (fun n => ∑ p ∈ n.primesBelow, f p) atTop (𝓝 (∑' (p : ↑{p | p.Prime}), f ↑p))
Tactic:
simp_rw [tsum_subtype, sum_primesBelow_eq_sum_range_indicator]
State after:
R : Type u_1
inst✝⁴ : AddCommGroup R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : CompleteSpace R
inst✝ : T2Space R
f : ℕ → R
hsum : Summable f
⊢ Tendsto (fun n => ∑ m ∈ Finset.range n, {p | p.Prime}.indicator (fun p => f p) m) atTop
    (𝓝 (∑' (x : ℕ), {p | p.Prime}.indicator f x))

State before:
R : Type u_1
inst✝⁴ : AddCommGroup R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : CompleteSpace R
inst✝ : T2Space R
f : ℕ → R
hsum : Summable f
⊢ Tendsto (fun n => ∑ m ∈ Finset.range n, {p | p.Prime}.indicator (fun p => f p) m) atTop
    (𝓝 (∑' (x : ℕ), {p | p.Prime}.indicator f x))
Tactic:
exact (Summable.hasSum_iff_tendsto_nat <| hsum.indicator _).mp <| (hsum.indicator _).hasSum
State after:
no goals