α : Type ?u.233118
β : Type u_1
γ : Type ?u.233124
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : β → ℝ≥0
h : (∑' (b : β), ↑(f b)) ≠ ⊤
⊢ Summable f
α : Type ?u.233118
β : Type u_1
γ : Type ?u.233124
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : β → ℝ≥0
⊢ (∑' (b : β), ↑(f b)) ≠ ⊤ ↔ Summable f
refine ⟨fun h => ?_, fun h => ENNReal.coe_tsum h ▸ ENNReal.coe_ne_top⟩
case intro
α : Type ?u.233118
β : Type u_1
γ : Type ?u.233124
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ Summable f
α : Type ?u.233118
β : Type u_1
γ : Type ?u.233124
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : β → ℝ≥0
h : (∑' (b : β), ↑(f b)) ≠ ⊤
⊢ Summable f
lift ∑' b, (f b : ℝ≥0∞) to ℝ≥0 using h with a ha
case intro
α : Type ?u.233118
β : Type u_1
γ : Type ?u.233124
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a => ↑(f a)) ↑a
case intro
α : Type ?u.233118
β : Type u_1
γ : Type ?u.233124
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ Summable f
refine' ⟨a, ENNReal.hasSum_coe.1 _⟩
case intro
α : Type ?u.233118
β : Type u_1
γ : Type ?u.233124
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a => ↑(f a)) (∑' (b : β), ↑(f b))
case intro
α : Type ?u.233118
β : Type u_1
γ : Type ?u.233124
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a => ↑(f a)) ↑a
rw [ha]
no goals
case intro
α : Type ?u.233118
β : Type u_1
γ : Type ?u.233124
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a => ↑(f a)) (∑' (b : β), ↑(f b))
exact ENNReal.summable.hasSum