[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum f a₁
hg : HasSum g a₂
⊢ a₁ ≤ a₂
[PROOFSTEP]
rw [← hasSum_extend_zero he] at hf 
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
⊢ a₁ ≤ a₂
[PROOFSTEP]
refine hasSum_le (fun c => ?_) hf hg
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
⊢ extend e f 0 c ≤ g c
[PROOFSTEP]
obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e)
[GOAL]
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
i : ι
⊢ extend e f 0 (e i) ≤ g (e i)
[PROOFSTEP]
rw [he.extend_apply]
[GOAL]
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
i : ι
⊢ f i ≤ g (e i)
[PROOFSTEP]
exact h _
[GOAL]
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
h : ¬c ∈ Set.range e
⊢ extend e f 0 c ≤ g c
[PROOFSTEP]
rw [extend_apply' _ _ _ h]
[GOAL]
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
h : ¬c ∈ Set.range e
⊢ OfNat.ofNat 0 c ≤ g c
[PROOFSTEP]
exact hs _ h
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : HasSum f a
i : ι
hb : ∀ (j : ι), j ≠ i → 0 ≤ f j
⊢ ∀ (i_1 : ι), ¬i_1 ∈ {i} → 0 ≤ f i_1
[PROOFSTEP]
simpa
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
ha₂ : 0 ≤ a₂
h : ∀ (s : Finset ι), ∑ i in s, f i ≤ a₂
⊢ ∑' (i : ι), f i ≤ a₂
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
ha₂ : 0 ≤ a₂
h : ∀ (s : Finset ι), ∑ i in s, f i ≤ a₂
hf : Summable f
⊢ ∑' (i : ι), f i ≤ a₂
[PROOFSTEP]
exact tsum_le_of_sum_le hf h
[GOAL]
case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
ha₂ : 0 ≤ a₂
h : ∀ (s : Finset ι), ∑ i in s, f i ≤ a₂
hf : ¬Summable f
⊢ ∑' (i : ι), f i ≤ a₂
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf]
[GOAL]
case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
ha₂ : 0 ≤ a₂
h : ∀ (s : Finset ι), ∑ i in s, f i ≤ a₂
hf : ¬Summable f
⊢ 0 ≤ a₂
[PROOFSTEP]
exact ha₂
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 0 ≤ g i
⊢ 0 ≤ ∑' (i : ι), g i
[PROOFSTEP]
by_cases hg : Summable g
[GOAL]
case pos
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 0 ≤ g i
hg : Summable g
⊢ 0 ≤ ∑' (i : ι), g i
[PROOFSTEP]
exact hg.hasSum.nonneg h
[GOAL]
case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 0 ≤ g i
hg : ¬Summable g
⊢ 0 ≤ ∑' (i : ι), g i
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hg]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), f i ≤ 0
⊢ ∑' (i : ι), f i ≤ 0
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), f i ≤ 0
hf : Summable f
⊢ ∑' (i : ι), f i ≤ 0
[PROOFSTEP]
exact hf.hasSum.nonpos h
[GOAL]
case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), f i ≤ 0
hf : ¬Summable f
⊢ ∑' (i : ι), f i ≤ 0
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
⊢ HasSum f 0 ↔ f = 0
[PROOFSTEP]
refine' ⟨fun hf' => _, _⟩
[GOAL]
case refine'_1
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
hf' : HasSum f 0
⊢ f = 0
[PROOFSTEP]
ext i
[GOAL]
case refine'_1.h
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
hf' : HasSum f 0
i : ι
⊢ f i = OfNat.ofNat 0 i
[PROOFSTEP]
exact (hf i).antisymm' (le_hasSum hf' _ fun j _ => hf j)
[GOAL]
case refine'_2
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
⊢ f = 0 → HasSum f 0
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ OfNat.ofNat 0 i
⊢ HasSum 0 0
[PROOFSTEP]
exact hasSum_zero
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasSum f a₁
hg : HasSum g a₂
⊢ a₁ < a₂
[PROOFSTEP]
have : update f i 0 ≤ update g i 0 := update_le_update_iff.mpr ⟨rfl.le, fun i _ => h i⟩
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasSum f a₁
hg : HasSum g a₂
this : update f i 0 ≤ update g i 0
⊢ a₁ < a₂
[PROOFSTEP]
have : 0 - f i + a₁ ≤ 0 - g i + a₂ := hasSum_le this (hf.update i 0) (hg.update i 0)
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasSum f a₁
hg : HasSum g a₂
this✝ : update f i 0 ≤ update g i 0
this : 0 - f i + a₁ ≤ 0 - g i + a₂
⊢ a₁ < a₂
[PROOFSTEP]
simpa only [zero_sub, add_neg_cancel_left] using add_lt_add_of_lt_of_le hi this
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hsum : Summable g
hg : ∀ (i : ι), 0 ≤ g i
i : ι
hi : 0 < g i
⊢ 0 < ∑' (i : ι), g i
[PROOFSTEP]
rw [← tsum_zero]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hsum : Summable g
hg : ∀ (i : ι), 0 ≤ g i
i : ι
hi : 0 < g i
⊢ ∑' (x : ?m.47496), 0 < ∑' (i : ι), g i
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hsum : Summable g
hg : ∀ (i : ι), 0 ≤ g i
i : ι
hi : 0 < g i
⊢ Type ?u.47494
[PROOFSTEP]
exact tsum_lt_tsum hg hi summable_zero hsum
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
hf : Summable f
⊢ ∑' (i : ι), f i = 0 ↔ ∀ (x : ι), f x = 0
[PROOFSTEP]
rw [← hasSum_zero_iff, hf.hasSum_iff]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
hf : Summable f
⊢ ∑' (i : ι), f i ≠ 0 ↔ ∃ x, f x ≠ 0
[PROOFSTEP]
rw [Ne.def, tsum_eq_zero_iff hf, not_forall]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : CompleteSpace α
f : ι → α
s : Set ι := {x | 0 ≤ f x}
h1 : ∀ (x : ↑s), |f ↑x| = f ↑x
h2 : ∀ (x : ↑sᶜ), |f ↑x| = -f ↑x
⊢ ((Summable fun x => |f ↑x|) ∧ Summable fun x => |f ↑x|) ↔ (Summable fun x => f ↑x) ∧ Summable fun x => -f ↑x
[PROOFSTEP]
simp only [h1, h2]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : CompleteSpace α
f : ι → α
s : Set ι := {x | 0 ≤ f x}
h1 : ∀ (x : ↑s), |f ↑x| = f ↑x
h2 : ∀ (x : ↑sᶜ), |f ↑x| = -f ↑x
⊢ ((Summable fun x => f ↑x) ∧ Summable fun x => -f ↑x) ↔ Summable f
[PROOFSTEP]
simp only [summable_neg_iff, summable_subtype_and_compl]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
⊢ Finite ι
[PROOFSTEP]
have H : ∀ s : Finset ι, s.card • b ≤ ∑' _ : ι, b := fun s => by
  simpa using sum_le_hasSum s (fun a _ => hb.le) hf.hasSum
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
s : Finset ι
⊢ card s • b ≤ ∑' (x : ι), b
[PROOFSTEP]
simpa using sum_le_hasSum s (fun a _ => hb.le) hf.hasSum
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
⊢ Finite ι
[PROOFSTEP]
obtain ⟨n, hn⟩ := Archimedean.arch (∑' _ : ι, b) hb
[GOAL]
case intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
⊢ Finite ι
[PROOFSTEP]
have : ∀ s : Finset ι, s.card ≤ n := fun s => by simpa [nsmul_le_nsmul_iff hb] using (H s).trans hn
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
s : Finset ι
⊢ card s ≤ n
[PROOFSTEP]
simpa [nsmul_le_nsmul_iff hb] using (H s).trans hn
[GOAL]
case intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
this : ∀ (s : Finset ι), card s ≤ n
⊢ Finite ι
[PROOFSTEP]
have : Fintype ι := fintypeOfFinsetCardLe n this
[GOAL]
case intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
this✝ : ∀ (s : Finset ι), card s ≤ n
this : Fintype ι
⊢ Finite ι
[PROOFSTEP]
infer_instance
