case pos
α : Type ?u.309286
β : Type u_1
γ : Type ?u.309292
f : β → ℝ≥0
h : Summable f
⊢ (∑' (b : β), f b) = ENNReal.toNNReal (∑' (b : β), ↑(f b))

case neg
α : Type ?u.309286
β : Type u_1
γ : Type ?u.309292
f : β → ℝ≥0
h : ¬Summable f
⊢ (∑' (b : β), f b) = ENNReal.toNNReal (∑' (b : β), ↑(f b))
α : Type ?u.309286
β : Type u_1
γ : Type ?u.309292
f : β → ℝ≥0
⊢ (∑' (b : β), f b) = ENNReal.toNNReal (∑' (b : β), ↑(f b))
by_cases h : Summable f
no goals
case pos
α : Type ?u.309286
β : Type u_1
γ : Type ?u.309292
f : β → ℝ≥0
h : Summable f
⊢ (∑' (b : β), f b) = ENNReal.toNNReal (∑' (b : β), ↑(f b))
rw [← ENNReal.coe_tsum h, ENNReal.toNNReal_coe]
case neg
α : Type ?u.309286
β : Type u_1
γ : Type ?u.309292
f : β → ℝ≥0
h : ¬Summable f
A : (∑' (b : β), f b) = 0
⊢ (∑' (b : β), f b) = ENNReal.toNNReal (∑' (b : β), ↑(f b))
case neg
α : Type ?u.309286
β : Type u_1
γ : Type ?u.309292
f : β → ℝ≥0
h : ¬Summable f
⊢ (∑' (b : β), f b) = ENNReal.toNNReal (∑' (b : β), ↑(f b))
have A := tsum_eq_zero_of_not_summable h
case neg
α : Type ?u.309286
β : Type u_1
γ : Type ?u.309292
f : β → ℝ≥0
A : (∑' (b : β), f b) = 0
h : (∑' (b : β), ↑(f b)) = ⊤
⊢ (∑' (b : β), f b) = ENNReal.toNNReal (∑' (b : β), ↑(f b))
case neg
α : Type ?u.309286
β : Type u_1
γ : Type ?u.309292
f : β → ℝ≥0
h : ¬Summable f
A : (∑' (b : β), f b) = 0
⊢ (∑' (b : β), f b) = ENNReal.toNNReal (∑' (b : β), ↑(f b))
simp only [← ENNReal.tsum_coe_ne_top_iff_summable, Classical.not_not] at h
no goals
case neg
α : Type ?u.309286
β : Type u_1
γ : Type ?u.309292
f : β → ℝ≥0
A : (∑' (b : β), f b) = 0
h : (∑' (b : β), ↑(f b)) = ⊤
⊢ (∑' (b : β), f b) = ENNReal.toNNReal (∑' (b : β), ↑(f b))
simp only [h, ENNReal.top_toNNReal, A]