[GOAL]
α : Type u_1
⊢ Tendsto Real.toNNReal atTop atTop
[PROOFSTEP]
rw [← tendsto_coe_atTop]
[GOAL]
α : Type u_1
⊢ Tendsto (fun a => ↑(Real.toNNReal a)) atTop atTop
[PROOFSTEP]
exact tendsto_atTop_mono Real.le_coe_toNNReal tendsto_id
[GOAL]
α : Type u_1
⊢ ⨅ (l : ℝ≥0) (_ : ⊥ < l), 𝓟 (Set.Iio l) = ⨅ (a : ℝ≥0) (_ : a ≠ 0), 𝓟 (Set.Iio a)
[PROOFSTEP]
simp only [bot_lt_iff_ne_bot]
[GOAL]
α : Type u_1
⊢ ⨅ (l : ℝ≥0) (_ : l ≠ ⊥), 𝓟 (Set.Iio l) = ⨅ (a : ℝ≥0) (_ : a ≠ 0), 𝓟 (Set.Iio a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
⊢ HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r
[PROOFSTEP]
simp only [HasSum, ← coe_sum, tendsto_coe]
[GOAL]
α : Type u_1
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y
⊢ HasSum (fun x => Real.toNNReal (f x)) (Real.toNNReal y)
[PROOFSTEP]
lift y to ℝ≥0 using hy.nonneg hf₀
[GOAL]
case intro
α : Type u_1
f : α → ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
y : ℝ≥0
hy : HasSum f ↑y
⊢ HasSum (fun x => Real.toNNReal (f x)) (Real.toNNReal ↑y)
[PROOFSTEP]
lift f to α → ℝ≥0 using hf₀
[GOAL]
case intro.intro
α : Type u_1
y : ℝ≥0
f : α → ℝ≥0
hy : HasSum (fun i => ↑(f i)) ↑y
⊢ HasSum (fun x => Real.toNNReal ((fun i => ↑(f i)) x)) (Real.toNNReal ↑y)
[PROOFSTEP]
simpa [hasSum_coe] using hy
[GOAL]
α : Type u_1
f : α → ℝ≥0
⊢ (Summable fun a => ↑(f a)) ↔ Summable f
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
f : α → ℝ≥0
⊢ (Summable fun a => ↑(f a)) → Summable f
case mpr α : Type u_1 f : α → ℝ≥0 ⊢ Summable f → Summable fun a => ↑(f a)
[PROOFSTEP]
exact fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩
[GOAL]
case mpr
α : Type u_1
f : α → ℝ≥0
⊢ Summable f → Summable fun a => ↑(f a)
[PROOFSTEP]
exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩
[GOAL]
α : Type u_1
f : α → ℝ≥0
hf : ¬Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
[PROOFSTEP]
simp [tsum_def, hf, mt summable_coe.1 hf]
[GOAL]
α : Type u_1
a : ℝ≥0
f : α → ℝ≥0
⊢ ↑(∑' (x : α), a * f x) = ↑(a * ∑' (x : α), f x)
[PROOFSTEP]
simp only [coe_tsum, NNReal.coe_mul, tsum_mul_left]
[GOAL]
α : Type u_1
f : α → ℝ≥0
a : ℝ≥0
⊢ ↑(∑' (x : α), f x * a) = ↑((∑' (x : α), f x) * a)
[PROOFSTEP]
simp only [coe_tsum, NNReal.coe_mul, tsum_mul_right]
[GOAL]
α : Type u_1
β : Type u_2
f : α → ℝ≥0
hf : Summable f
i : β → α
hi : Function.Injective i
⊢ Summable (f ∘ i)
[PROOFSTEP]
rw [← summable_coe] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
i : β → α
hi : Function.Injective i
⊢ Summable fun a => ↑((f ∘ i) a)
[PROOFSTEP]
exact hf.comp_injective hi
[GOAL]
α : Type u_1
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun i => f (i + k)) ↔ Summable f
[PROOFSTEP]
rw [← summable_coe, ← summable_coe]
[GOAL]
α : Type u_1
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun a => ↑(f (a + k))) ↔ Summable fun a => ↑(f a)
[PROOFSTEP]
exact @summable_nat_add_iff ℝ _ _ _ (fun i => (f i : ℝ)) k
[GOAL]
α : Type u_1
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i in Finset.range k, f i)
[PROOFSTEP]
rw [← hasSum_coe, hasSum_nat_add_iff (f := fun n => toReal (f n)) k]
[GOAL]
α : Type u_1
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n => ↑(f n)) (↑a + ∑ i in Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i in Finset.range k, f i)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
f : α → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
[PROOFSTEP]
simp only [← summable_coe, ← tendsto_coe] at hf ⊢
[GOAL]
α : Type u_1
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
⊢ Tendsto (fun a => ↑(f a)) cofinite (𝓝 ↑0)
[PROOFSTEP]
exact hf.tendsto_cofinite_zero
[GOAL]
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f atTop (𝓝 0)
[PROOFSTEP]
rw [← Nat.cofinite_eq_atTop]
[GOAL]
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
[PROOFSTEP]
exact tendsto_cofinite_zero_of_summable hf
[GOAL]
α : Type u_1
f : α → ℝ≥0
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)
[PROOFSTEP]
simp_rw [← tendsto_coe, coe_tsum, NNReal.coe_zero]
[GOAL]
α : Type u_1
f : α → ℝ≥0
⊢ Tendsto (fun a => ∑' (a_1 : { x // ¬x ∈ a }), ↑(f ↑a_1)) atTop (𝓝 0)
[PROOFSTEP]
exact tendsto_tsum_compl_atTop_zero fun a : α => (f a : ℝ)
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ Tendsto (fun b => id b ^ n) atBot atBot
[PROOFSTEP]
simpa [OrderBot.atBot_eq, pos_iff_ne_zero]
