feat(topology): prove geometric series

algebra/big_operators.lean

@@ -91,6 +91,9 @@ fold_union_inter
 lemma prod_union (h : s₁ ∩ s₂ = ∅) : (s₁ ∪ s₂).prod f = s₁.prod f * s₂.prod f :=
 by rw [←prod_union_inter, h]; simp
 
+lemma prod_sdiff (h : s₁ ⊆ s₂) : (s₂ \ s₁).prod f * s₁.prod f = s₂.prod f :=
+by rw [←prod_union sdiff_inter_self, sdiff_union_of_subset h]
+
 lemma prod_bind [decidable_eq γ] {s : finset γ} {t : γ → finset α} :
   (∀x∈s, ∀y∈s, x ≠ y → t x ∩ t y = ∅) → (s.bind t).prod f = s.prod (λx, (t x).prod f) :=
 s.induction_on (by simp) $
@@ -140,9 +143,7 @@ eq.trans (by rw [h₁]; refl) (fold_hom h₂)
 lemma prod_subset (h : s₁ ⊆ s₂) (hf : ∀x∈s₂, x ∉ s₁ → f x = 1) : s₁.prod f = s₂.prod f :=
 have (s₂ \ s₁).prod f = (s₂ \ s₁).prod (λx, 1),
   from prod_congr begin simp [hf] {contextual := tt} end,
-calc s₁.prod f = (s₂ \ s₁).prod f * s₁.prod f : by simp [this]
-  ... = ((s₂ \ s₁) ∪ s₁).prod f : by rw [prod_union]; exact sdiff_inter_self
-  ... = s₂.prod f : by rw [sdiff_union_of_subset h]
+by rw [←prod_sdiff h]; simp [this]
 
 end comm_monoid
 
@@ -236,6 +237,7 @@ run_cmd transport_multiplicative_to_additive [
   (`finset.prod_const_one, `finset.sum_const_zero),
   (`finset.prod_comm, `finset.sum_comm),
   (`finset.prod_sigma, `finset.sum_sigma),
+  (`finset.prod_sdiff, `finset.sum_sdiff),
   (`finset.prod_subset, `finset.sum_subset)]
 
 namespace finset
