α : Type u_1
β : Type ?u.330764
γ : Type ?u.330767
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ update (fun x => f x) i 0 i' ≤ f i'
α : Type u_1
β : Type ?u.330764
γ : Type ?u.330767
f : α → ℝ≥0
hf : Summable f
i : α
⊢ (∑' (x : α), f x) = f i + ∑' (x : α), if x = i then 0 else f x
refine' tsum_eq_add_tsum_ite' i (NNReal.summable_of_le (fun i' => _) hf)
α : Type u_1
β : Type ?u.330764
γ : Type ?u.330767
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ (if i' = i then 0 else f i') ≤ f i'
α : Type u_1
β : Type ?u.330764
γ : Type ?u.330767
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ update (fun x => f x) i 0 i' ≤ f i'
rw [Function.update_apply]
no goals
α : Type u_1
β : Type ?u.330764
γ : Type ?u.330767
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ (if i' = i then 0 else f i') ≤ f i'
split_ifs <;> simp only [zero_le', le_rfl]