feat(topology/algebra/infinite_sum): add tsum_even_add_odd (#6620)

Prove `∑' i, f (2 * i) + ∑' i, f (2 * i + 1) = ∑' i, f i` and some
supporting lemmas.

Author: urkud

src/algebra/ring/basic.lean

@@ -171,9 +171,17 @@ def even (a : α) : Prop := ∃ k, a = 2*k
 
 lemma even_iff_two_dvd {a : α} : even a ↔ 2 ∣ a := iff.rfl
 
+@[simp] lemma range_two_mul (α : Type*) [semiring α] :
+  set.range (λ x : α, 2 * x) = {a | even a} :=
+by { ext x, simp [even, eq_comm] }
+
 /-- An element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`. -/
 def odd (a : α) : Prop := ∃ k, a = 2*k + 1
 
+@[simp] lemma range_two_mul_add_one (α : Type*) [semiring α] :
+  set.range (λ x : α, 2 * x + 1) = {a | odd a} :=
+by { ext x, simp [odd, eq_comm] }
+
 theorem dvd_add {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
 dvd.elim h₁ (λ d hd, dvd.elim h₂ (λ e he, dvd.intro (d + e) (by simp [left_distrib, hd, he])))
 

src/data/nat/parity.lean

@@ -36,6 +36,9 @@ by rw [not_odd_iff, even_iff]
 @[simp] lemma odd_iff_not_even : odd n ↔ ¬ even n :=
 by rw [not_even_iff, odd_iff]
 
+lemma is_compl_even_odd : is_compl {n : ℕ | even n} {n | odd n} :=
+by simp [← set.compl_set_of, is_compl_compl]
+
 lemma even_or_odd (n : ℕ) : even n ∨ odd n :=
 or.imp_right (odd_iff_not_even.2) (em (even n))
 

src/topology/algebra/infinite_sum.lean

@@ -8,6 +8,7 @@ import topology.instances.real
 import topology.algebra.module
 import data.indicator_function
 import data.equiv.encodable.lattice
+import data.nat.parity
 import order.filter.at_top_bot
 
 /-!
@@ -150,6 +151,10 @@ lemma equiv.has_sum_iff (e : γ ≃ β) :
   has_sum (f ∘ e) a ↔ has_sum f a :=
 e.injective.has_sum_iff $ by simp
 
+lemma function.injective.has_sum_range_iff {g : γ → β} (hg : injective g) :
+  has_sum (λ x : set.range g, f x) a ↔ has_sum (f ∘ g) a :=
+(equiv.set.range g hg).has_sum_iff.symm
+
 lemma equiv.summable_iff (e : γ ≃ β) :
   summable (f ∘ e) ↔ summable f :=
 exists_congr $ λ a, e.has_sum_iff
@@ -231,10 +236,25 @@ lemma summable_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, summab
   summable (λb, ∑ i in s, f i b) :=
 (has_sum_sum $ assume i hi, (hf i hi).has_sum).summable
 
+lemma has_sum.add_disjoint {s t : set β} (hs : disjoint s t)
+  (ha : has_sum (f ∘ coe : s → α) a) (hb : has_sum (f ∘ coe : t → α) b) :
+  has_sum (f ∘ coe : s ∪ t → α) (a + b) :=
+begin
+  rw has_sum_subtype_iff_indicator at *,
+  rw set.indicator_union_of_disjoint hs,
+  exact ha.add hb
+end
+
+lemma has_sum.add_is_compl {s t : set β} (hs : is_compl s t)
+  (ha : has_sum (f ∘ coe : s → α) a) (hb : has_sum (f ∘ coe : t → α) b) :
+  has_sum f (a + b) :=
+by simpa [← hs.compl_eq]
+  using (has_sum_subtype_iff_indicator.1 ha).add (has_sum_subtype_iff_indicator.1 hb)
+
 lemma has_sum.add_compl {s : set β} (ha : has_sum (f ∘ coe : s → α) a)
   (hb : has_sum (f ∘ coe : sᶜ → α) b) :
   has_sum f (a + b) :=
-by simpa using (has_sum_subtype_iff_indicator.1 ha).add (has_sum_subtype_iff_indicator.1 hb)
+ha.add_is_compl is_compl_compl hb
 
 lemma summable.add_compl {s : set β} (hs : summable (f ∘ coe : s → α))
   (hsc : summable (f ∘ coe : sᶜ → α)) :
@@ -244,13 +264,29 @@ lemma summable.add_compl {s : set β} (hs : summable (f ∘ coe : s → α))
 lemma has_sum.compl_add {s : set β} (ha : has_sum (f ∘ coe : sᶜ → α) a)
   (hb : has_sum (f ∘ coe : s → α) b) :
   has_sum f (a + b) :=
-by simpa using (has_sum_subtype_iff_indicator.1 ha).add (has_sum_subtype_iff_indicator.1 hb)
+ha.add_is_compl is_compl_compl.symm hb
+
+lemma has_sum.even_add_odd {f : ℕ → α} (he : has_sum (λ k, f (2 * k)) a)
+  (ho : has_sum (λ k, f (2 * k + 1)) b) :
+  has_sum f (a + b) :=
+begin
+  have := mul_right_injective' (@two_ne_zero ℕ _ _),
+  replace he := this.has_sum_range_iff.2 he,
+  replace ho := ((add_left_injective 1).comp this).has_sum_range_iff.2 ho,
+  refine he.add_is_compl _ ho,
+  simpa [(∘)] using nat.is_compl_even_odd
+end
 
 lemma summable.compl_add {s : set β} (hs : summable (f ∘ coe : sᶜ → α))
   (hsc : summable (f ∘ coe : s → α)) :
   summable f :=
 (hs.has_sum.compl_add hsc.has_sum).summable
 
+lemma summable.even_add_odd {f : ℕ → α} (he : summable (λ k, f (2 * k)))
+  (ho : summable (λ k, f (2 * k + 1))) :
+  summable f :=
+(he.has_sum.even_add_odd ho.has_sum).summable
+
 lemma has_sum.sigma [regular_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α}
   (ha : has_sum f a) (hf : ∀b, has_sum (λc, f ⟨b, c⟩) (g b)) : has_sum g a :=
 begin
@@ -464,6 +500,23 @@ end
 
 end encodable
 
+variables [has_continuous_add α]
+
+lemma tsum_add_tsum_compl {s : set β} (hs : summable (f ∘ coe : s → α))
+  (hsc : summable (f ∘ coe : sᶜ → α)) :
+  (∑' x : s, f x) + (∑' x : sᶜ, f x) = ∑' x, f x :=
+(hs.has_sum.add_compl hsc.has_sum).tsum_eq.symm
+
+lemma tsum_union_disjoint {s t : set β} (hd : disjoint s t)
+  (hs : summable (f ∘ coe : s → α)) (ht : summable (f ∘ coe : t → α)) :
+  (∑' x : s ∪ t, f x) = (∑' x : s, f x) + (∑' x : t, f x) :=
+(hs.has_sum.add_disjoint hd ht.has_sum).tsum_eq
+
+lemma tsum_even_add_odd {f : ℕ → α} (he : summable (λ k, f (2 * k)))
+  (ho : summable (λ k, f (2 * k + 1))) :
+  (∑' k, f (2 * k)) + (∑' k, f (2 * k + 1)) = ∑' k, f k :=
+(he.has_sum.even_add_odd ho.has_sum).tsum_eq.symm
+
 end tsum
 
 section pi
@@ -562,11 +615,6 @@ hf.has_sum.neg.tsum_eq
 lemma tsum_sub (hf : summable f) (hg : summable g) : ∑'b, (f b - g b) = ∑'b, f b - ∑'b, g b :=
 (hf.has_sum.sub hg.has_sum).tsum_eq
 
-lemma tsum_add_tsum_compl {s : set β} (hs : summable (f ∘ coe : s → α))
-  (hsc : summable (f ∘ coe : sᶜ → α)) :
-  (∑' x : s, f x) + (∑' x : sᶜ, f x) = ∑' x, f x :=
-(hs.has_sum.add_compl hsc.has_sum).tsum_eq.symm
-
 lemma sum_add_tsum_compl {s : finset β} (hf : summable f) :
   (∑ x in s, f x) + (∑' x : (↑s : set β)ᶜ, f x) = ∑' x, f x :=
 ((s.has_sum f).add_compl (s.summable_compl_iff.2 hf).has_sum).tsum_eq.symm