feat(analysis): Cauchy sequence and series lemmas (#7858)

from LTE. Mostly relaxing assumptions from metric to
pseudo-metric and proving some obvious lemmas.

eventually_constant_prod and eventually_constant_sum are duplicated by hand because `to_additive` gets confused by the appearance of `1`.

In `norm_le_zero_iff' {G : Type*} [semi_normed_group G] [separated_space G]` and the following two lemmas the type classes assumptions look silly, but those lemmas are indeed useful in some specific situation in LTE.

Author: PatrickMassot

src/algebra/big_operators/basic.lean

@@ -761,6 +761,24 @@ lemma prod_range_succ' (f : ℕ → β) :
 | 0       := prod_range_succ _ _
 | (n + 1) := by rw [prod_range_succ _ n, mul_right_comm, ← prod_range_succ', prod_range_succ]
 
+lemma eventually_constant_prod {u : ℕ → β} {N : ℕ} (hu : ∀ n ≥ N, u n = 1) {n : ℕ} (hn : N ≤ n) :
+  ∏ k in range (n + 1), u k = ∏ k in range (N + 1), u k :=
+begin
+  obtain ⟨m, rfl : n = N + m⟩ := le_iff_exists_add.mp hn,
+  clear hn,
+  induction m with m hm,
+  { simp },
+  erw [prod_range_succ, hm],
+  simp [hu]
+end
+
+lemma eventually_constant_sum {β} [add_comm_monoid β] {u : ℕ → β} {N : ℕ}
+  (hu : ∀ n ≥ N, u n = 0) {n : ℕ} (hn : N ≤ n) :
+  ∑ k in range (n + 1), u k = ∑ k in range (N + 1), u k :=
+@eventually_constant_prod (multiplicative β) _ _ _ hu _ hn
+
+attribute [to_additive] eventually_constant_prod
+
 lemma prod_range_add (f : ℕ → β) (n m : ℕ) :
   ∏ x in range (n + m), f x =
   (∏ x in range n, f x) * (∏ x in range m, f (n + x)) :=

src/analysis/normed_space/basic.lean

@@ -208,6 +208,9 @@ lemma norm_le_insert (u v : α) : ∥v∥ ≤ ∥u∥ + ∥u - v∥ :=
 calc ∥v∥ = ∥u - (u - v)∥ : by abel
 ... ≤ ∥u∥ + ∥u - v∥ : norm_sub_le u _
 
+lemma norm_le_insert' (u v : α) : ∥u∥ ≤ ∥v∥ + ∥u - v∥ :=
+by { rw norm_sub_rev, exact norm_le_insert v u }
+
 lemma ball_0_eq (ε : ℝ) : ball (0:α) ε = {x | ∥x∥ < ε} :=
 set.ext $ assume a, by simp
 
@@ -294,6 +297,44 @@ lemma normed_group.tendsto_nhds_nhds {f : α → β} {x : α} {y : β} :
   tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x', ∥x' - x∥ < δ → ∥f x' - y∥ < ε :=
 by simp_rw [metric.tendsto_nhds_nhds, dist_eq_norm]
 
+lemma normed_group.cauchy_seq_iff {u : ℕ → α} :
+  cauchy_seq u ↔ ∀ ε > 0, ∃ N, ∀ m n, N ≤ m → N ≤ n → ∥u m - u n∥ < ε :=
+by simp [metric.cauchy_seq_iff, dist_eq_norm]
+
+lemma cauchy_seq.add {u v : ℕ → α} (hu : cauchy_seq u) (hv : cauchy_seq v) : cauchy_seq (u + v) :=
+begin
+  rw normed_group.cauchy_seq_iff at *,
+  intros ε ε_pos,
+  rcases hu (ε/2) (half_pos ε_pos) with ⟨Nu, hNu⟩,
+  rcases hv (ε/2) (half_pos ε_pos) with ⟨Nv, hNv⟩,
+  use max Nu Nv,
+  intros m n hm hn,
+  replace hm := max_le_iff.mp hm,
+  replace hn := max_le_iff.mp hn,
+
+  calc ∥(u + v) m - (u + v) n∥ = ∥u m + v m - (u n + v n)∥ : rfl
+  ... = ∥(u m - u n) + (v m - v n)∥ : by abel
+  ... ≤ ∥u m - u n∥ + ∥v m - v n∥ : norm_add_le _ _
+  ... < ε : by linarith only [hNu m n hm.1 hn.1, hNv m n hm.2 hn.2]
+end
+
+open finset
+
+lemma cauchy_seq_sum_of_eventually_eq {u v : ℕ → α} {N : ℕ} (huv : ∀ n ≥ N, u n = v n)
+  (hv : cauchy_seq (λ n, ∑ k in range (n+1), v k)) : cauchy_seq (λ n, ∑ k in range (n + 1), u k) :=
+begin
+  let d : ℕ → α := λ n, ∑ k in range (n + 1), (u k - v k),
+  rw show (λ n, ∑ k in range (n + 1), u k) = d + (λ n, ∑ k in range (n + 1), v k),
+    by { ext n, simp [d] },
+  have : ∀ n ≥ N, d n = d N,
+  { intros n hn,
+    dsimp [d],
+    rw eventually_constant_sum _ hn,
+    intros m hm,
+    simp [huv m hm] },
+  exact (tendsto_at_top_of_eventually_const this).cauchy_seq.add hv
+end
+
 /-- A homomorphism `f` of seminormed groups is Lipschitz, if there exists a constant `C` such that
 for all `x`, one has `∥f x∥ ≤ C * ∥x∥`. The analogous condition for a linear map of
 (semi)normed spaces is in `normed_space.operator_norm`. -/
@@ -619,6 +660,35 @@ lemma nat.norm_cast_le [has_one α] : ∀ n : ℕ, ∥(n : α)∥ ≤ n * ∥(1
 | (n + 1) := by { rw [n.cast_succ, n.cast_succ, add_mul, one_mul],
                   exact norm_add_le_of_le (nat.norm_cast_le n) le_rfl }
 
+lemma semi_normed_group.mem_closure_iff {s : set α} {x : α} :
+  x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, ∥x - y∥ < ε :=
+by simp [metric.mem_closure_iff, dist_eq_norm]
+
+lemma norm_le_zero_iff' [separated_space α] {g : α} :
+  ∥g∥ ≤ 0 ↔ g = 0 :=
+begin
+  have : g = 0 ↔ g ∈ closure ({0} : set α),
+  by simpa only [separated_space.out, mem_id_rel, sub_zero] using group_separation_rel g (0 : α),
+  rw [this, semi_normed_group.mem_closure_iff],
+  simp [forall_lt_iff_le']
+end
+
+lemma norm_eq_zero_iff' [separated_space α] {g : α} : ∥g∥ = 0 ↔ g = 0 :=
+begin
+  conv_rhs { rw ← norm_le_zero_iff' },
+  split ; intro h,
+  { rw h },
+  { exact le_antisymm h (norm_nonneg g) }
+end
+
+lemma norm_pos_iff' [separated_space α] {g : α} : 0 < ∥g∥ ↔ g ≠ 0 :=
+begin
+  rw lt_iff_le_and_ne,
+  simp only [norm_nonneg, true_and],
+  rw [ne_comm],
+  exact not_iff_not_of_iff (norm_eq_zero_iff'),
+end
+
 end semi_normed_group
 
 section normed_group
@@ -667,7 +737,7 @@ dist_zero_right g ▸ dist_eq_zero
 dist_zero_right g ▸ dist_pos
 
 @[simp] lemma norm_le_zero_iff {g : α} : ∥g∥ ≤ 0 ↔ g = 0 :=
-by { rw[←dist_zero_right], exact dist_le_zero }
+by { rw [← dist_zero_right], exact dist_le_zero }
 
 lemma eq_of_norm_sub_le_zero {g h : α} (a : ∥g - h∥ ≤ 0) : g = h :=
 by rwa [← sub_eq_zero, ← norm_le_zero_iff]

src/analysis/specific_limits.lean

@@ -180,7 +180,7 @@ begin
   tfae_finish
 end
 
-lemma uniformity_basis_dist_pow_of_lt_1 {α : Type*} [metric_space α]
+lemma uniformity_basis_dist_pow_of_lt_1 {α : Type*} [pseudo_metric_space α]
   {r : ℝ} (h₀ : 0 < r) (h₁ : r < 1) :
   (𝓤 α).has_basis (λ k : ℕ, true) (λ k, {p : α × α | dist p.1 p.2 < r ^ k}) :=
 metric.mk_uniformity_basis (λ i _, pow_pos h₀ _) $ λ ε ε0,
@@ -477,7 +477,7 @@ decaying terms.
 -/
 section edist_le_geometric
 
-variables [emetric_space α] (r C : ℝ≥0∞) (hr : r < 1) (hC : C ≠ ⊤) {f : ℕ → α}
+variables [pseudo_emetric_space α] (r C : ℝ≥0∞) (hr : r < 1) (hC : C ≠ ⊤) {f : ℕ → α}
   (hu : ∀n, edist (f n) (f (n+1)) ≤ C * r^n)
 
 include hr hC hu
@@ -513,7 +513,7 @@ end edist_le_geometric
 
 section edist_le_geometric_two
 
-variables [emetric_space α] (C : ℝ≥0∞) (hC : C ≠ ⊤) {f : ℕ → α}
+variables [pseudo_emetric_space α] (C : ℝ≥0∞) (hC : C ≠ ⊤) {f : ℕ → α}
   (hu : ∀n, edist (f n) (f (n+1)) ≤ C / 2^n) {a : α} (ha : tendsto f at_top (𝓝 a))
 
 include hC hu
@@ -550,7 +550,7 @@ end edist_le_geometric_two
 
 section le_geometric
 
-variables [metric_space α] {r C : ℝ} (hr : r < 1) {f : ℕ → α}
+variables [pseudo_metric_space α] {r C : ℝ} (hr : r < 1) {f : ℕ → α}
   (hu : ∀n, dist (f n) (f (n+1)) ≤ C * r^n)
 
 include hr hu
@@ -620,7 +620,11 @@ end le_geometric
 
 section summable_le_geometric
 
-variables [normed_group α] {r C : ℝ} {f : ℕ → α}
+variables [semi_normed_group α] {r C : ℝ} {f : ℕ → α}
+
+lemma semi_normed_group.cauchy_seq_of_le_geometric {C : ℝ} {r : ℝ} (hr : r < 1)
+  {u : ℕ → α} (h : ∀ n, ∥u n - u (n + 1)∥ ≤ C*r^n) : cauchy_seq u :=
+cauchy_seq_of_le_geometric r C hr (by simpa [dist_eq_norm] using h)
 
 lemma dist_partial_sum_le_of_le_geometric (hf : ∀n, ∥f n∥ ≤ C * r^n) (n : ℕ) :
   dist (∑ i in range n, f i) (∑ i in range (n+1), f i) ≤ C * r ^ n :=
@@ -648,6 +652,63 @@ begin
   exact ha.tendsto_sum_nat
 end
 
+@[simp] lemma dist_partial_sum (u : ℕ → α) (n : ℕ) :
+ dist (∑ k in range (n + 1), u k) (∑ k in range n, u k) = ∥u n∥ :=
+by simp [dist_eq_norm, sum_range_succ]
+
+@[simp] lemma dist_partial_sum' (u : ℕ → α) (n : ℕ) :
+ dist (∑ k in range n, u k) (∑ k in range (n+1), u k) = ∥u n∥ :=
+by simp [dist_eq_norm', sum_range_succ]
+
+lemma cauchy_series_of_le_geometric {C : ℝ} {u : ℕ → α}
+  {r : ℝ} (hr : r < 1) (h : ∀ n, ∥u n∥ ≤ C*r^n) : cauchy_seq (λ n, ∑ k in range n, u k) :=
+cauchy_seq_of_le_geometric r C hr (by simp [h])
+
+lemma normed_group.cauchy_series_of_le_geometric' {C : ℝ} {u : ℕ → α} {r : ℝ} (hr : r < 1)
+  (h : ∀ n, ∥u n∥ ≤ C*r^n) : cauchy_seq (λ n, ∑ k in range (n + 1), u k) :=
+begin
+  by_cases hC : C = 0,
+  { subst hC,
+    simp at h,
+    exact cauchy_seq_of_le_geometric 0 0 zero_lt_one (by simp [h]) },
+  have : 0 ≤ C,
+  { simpa using (norm_nonneg _).trans (h 0) },
+  replace hC : 0 < C,
+    from (ne.symm hC).le_iff_lt.mp this,
+  have : 0 ≤ r,
+  { have := (norm_nonneg _).trans (h 1),
+    rw pow_one at this,
+    exact (zero_le_mul_left hC).mp this },
+  simp_rw finset.sum_range_succ_comm,
+  have : cauchy_seq u,
+  { apply tendsto.cauchy_seq,
+    apply squeeze_zero_norm h,
+    rw show 0 = C*0, by simp,
+    exact tendsto_const_nhds.mul (tendsto_pow_at_top_nhds_0_of_lt_1 this hr) },
+  exact this.add (cauchy_series_of_le_geometric hr h),
+end
+
+lemma normed_group.cauchy_series_of_le_geometric'' {C : ℝ} {u : ℕ → α} {N : ℕ} {r : ℝ}
+  (hr₀ : 0 < r) (hr₁ : r < 1)
+  (h : ∀ n ≥ N, ∥u n∥ ≤ C*r^n) : cauchy_seq (λ n, ∑ k in range (n + 1), u k) :=
+begin
+  set v : ℕ → α := λ n, if n < N then 0 else u n,
+  have hC : 0 ≤ C,
+    from (zero_le_mul_right $ pow_pos hr₀ N).mp ((norm_nonneg _).trans $ h N $ le_refl N),
+  have : ∀ n ≥ N, u n = v n,
+  { intros n hn,
+    simp [v, hn, if_neg (not_lt.mpr hn)] },
+  refine cauchy_seq_sum_of_eventually_eq this (normed_group.cauchy_series_of_le_geometric' hr₁ _),
+  { exact C },
+  intro n,
+  dsimp [v],
+  split_ifs with H H,
+  { rw norm_zero,
+    exact mul_nonneg hC (pow_nonneg hr₀.le _) },
+  { push_neg at H,
+    exact h _ H }
+end
+
 end summable_le_geometric
 
 section normed_ring_geometric

src/topology/basic.lean

@@ -675,6 +675,14 @@ all_mem_nhds_filter _ _ (λ s t h, preimage_mono h) _
 lemma tendsto_const_nhds {a : α} {f : filter β} : tendsto (λb:β, a) f (𝓝 a) :=
 tendsto_nhds.mpr $ assume s hs ha, univ_mem_sets' $ assume _, ha
 
+lemma tendsto_at_top_of_eventually_const {ι : Type*} [semilattice_sup ι] [nonempty ι]
+  {x : α} {u : ι → α} {i₀ : ι} (h : ∀ i ≥ i₀, u i = x) : tendsto u at_top (𝓝 x) :=
+tendsto.congr' (eventually_eq.symm (eventually_at_top.mpr ⟨i₀, h⟩)) tendsto_const_nhds
+
+lemma tendsto_at_bot_of_eventually_const {ι : Type*} [semilattice_inf ι] [nonempty ι]
+  {x : α} {u : ι → α} {i₀ : ι} (h : ∀ i ≤ i₀, u i = x) : tendsto u at_bot (𝓝 x) :=
+tendsto.congr' (eventually_eq.symm (eventually_at_bot.mpr ⟨i₀, h⟩)) tendsto_const_nhds
+
 lemma pure_le_nhds : pure ≤ (𝓝 : α → filter α) :=
 assume a s hs, mem_pure_sets.2 $ mem_of_mem_nhds hs