@@ -331,4 +333,17 @@ calc s₁.sum f = (s₁.filter (λx, f x = 0)).sum f + (s₁.filter (λx, f x 
 
 end canonically_ordered_monoid
 
+section discrete_linear_ordered_field
+variables [discrete_linear_ordered_field α] [decidable_eq β]
+
+lemma abs_sum_le_sum_abs {f : β → α} {s : finset β} : abs (s.sum f) ≤ s.sum (λa, abs (f a)) :=
+s.induction_on (by simp [abs_zero]) $
+  assume a s has ih,
+  calc abs (sum (insert a s) f) ≤ abs (f a) + abs (sum s f) :
+      by simp [has]; exact abs_add_le_abs_add_abs _ _
+    ... ≤ abs (f a) + s.sum (λa, abs (f a)) : add_le_add (le_refl _) ih
+    ... ≤ sum (insert a s) (λ (a : β), abs (f a)) : by simp [has]
+
+end discrete_linear_ordered_field
+
 end finset

algebra/group_power.lean

@@ -11,11 +11,16 @@ a^n is used for the first, but users can locally redefine it to gpow when needed
 
 Note: power adopts the convention that 0^0=1.
 -/
-import data.nat.basic data.int.basic tactic.finish 
+import data.nat.basic data.int.basic tactic.finish
 
 universe u
 variable {α : Type u}
 
+@[simp] theorem inv_one [division_ring α] : (1⁻¹ : α) = 1 := by rw [inv_eq_one_div, one_div_one]
+
+@[simp] theorem inv_inv' [discrete_field α] {a:α} : a⁻¹⁻¹ = a :=
+by rw [inv_eq_one_div, inv_eq_one_div, div_div_eq_mul_div]; simp [div_one]
+
 class has_pow_nat (α : Type u) :=
 (pow_nat : α → nat → α)
 
@@ -50,9 +55,9 @@ theorem pow_succ (a : α) (n : ℕ) : a^(n+1) = a * a^n := rfl
 theorem pow_mul_comm' (a : α) (n : ℕ) : a^n * a = a * a^n :=
 by induction n with n ih; simp [*, pow_succ]
 
-theorem pow_succ' (a : α) (n : ℕ) : a^(n+1) = a^n * a := 
+theorem pow_succ' (a : α) (n : ℕ) : a^(n+1) = a^n * a :=
 by simp [pow_succ, pow_mul_comm']
- 
+
 theorem pow_add (a : α) (m n : ℕ) : a^(m + n) = a^m * a^n :=
 by induction n; simp [*, pow_succ', nat.add_succ]
 
@@ -74,7 +79,7 @@ section comm_monoid
 variable [comm_monoid α]
 
 theorem mul_pow (a b : α) : ∀ n, (a * b)^n = a^n * b^n
-| 0     := by simp 
+| 0     := by simp
 | (n+1) := by simp [pow_succ]; rw mul_pow
 
 end comm_monoid
@@ -86,7 +91,7 @@ section nat
 
 theorem inv_pow (a : α) : ∀n, (a⁻¹)^n = (a^n)⁻¹
 | 0     := by simp
-| (n+1) := by rw [pow_succ', _root_.pow_succ, mul_inv_rev, inv_pow] 
+| (n+1) := by rw [pow_succ', _root_.pow_succ, mul_inv_rev, inv_pow]
 
 theorem pow_sub (a : α) {m n : ℕ} (h : m ≥ n) : a^(m - n) = a^m * (a^n)⁻¹ :=
 have h1 : m - n + n = m, from nat.sub_add_cancel h,
@@ -126,7 +131,7 @@ or.elim (nat.lt_or_ge m (nat.succ n))
   suffices (a^(nat.succ n - m))⁻¹ = (gpow a (of_nat m)) * (gpow a -[1+n]), by rw ←succ_sub; assumption,
   by rw pow_sub; finish [gpow])
  (assume : m ≥ succ n,
-  suffices gpow a (of_nat (m - succ n)) = (gpow a (of_nat m)) * (gpow a -[1+ n]), 
+  suffices gpow a (of_nat (m - succ n)) = (gpow a (of_nat m)) * (gpow a -[1+ n]),
     by rw [of_nat_add_neg_succ_of_nat_of_ge]; assumption,
   suffices a ^ (m - succ n) = a^m * (a^succ n)⁻¹, from this,
   by rw pow_sub; assumption)
@@ -135,31 +140,54 @@ theorem gpow_add (a : α) : ∀i j : int, gpow a (i + j) = gpow a i * gpow a j
 | (of_nat m) (of_nat n) := pow_add _ _ _
 | (of_nat m) -[1+n]     := gpow_add_aux _ _ _
 | -[1+m]     (of_nat n) := begin rw [add_comm, gpow_add_aux], unfold gpow, rw [←inv_pow, pow_inv_comm] end
-| -[1+m]     -[1+n]     := 
+| -[1+m]     -[1+n]     :=
   suffices (a ^ (m + succ (succ n)))⁻¹ = (a ^ succ m)⁻¹ * (a ^ succ n)⁻¹, from this,
   by rw [←succ_add_eq_succ_add, add_comm, _root_.pow_add, mul_inv_rev]
 
 theorem gpow_mul_comm (a : α) (i j : ℤ) : gpow a i * gpow a j = gpow a j * gpow a i :=
 by rw [←gpow_add, ←gpow_add, add_comm]
 end group
 
+theorem pow_ne_zero [integral_domain α] {a : α} {n : ℕ} (h : a ≠ 0) : a ^ n ≠ 0 :=
+by induction n with n ih; simp [pow_succ, mul_eq_zero_iff_eq_zero_or_eq_zero, *]
+
+section discrete_field
+variables [discrete_field α] {a b c : α} {n : ℕ}
+
+theorem pow_inv (ha : a ≠ 0) : a⁻¹ ^ n = (a ^ n)⁻¹ :=
+by induction n with n ih; simp [pow_succ, mul_inv', pow_ne_zero, *]
+
+end discrete_field
+
 section ordered_ring
 variable [linear_ordered_ring α]
 
-theorem pow_pos {a : α} (H : a > 0) : ∀ (n : ℕ), a ^ n > 0 
+theorem pow_pos {a : α} (H : a > 0) : ∀ (n : ℕ), a ^ n > 0
 | 0     := by simp; apply zero_lt_one
 | (n+1) := begin simp [_root_.pow_succ], apply mul_pos, assumption, apply pow_pos end
 
-theorem pow_ge_one_of_ge_one {a : α} (H : a ≥ 1) : ∀ (n : ℕ), a ^ n ≥ 1 
+theorem pow_nonneg {a : α} (H : a ≥ 0) : ∀ (n : ℕ), a ^ n ≥ 0
+| 0     := by simp; apply zero_le_one
+| (n+1) := begin simp [_root_.pow_succ], apply mul_nonneg, assumption, apply pow_nonneg end
+
+theorem pow_ge_one_of_ge_one {a : α} (H : a ≥ 1) : ∀ (n : ℕ), a ^ n ≥ 1
 | 0     := by simp; apply le_refl
-| (n+1) := 
-  begin 
-   simp [_root_.pow_succ], rw ←(one_mul (1 : α)), 
-   apply mul_le_mul, 
+| (n+1) :=
+  begin
+   simp [_root_.pow_succ], rw ←(one_mul (1 : α)),
+   apply mul_le_mul,
    assumption,
-   apply pow_ge_one_of_ge_one,  
+   apply pow_ge_one_of_ge_one,
    apply zero_le_one,
    transitivity, apply zero_le_one, assumption
   end
 
+theorem pow_le_pow {a : α} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
+let ⟨k, hk⟩ := nat.le.dest h in
+calc a ^ n = a ^ n * 1 : by simp
+  ... ≤ a ^ n * a ^ k : mul_le_mul_of_nonneg_left
+    (pow_ge_one_of_ge_one ha _)
+    (pow_nonneg (le_trans zero_le_one ha) _)
+  ... = a ^ m : by rw [←hk, pow_add]
+
 end ordered_ring

data/finset/basic.lean

@@ -560,7 +560,7 @@ ext $ assume a, by by_cases p a; simp [*] {contextual := tt}
 end filter
 
 section sdiff
-variables [decidable_eq α] {a : α} {s₁ s₂ : finset α}
+variables [decidable_eq α] {a : α} {s₁ s₂ t₁ t₂ : finset α}
 
 instance : has_sdiff (finset α) := ⟨λs₁ s₂, s₁.filter (λa, a ∉ s₂)⟩
 
@@ -574,6 +574,12 @@ ext $ assume a,
 lemma sdiff_inter_self : (s₂ \ s₁) ∩ s₁ = ∅ :=
 ext $ by simp {contextual := tt}
 
+lemma sdiff_subset_sdiff : t₁ ⊆ t₂ → s₂ ⊆ s₁ → t₁ \ s₁ ⊆ t₂ \ s₂ :=
+begin
+  simp [subset_iff, mem_sdiff_iff] {contextual := tt},
+  exact assume h₁ h₂ a _ ha₁ ha₂, ha₁ $ h₂ _ ha₂
+end
+
 end sdiff
 
 /- upto -/
@@ -600,6 +606,29 @@ theorem upto_zero : upto 0 = ∅ := rfl
 theorem upto_succ : upto (succ n) = insert n (upto n) :=
 ext $ by simp [mem_upto_iff, mem_insert_iff, lt_succ_iff_lt_or_eq]
 
+@[simp] theorem not_mem_upto : n ∉ upto n :=
+by simp [mem_upto_iff, lt_irrefl]
+
+@[simp] theorem upto_subset_upto_iff {n m} : upto n ⊆ upto m ↔ n ≤ m :=
+begin
+  simp [subset_iff, mem_upto_iff],
+  constructor,
+  { cases n,
+    case nat.zero { simp [nat.zero_le] },
+    case nat.succ n { exact assume h, h _ (lt_succ_self _) } },
+  { exact assume h i hi, lt_of_lt_of_le hi h }
+end
+
+theorem exists_nat_subset_upto {s : finset ℕ} : ∃n:ℕ, s ⊆ upto n :=
+s.induction_on ⟨0, by simp⟩ $
+  assume a s ha ⟨n, hn⟩,
+  ⟨max (a + 1) n, subset_iff.mpr $ assume x,
+    begin
+      simp [subset_iff, mem_upto_iff] at hn,
+      simp [or_imp_distrib, mem_upto_iff, lt_max_iff, hn] {contextual := tt},
+      exact assume _, or.inr (lt_succ_self a)
+    end⟩
+
 end upto
 
 /- useful rules for calculations with quantifiers -/

topology/infinite_sum.lean

@@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 Infinite sum over a topological monoid
+
+This sum is known as unconditionally convergent, as it sums to the same value under all possible
+permutations. For Euclidean spaces (finite dimensional Banach spaces) this is equivalent to absolute
+convergence.
 -/
-import data.set data.finset topology.topological_structures algebra.big_operators
+import data.set data.finset topology.topological_structures topology.metric_space algebra.big_operators
   logic.function_inverse
 noncomputable theory
 open set lattice finset filter function
@@ -22,11 +26,17 @@ iff.intro
 
 end logic
 
+lemma add_div {α : Type*} [division_ring α] {a b c : α} : (a + b) / c = a / c + b / c :=
+by rw [div_eq_mul_one_div, add_mul, ←div_eq_mul_one_div, ←div_eq_mul_one_div]
+
 open classical
 local attribute [instance] decidable_inhabited prop_decidable
 
 namespace filter
 
+lemma mem_at_top [preorder α] (a : α) : {b : α | a ≤ b} ∈ (@at_top α _).sets :=
+mem_infi_sets a $ subset.refl _
+
 lemma mem_infi_sets_finset {s : finset α} {f : α → filter β} :
   ∀t, t ∈ (⨅a∈s, f a).sets ↔ (∃p:α → set β, (∀a∈s, p a ∈ (f a).sets) ∧ (⋂a∈s, p a) ⊆ t) :=
 show ∀t,  t ∈ (⨅a∈s, f a).sets ↔ (∃p:α → set β, (∀a∈s, p a ∈ (f a).sets) ∧ (⨅a∈s, p a) ≤ t),
@@ -46,6 +56,8 @@ show ∀t,  t ∈ (⨅a∈s, f a).sets ↔ (∃p:α → set β, (∀a∈s, p a 
 
 end filter
 
+open filter
+
 section topological_space
 
 variables [topological_space α]
@@ -176,6 +188,14 @@ have (λs:finset β, s.sum (g ∘ f)) = g ∘ (λs:finset β, s.sum f),
 show tendsto (λs:finset β, s.sum (g ∘ f)) at_top (nhds (g a)),
   by rw [this]; exact tendsto_compose hf (continuous_iff_tendsto.mp h₃ a)
 
+lemma tendsto_sum_nat_of_is_sum {f : ℕ → α} (h : is_sum f a) :
+  tendsto (λn:ℕ, (upto n).sum f) at_top (nhds a) :=
+suffices map (λ (n : ℕ), sum (upto n) f) at_top ≤ map (λ (s : finset ℕ), sum s f) at_top,
+  from le_trans this h,
+assume s (hs : {t : finset ℕ | t.sum f ∈ s} ∈ at_top.sets),
+let ⟨t, ht⟩ := mem_at_top_iff.mp hs, ⟨n, hn⟩ := @exists_nat_subset_upto t in
+mem_at_top_iff.mpr ⟨n, assume n' hn', ht _ $ subset.trans hn $ upto_subset_upto_iff.mpr hn'⟩
+
 lemma is_sum_sigma [regular_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α}
   (hf : ∀b, is_sum (λc, f ⟨b, c⟩) (g b)) (ha : is_sum f a) : is_sum g a :=
 assume s' hs',
@@ -481,7 +501,64 @@ suffices cauchy (at_top.map (λs:finset β, s.sum f')),
       from hss' this $ refl_mem_uniformity hs,
     by rwa [eq h₁, eq h₂] at this,
   mem_prod_same_iff.mpr ⟨(λu:finset β, u.sum f') '' {u | t ⊆ u},
-    image_mem_map $ mem_infi_sets t $ mem_principal_sets.mpr $ subset.refl _,
+    image_mem_map $ mem_at_top t,
     assume ⟨a₁, a₂⟩ ⟨⟨t₁, h₁, eq₁⟩, ⟨t₂, h₂, eq₂⟩⟩, by simp at eq₁ eq₂; rw [←eq₁, ←eq₂]; exact this h₁ h₂⟩⟩
 
 end uniform_group
+
+section real
+
+lemma has_sum_of_absolute_convergence {f : ℕ → ℝ}
+  (hf : ∃r, tendsto (λn, (upto n).sum (λi, abs (f i))) at_top (nhds r)) : has_sum f :=
+let f' := λs:finset ℕ, s.sum (λi, abs (f i)) in
+suffices cauchy (map (λs:finset ℕ, s.sum f) at_top),
+  from complete_space.complete this,
+cauchy_iff.mpr $ and.intro (map_ne_bot at_top_ne_bot) $
+assume s hs,
+let ⟨ε, hε, hsε⟩ := mem_uniformity_dist.mp hs, ⟨r, hr⟩ := hf in
+have hε' : {p : ℝ × ℝ | dist p.1 p.2 < ε / 2} ∈ (@uniformity ℝ _).sets,
+  from mem_uniformity_dist.mpr ⟨ε / 2, div_pos_of_pos_of_pos hε two_pos, assume a b h, h⟩,
+have cauchy (at_top.map $ λn, f' (upto n)),
+  from cauchy_downwards cauchy_nhds (map_ne_bot at_top_ne_bot) hr,
+have ∃n, ∀{n'}, n ≤ n' → dist (f' (upto n)) (f' (upto n')) < ε / 2,
+  by simp [cauchy_iff, mem_at_top_iff] at this;
+  from let ⟨t, ht, u, hu⟩ := this _ hε' in
+    ⟨u, assume n' hn, ht $ prod_mk_mem_set_prod_eq.mpr ⟨hu _ (le_refl _), hu _ hn⟩⟩,
+let ⟨n, hn⟩ := this in
+have ∀{s}, upto n ⊆ s → abs ((s \ upto n).sum f) < ε / 2,
+  from assume s hs,
+  let ⟨n', hn'⟩ := @exists_nat_subset_upto s in
+  have upto n ⊆ upto n', from subset.trans hs hn',
+  have f'_nn : 0 ≤ f' (upto n' \ upto n), from zero_le_sum $ assume _ _, abs_nonneg _,
+  calc abs ((s \ upto n).sum f) ≤ f' (s \ upto n) : abs_sum_le_sum_abs
+    ... ≤ f' (upto n' \ upto n) : sum_le_sum_of_subset_of_nonneg
+      (finset.sdiff_subset_sdiff hn' (finset.subset.refl _))
+      (assume _ _ _, abs_nonneg _)
+    ... = abs (f' (upto n' \ upto n)) : (abs_of_nonneg f'_nn).symm
+    ... = abs (f' (upto n') - f' (upto n)) :
+      by simp [f', (sum_sdiff ‹upto n ⊆ upto n'›).symm]
+    ... = abs (f' (upto n) - f' (upto n')) : abs_sub _ _
+    ... < ε / 2 : hn $ upto_subset_upto_iff.mp this,
+have ∀{s t}, upto n ⊆ s → upto n ⊆ t → dist (s.sum f) (t.sum f) < ε,
+  from assume s t hs ht,
+  calc abs (s.sum f - t.sum f) = abs ((s \ upto n).sum f + - (t \ upto n).sum f) :
+      by rw [←sum_sdiff hs, ←sum_sdiff ht]; simp
+    ... ≤ abs ((s \ upto n).sum f) + abs ((t \ upto n).sum f) :
+      le_trans (abs_add_le_abs_add_abs _ _) $ by rw [abs_neg]; exact le_refl _
+    ... < ε / 2 + ε / 2 : add_lt_add (this hs) (this ht)
+    ... = ε : by rw [←add_div, add_self_div_two],
+⟨(λs:finset ℕ, s.sum f) '' {s | upto n ⊆ s}, image_mem_map $ mem_at_top (upto n),
+  assume ⟨a, b⟩ ⟨⟨t, ht, ha⟩, ⟨s, hs, hb⟩⟩, by simp at ha hb; exact ha ▸ hb ▸ hsε _ _ (this ht hs)⟩
+
+lemma is_sum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} {r : ℝ} (hf : ∀n, 0 ≤ f n) :
+  is_sum f r ↔ tendsto (λn, (upto n).sum f) at_top (nhds r) :=
+⟨tendsto_sum_nat_of_is_sum,
+  assume hr,
+  have tendsto (λn, (upto n).sum (λn, abs (f n))) at_top (nhds r),
+    by simp [(λi, abs_of_nonneg (hf i)), hr],
+  let ⟨p, h⟩ := has_sum_of_absolute_convergence ⟨r, this⟩ in
+  have hp : tendsto (λn, (upto n).sum f) at_top (nhds p), from tendsto_sum_nat_of_is_sum h,
+  have p = r, from tendsto_nhds_unique at_top_ne_bot hp hr,
+  this ▸ h⟩
+
+end real