From 01b1576c5d81eb4234e061da9f4cef79a247665f Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 27 Nov 2019 12:34:07 -0500 Subject: [PATCH] feat(topology/algebra/infinite_sum): prove `cauchy_seq_of_edist_le_of_summable` (#1739) * feat(topology/algebra/infinite_sum): prove `cauchy_seq_of_edist_le_of_summable` Other changes: * Add estimates on the distance to the limit (`dist` version only) * Simplify some proofs * Add some supporting lemmas * Fix a typo in a lemma name in `ennreal` * Add `move_cast` attrs * More `*_cast` tags, use `norm_cast` --- src/data/real/ennreal.lean | 46 ++++++---- src/data/real/nnreal.lean | 44 +++++---- src/order/filter/basic.lean | 4 + src/topology/algebra/infinite_sum.lean | 96 ++++++++++++++------ src/topology/metric_space/basic.lean | 13 +++ src/topology/metric_space/emetric_space.lean | 19 ++++ src/topology/uniform_space/cauchy.lean | 5 + 7 files changed, 167 insertions(+), 60 deletions(-) diff --git a/src/data/real/ennreal.lean b/src/data/real/ennreal.lean index b980d0f97318d..ced59e5d5938e 100644 --- a/src/data/real/ennreal.lean +++ b/src/data/real/ennreal.lean @@ -109,22 +109,23 @@ by simp [ennreal.to_real, to_nnreal_eq_zero_iff] @[simp] lemma one_ne_top : 1 ≠ ∞ := coe_ne_top @[simp] lemma top_ne_one : ∞ ≠ 1 := top_ne_coe -@[simp] lemma coe_eq_coe : (↑r : ennreal) = ↑q ↔ r = q := with_top.coe_eq_coe -@[simp] lemma coe_le_coe : (↑r : ennreal) ≤ ↑q ↔ r ≤ q := with_top.coe_le_coe -@[simp] lemma coe_lt_coe : (↑r : ennreal) < ↑q ↔ r < q := with_top.coe_lt_coe +@[simp, elim_cast] lemma coe_eq_coe : (↑r : ennreal) = ↑q ↔ r = q := with_top.coe_eq_coe +@[simp, elim_cast] lemma coe_le_coe : (↑r : ennreal) ≤ ↑q ↔ r ≤ q := with_top.coe_le_coe +@[simp, elim_cast] lemma coe_lt_coe : (↑r : ennreal) < ↑q ↔ r < q := with_top.coe_lt_coe +lemma coe_mono : monotone (coe : nnreal → ennreal) := λ _ _, coe_le_coe.2 -@[simp] lemma coe_eq_zero : (↑r : ennreal) = 0 ↔ r = 0 := coe_eq_coe -@[simp] lemma zero_eq_coe : 0 = (↑r : ennreal) ↔ 0 = r := coe_eq_coe -@[simp] lemma coe_eq_one : (↑r : ennreal) = 1 ↔ r = 1 := coe_eq_coe -@[simp] lemma one_eq_coe : 1 = (↑r : ennreal) ↔ 1 = r := coe_eq_coe -@[simp] lemma coe_nonneg : 0 ≤ (↑r : ennreal) ↔ 0 ≤ r := coe_le_coe -@[simp] lemma coe_pos : 0 < (↑r : ennreal) ↔ 0 < r := coe_lt_coe +@[simp, elim_cast] lemma coe_eq_zero : (↑r : ennreal) = 0 ↔ r = 0 := coe_eq_coe +@[simp, elim_cast] lemma zero_eq_coe : 0 = (↑r : ennreal) ↔ 0 = r := coe_eq_coe +@[simp, elim_cast] lemma coe_eq_one : (↑r : ennreal) = 1 ↔ r = 1 := coe_eq_coe +@[simp, elim_cast] lemma one_eq_coe : 1 = (↑r : ennreal) ↔ 1 = r := coe_eq_coe +@[simp, elim_cast] lemma coe_nonneg : 0 ≤ (↑r : ennreal) ↔ 0 ≤ r := coe_le_coe +@[simp, elim_cast] lemma coe_pos : 0 < (↑r : ennreal) ↔ 0 < r := coe_lt_coe -@[simp] lemma coe_add : ↑(r + p) = (r + p : ennreal) := with_top.coe_add -@[simp] lemma coe_mul : ↑(r * p) = (r * p : ennreal) := with_top.coe_mul +@[simp, move_cast] lemma coe_add : ↑(r + p) = (r + p : ennreal) := with_top.coe_add +@[simp, move_cast] lemma coe_mul : ↑(r * p) = (r * p : ennreal) := with_top.coe_mul -@[simp] lemma coe_bit0 : (↑(bit0 r) : ennreal) = bit0 r := coe_add -@[simp] lemma coe_bit1 : (↑(bit1 r) : ennreal) = bit1 r := by simp [bit1] +@[simp, move_cast] lemma coe_bit0 : (↑(bit0 r) : ennreal) = bit0 r := coe_add +@[simp, move_cast] lemma coe_bit1 : (↑(bit1 r) : ennreal) = bit1 r := by simp [bit1] @[simp] lemma add_top : a + ∞ = ∞ := with_top.add_top @[simp] lemma top_add : ∞ + a = ∞ := with_top.top_add @@ -132,6 +133,9 @@ by simp [ennreal.to_real, to_nnreal_eq_zero_iff] instance : is_semiring_hom (coe : nnreal → ennreal) := by refine_struct {..}; simp +@[simp, move_cast] lemma coe_pow (n : ℕ) : (↑(r^n) : ennreal) = r^n := +is_monoid_hom.map_pow coe r n + lemma add_eq_top : a + b = ∞ ↔ a = ∞ ∨ b = ∞ := with_top.add_eq_top _ _ lemma add_lt_top : a + b < ∞ ↔ a < ∞ ∧ b < ∞ := with_top.add_lt_top _ _ @@ -164,10 +168,12 @@ with_top.mul_eq_top_iff lemma mul_lt_top {a b : ennreal} : a < ⊤ → b < ⊤ → a * b < ⊤ := by simp [ennreal.lt_top_iff_ne_top, (≠), mul_eq_top] {contextual := tt} -@[simp] lemma coe_finset_sum {s : finset α} {f : α → nnreal} : ↑(s.sum f) = (s.sum (λa, f a) : ennreal) := +@[simp, move_cast] lemma coe_finset_sum {s : finset α} {f : α → nnreal} : + ↑(s.sum f) = (s.sum (λa, f a) : ennreal) := (finset.sum_hom coe).symm -@[simp] lemma coe_finset_prod {s : finset α} {f : α → nnreal} : ↑(s.prod f) = (s.prod (λa, f a) : ennreal) := +@[simp, move_cast] lemma coe_finset_prod {s : finset α} {f : α → nnreal} : + ↑(s.prod f) = (s.prod (λa, f a) : ennreal) := (finset.prod_hom coe).symm @[simp] lemma bot_eq_zero : (⊥ : ennreal) = 0 := rfl @@ -179,7 +185,7 @@ section order @[simp] lemma one_le_coe_iff : (1:ennreal) ≤ ↑r ↔ 1 ≤ r := coe_le_coe @[simp] lemma coe_le_one_iff : ↑r ≤ (1:ennreal) ↔ r ≤ 1 := coe_le_coe @[simp] lemma coe_lt_one_iff : (↑p : ennreal) < 1 ↔ p < 1 := coe_lt_coe -@[simp] lemma one_lt_zero_iff : 1 < (↑p : ennreal) ↔ 1 < p := coe_lt_coe +@[simp] lemma one_lt_coe_iff : 1 < (↑p : ennreal) ↔ 1 < p := coe_lt_coe @[simp] lemma coe_nat (n : nat) : ((n : nnreal) : ennreal) = n := with_top.coe_nat n @[simp] lemma nat_ne_top (n : nat) : (n : ennreal) ≠ ⊤ := with_top.nat_ne_top n @[simp] lemma top_ne_nat (n : nat) : (⊤ : ennreal) ≠ n := with_top.top_ne_nat n @@ -255,6 +261,12 @@ begin apply lt_of_lt_of_le I J end +@[move_cast] lemma coe_min : ((min r p:nnreal):ennreal) = min r p := +coe_mono.map_min + +@[move_cast] lemma coe_max : ((max r p:nnreal):ennreal) = max r p := +coe_mono.map_max + end order section complete_lattice @@ -301,7 +313,7 @@ end mul section sub instance : has_sub ennreal := ⟨λa b, Inf {d | a ≤ d + b}⟩ -lemma coe_sub : ↑(p - r) = (↑p:ennreal) - r := +@[move_cast] lemma coe_sub : ↑(p - r) = (↑p:ennreal) - r := le_antisymm (le_Inf $ assume b (hb : ↑p ≤ b + r), coe_le_iff.2 $ by rintros d rfl; rwa [← coe_add, coe_le_coe, ← nnreal.sub_le_iff_le_add] at hb) diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean index 54583971f9b28..3b450f8205f6e 100644 --- a/src/data/real/nnreal.lean +++ b/src/data/real/nnreal.lean @@ -53,11 +53,11 @@ instance : inhabited ℝ≥0 := ⟨0⟩ @[simp] protected lemma coe_zero : ((0 : ℝ≥0) : ℝ) = 0 := rfl @[simp] protected lemma coe_one : ((1 : ℝ≥0) : ℝ) = 1 := rfl @[simp] protected lemma coe_add (r₁ r₂ : ℝ≥0) : ((r₁ + r₂ : ℝ≥0) : ℝ) = r₁ + r₂ := rfl -@[simp] protected lemma coe_mul (r₁ r₂ : ℝ≥0) : ((r₁ * r₂ : ℝ≥0) : ℝ) = r₁ * r₂ := rfl -@[simp] protected lemma coe_div (r₁ r₂ : ℝ≥0) : ((r₁ / r₂ : ℝ≥0) : ℝ) = r₁ / r₂ := rfl -@[simp] protected lemma coe_inv (r : ℝ≥0) : ((r⁻¹ : ℝ≥0) : ℝ) = r⁻¹ := rfl +@[simp, move_cast] protected lemma coe_mul (r₁ r₂ : ℝ≥0) : ((r₁ * r₂ : ℝ≥0) : ℝ) = r₁ * r₂ := rfl +@[simp, move_cast] protected lemma coe_div (r₁ r₂ : ℝ≥0) : ((r₁ / r₂ : ℝ≥0) : ℝ) = r₁ / r₂ := rfl +@[simp, move_cast] protected lemma coe_inv (r : ℝ≥0) : ((r⁻¹ : ℝ≥0) : ℝ) = r⁻¹ := rfl -@[simp] protected lemma coe_sub (r₁ r₂ : ℝ≥0) (h : r₂ ≤ r₁) : ((r₁ - r₂ : ℝ≥0) : ℝ) = r₁ - r₂ := +@[simp] protected lemma coe_sub {r₁ r₂ : ℝ≥0} (h : r₂ ≤ r₁) : ((r₁ - r₂ : ℝ≥0) : ℝ) = r₁ - r₂ := max_eq_left $ le_sub.2 $ by simp [show (r₂ : ℝ) ≤ r₁, from h] -- TODO: setup semifield! @@ -75,19 +75,22 @@ end instance : is_semiring_hom (coe : ℝ≥0 → ℝ) := by refine_struct {..}; intros; refl -lemma sum_coe {α} {s : finset α} {f : α → ℝ≥0} : ↑(s.sum f) = s.sum (λa, (f a : ℝ)) := +@[move_cast] lemma coe_pow (r : ℝ≥0) (n : ℕ) : ((r^n : ℝ≥0) : ℝ) = r^n := +is_monoid_hom.map_pow coe r n + +@[move_cast] lemma sum_coe {α} {s : finset α} {f : α → ℝ≥0} : + ↑(s.sum f) = s.sum (λa, (f a : ℝ)) := eq.symm $ finset.sum_hom _ -lemma prod_coe {α} {s : finset α} {f : α → ℝ≥0} : ↑(s.prod f) = s.prod (λa, (f a : ℝ)) := +@[move_cast] lemma prod_coe {α} {s : finset α} {f : α → ℝ≥0} : + ↑(s.prod f) = s.prod (λa, (f a : ℝ)) := eq.symm $ finset.prod_hom _ -lemma smul_coe (r : ℝ≥0) : ∀n, ↑(add_monoid.smul n r) = add_monoid.smul n (r:ℝ) -| 0 := rfl -| (n + 1) := by simp [add_monoid.add_smul, smul_coe n] +@[move_cast] lemma smul_coe (r : ℝ≥0) (n : ℕ) : ↑(add_monoid.smul n r) = add_monoid.smul n (r:ℝ) := +is_add_monoid_hom.map_smul coe r n -@[simp] protected lemma coe_nat_cast : ∀(n : ℕ), (↑(↑n : ℝ≥0) : ℝ) = n -| 0 := rfl -| (n + 1) := by simp [coe_nat_cast n] +@[simp, squash_cast] protected lemma coe_nat_cast (n : ℕ) : (↑(↑n : ℝ≥0) : ℝ) = n := +is_semiring_hom.map_nat_cast coe n instance : decidable_linear_order ℝ≥0 := decidable_linear_order.lift (coe : ℝ≥0 → ℝ) subtype.val_injective (by apply_instance) @@ -95,6 +98,7 @@ decidable_linear_order.lift (coe : ℝ≥0 → ℝ) subtype.val_injective (by ap @[elim_cast] protected lemma coe_le {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) ≤ r₂ ↔ r₁ ≤ r₂ := iff.rfl @[elim_cast] protected lemma coe_lt {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) < r₂ ↔ r₁ < r₂ := iff.rfl @[elim_cast] protected lemma coe_pos {r : ℝ≥0} : (0 : ℝ) < r ↔ 0 < r := iff.rfl +@[elim_cast] protected lemma coe_eq {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) = r₂ ↔ r₁ = r₂ := subtype.ext.symm protected lemma coe_mono : monotone (coe : ℝ≥0 → ℝ) := λ _ _, nnreal.coe_le.2 @@ -332,21 +336,26 @@ end mul section sub +lemma sub_def {r p : ℝ≥0} : r - p = nnreal.of_real (r - p) := rfl + lemma sub_eq_zero {r p : nnreal} (h : r ≤ p) : r - p = 0 := nnreal.eq $ max_eq_right $ sub_le_iff_le_add.2 $ by simpa [nnreal.coe_le] using h +lemma sub_pos {r p : ℝ≥0} : 0 < r - p ↔ p < r := +of_real_pos.trans $ sub_pos.trans $ nnreal.coe_lt + protected lemma sub_lt_self {r p : nnreal} : 0 < r → 0 < p → r - p < r := assume hr hp, begin cases le_total r p, { rwa [sub_eq_zero h] }, - { rw [← nnreal.coe_lt, nnreal.coe_sub _ _ h], exact sub_lt_self _ hp } + { rw [← nnreal.coe_lt, nnreal.coe_sub h], exact sub_lt_self _ hp } end @[simp] lemma sub_le_iff_le_add {r p q : nnreal} : r - p ≤ q ↔ r ≤ q + p := match le_total p r with | or.inl h := - by rw [← nnreal.coe_le, ← nnreal.coe_le, nnreal.coe_sub _ _ h, nnreal.coe_add, sub_le_iff_le_add] + by rw [← nnreal.coe_le, ← nnreal.coe_le, nnreal.coe_sub h, nnreal.coe_add, sub_le_iff_le_add] | or.inr h := have r ≤ p + q, from le_add_right h, by simpa [nnreal.coe_le, nnreal.coe_le, sub_eq_zero h] @@ -359,7 +368,7 @@ lemma add_sub_cancel' {r p : nnreal} : (r + p) - r = p := by rw [add_comm, add_sub_cancel] @[simp] lemma sub_add_cancel_of_le {a b : nnreal} (h : b ≤ a) : (a - b) + b = a := -nnreal.eq $ by rw [nnreal.coe_add, nnreal.coe_sub _ _ h, sub_add_cancel] +nnreal.eq $ by rw [nnreal.coe_add, nnreal.coe_sub h, sub_add_cancel] end sub @@ -395,10 +404,13 @@ by rw [← mul_le_mul_left (zero_lt_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm @[simp] lemma lt_inv_iff_mul_lt {r p : ℝ≥0} (h : p ≠ 0) : (r < p⁻¹ ↔ r * p < 1) := by rw [← mul_lt_mul_left (zero_lt_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm] -lemma mul_le_if_le_inv {a b r : nnreal} (hr : r ≠ 0) : r * a ≤ b ↔ a ≤ r⁻¹ * b := +lemma mul_le_iff_le_inv {a b r : ℝ≥0} (hr : r ≠ 0) : r * a ≤ b ↔ a ≤ r⁻¹ * b := have 0 < r, from lt_of_le_of_ne (zero_le r) hr.symm, by rw [← @mul_le_mul_left _ _ a _ r this, ← mul_assoc, mul_inv_cancel hr, one_mul] +lemma le_div_iff_mul_le {a b r : ℝ≥0} (hr : r ≠ 0) : a ≤ b / r ↔ a * r ≤ b := +by rw [div_def, mul_comm, ← mul_le_iff_le_inv hr, mul_comm] + lemma le_of_forall_lt_one_mul_lt {x y : ℝ≥0} (h : ∀a<1, a * x ≤ y) : x ≤ y := le_of_forall_ge_of_dense $ assume a ha, have hx : x ≠ 0 := zero_lt_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha), diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean index 1e1ad203f89c6..6030aaa21d927 100644 --- a/src/order/filter/basic.lean +++ b/src/order/filter/basic.lean @@ -1578,6 +1578,10 @@ lemma tendsto_at_top_at_top_of_monotone [nonempty α] [semilattice_sup α] [preo alias tendsto_at_top_at_top_of_monotone ← monotone.tendsto_at_top_at_top +lemma tendsto_finset_range : tendsto finset.range at_top at_top := +(tendsto_at_top_at_top _).2 (λ s, ⟨s.sup id + 1, λ N hN n hn, + finset.mem_range.2 $ lt_of_le_of_lt (finset.le_sup hn) $ nat.lt_of_succ_le hN⟩) + lemma tendsto_finset_image_at_top_at_top {i : β → γ} {j : γ → β} (h : ∀x, j (i x) = x) : tendsto (λs:finset γ, s.image j) at_top at_top := tendsto_infi.2 $ assume s, tendsto_infi' (s.image i) $ tendsto_principal_principal.2 $ diff --git a/src/topology/algebra/infinite_sum.lean b/src/topology/algebra/infinite_sum.lean index f3f81925e65f3..3be6d9e94f72d 100644 --- a/src/topology/algebra/infinite_sum.lean +++ b/src/topology/algebra/infinite_sum.lean @@ -124,11 +124,7 @@ show tendsto (λs:finset β, s.sum (g ∘ f)) at_top (𝓝 (g a)), /-- If `f : ℕ → α` has sum `a`, then the partial sums `∑_{i=0}^{n-1} f i` converge to `a`. -/ lemma tendsto_sum_nat_of_has_sum {f : ℕ → α} (h : has_sum f a) : tendsto (λn:ℕ, (range n).sum f) at_top (𝓝 a) := -suffices map (λ (n : ℕ), sum (range 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), -let ⟨t, ht⟩ := mem_at_top_sets.mp hs, ⟨n, hn⟩ := @exists_nat_subset_range t in -mem_at_top_sets.mpr ⟨n, assume n' hn', ht _ $ finset.subset.trans hn $ range_subset.mpr hn'⟩ +@tendsto.comp _ _ _ finset.range (λ s : finset ℕ, s.sum f) _ _ _ h tendsto_finset_range variable [topological_add_monoid α] @@ -490,15 +486,8 @@ end lemma sum_le_has_sum {f : β → α} (s : finset β) (hs : ∀ b∉s, 0 ≤ f b) (hf : has_sum f a) : s.sum f ≤ a := -let f' := λ b, if b ∈ s then f b else 0 in -have hf' : has_sum f' (s.sum f'), - from has_sum_sum_of_ne_finset_zero $ λ b hb, if_neg hb, -have hle : ∀ b, f' b ≤ f b, - from λ b, if hb : b ∈ s - then by simp only [f', if_pos hb] - else by simp only [f', if_neg hb, hs b hb], -calc s.sum f = s.sum f' : finset.sum_congr rfl $ λ b hb, (if_pos hb).symm -... ≤ a : has_sum_le hle hf' hf +ge_of_tendsto at_top_ne_bot hf (mem_at_top_sets.2 ⟨s, λ t hst, + sum_le_sum_of_subset_of_nonneg hst $ λ b hbt hbs, hs b hbs⟩) lemma sum_le_tsum {f : β → α} (s : finset β) (hs : ∀ b∉s, 0 ≤ f b) (hf : summable f) : s.sum f ≤ tsum f := @@ -582,22 +571,75 @@ end uniform_group section cauchy_seq open finset.Ico filter +/-- If the extended distance between consequent points of a sequence is estimated +by a summable series of `nnreal`s, then the original sequence is a Cauchy sequence. -/ +lemma cauchy_seq_of_edist_le_of_summable [emetric_space α] {f : ℕ → α} (d : ℕ → nnreal) + (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) (hd : summable d) : cauchy_seq f := +begin + refine emetric.cauchy_seq_iff_nnreal.2 (λ ε εpos, _), + -- Actually we need partial sums of `d` to be a Cauchy sequence + replace hd : cauchy_seq (λ (n : ℕ), sum (range n) d) := + let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ (tendsto_sum_nat_of_has_sum H), + -- Now we take the same `N` as in one of the definitions of a Cauchy sequence + refine (metric.cauchy_seq_iff'.1 hd ε (nnreal.coe_pos.2 εpos)).imp (λ N hN n hn, _), + have hsum := hN n hn, + -- We simplify the known inequality + rw [dist_nndist, nnreal.nndist_eq, ← sum_range_add_sum_Ico _ hn, nnreal.add_sub_cancel'] at hsum, + norm_cast at hsum, + replace hsum := lt_of_le_of_lt (le_max_left _ _) hsum, + + -- Then use `hf` to simplify the goal to the same form + apply lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn (λ k _ _, hf k)), + assumption_mod_cast +end + +/-- If the distance between consequent points of a sequence is estimated by a summable series, +then the original sequence is a Cauchy sequence. -/ +lemma cauchy_seq_of_dist_le_of_summable [metric_space α] {f : ℕ → α} (d : ℕ → ℝ) + (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) : cauchy_seq f := +begin + refine metric.cauchy_seq_iff'.2 (λε εpos, _), + replace hd : cauchy_seq (λ (n : ℕ), sum (range n) d) := + let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ (tendsto_sum_nat_of_has_sum H), + refine (metric.cauchy_seq_iff'.1 hd ε εpos).imp (λ N hN n hn, _), + have hsum := hN n hn, + rw [real.dist_eq, ← sum_Ico_eq_sub _ hn] at hsum, + calc dist (f n) (f N) = dist (f N) (f n) : dist_comm _ _ + ... ≤ (Ico N n).sum d : dist_le_Ico_sum_of_dist_le hn (λ k _ _, hf k) + ... ≤ abs ((Ico N n).sum d) : le_abs_self _ + ... < ε : hsum +end + lemma cauchy_seq_of_summable_dist [metric_space α] {f : ℕ → α} (h : summable (λn, dist (f n) (f n.succ))) : cauchy_seq f := +cauchy_seq_of_dist_le_of_summable _ (λ _, le_refl _) h + +lemma dist_le_tsum_of_dist_le_of_tendsto [metric_space α] {f : ℕ → α} (d : ℕ → ℝ) + (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) {a : α} (ha : tendsto f at_top (𝓝 a)) + (n : ℕ) : + dist (f n) a ≤ ∑ m, d (n + m) := begin - let d := λn, dist (f n) (f (n+1)), - refine metric.cauchy_seq_iff'.2 (λε εpos, _), - rcases (summable_iff_vanishing _).1 h {x : ℝ | x < ε} (gt_mem_nhds εpos) with ⟨s, hs⟩, - have : ∃N:ℕ, ∀x ∈ s, x < N, - { by_cases h : s = ∅, - { use 0, simp [h]}, - { use s.max' h + 1, - exact λx hx, lt_of_le_of_lt (s.le_max' h x hx) (nat.lt_succ_self _) }}, - rcases this with ⟨N, hN⟩, - refine ⟨N, λn hn, _⟩, - calc dist (f n) (f N) ≤ (Ico N n).sum d : by rw dist_comm; apply dist_le_Ico_sum_dist f hn - ... < ε : hs _ (finset.disjoint_iff_ne.2 - (λa ha b hb, ne_of_gt (lt_of_lt_of_le (hN _ hb) (mem.1 ha).1))) + refine le_of_tendsto at_top_ne_bot (tendsto_dist tendsto_const_nhds ha) + (mem_at_top_sets.2 ⟨n, λ m hnm, _⟩), + refine le_trans (dist_le_Ico_sum_of_dist_le hnm (λ k _ _, hf k)) _, + rw [sum_Ico_eq_sum_range], + refine sum_le_tsum (range _) (λ _ _, le_trans dist_nonneg (hf _)) _, + exact summable_comp_of_summable_of_injective _ hd (add_left_injective n) end +lemma dist_le_tsum_of_dist_le_of_tendsto₀ [metric_space α] {f : ℕ → α} (d : ℕ → ℝ) + (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) {a : α} (ha : tendsto f at_top (𝓝 a)) : + dist (f 0) a ≤ tsum d := +by simpa only [zero_add] using dist_le_tsum_of_dist_le_of_tendsto d hf hd ha 0 + +lemma dist_le_tsum_dist_of_tendsto [metric_space α] {f : ℕ → α} + (h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) (n) : + dist (f n) a ≤ ∑ m, dist (f (n+m)) (f (n+m).succ) := +dist_le_tsum_of_dist_le_of_tendsto (λ n, dist (f n) (f n.succ)) (λ _, le_refl _) h ha n + +lemma dist_le_tsum_dist_of_tendsto₀ [metric_space α] {f : ℕ → α} + (h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) : + dist (f 0) a ≤ ∑ n, dist (f n) (f n.succ) := +by simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0 + end cauchy_seq diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean index 6b5984ff10544..434578223d159 100644 --- a/src/topology/metric_space/basic.lean +++ b/src/topology/metric_space/basic.lean @@ -767,6 +767,19 @@ section nnreal instance : metric_space nnreal := by unfold nnreal; apply_instance +lemma nnreal.dist_eq (a b : nnreal) : dist a b = abs ((a:ℝ) - b) := rfl + +lemma nnreal.nndist_eq (a b : nnreal) : + nndist a b = max (a - b) (b - a) := +begin + wlog h : a ≤ b, + { apply nnreal.coe_eq.1, + rw [nnreal.sub_eq_zero h, max_eq_right (zero_le $ b - a), ← dist_nndist, nnreal.dist_eq, + nnreal.coe_sub h, abs, neg_sub], + apply max_eq_right, + linarith [nnreal.coe_le.2 h] }, + rwa [nndist_comm, max_comm] +end end nnreal section prod diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean index 80f80121fc9c8..03f5963a47471 100644 --- a/src/topology/metric_space/emetric_space.lean +++ b/src/topology/metric_space/emetric_space.lean @@ -559,6 +559,25 @@ begin ... = ε : ennreal.add_halves _⟩ } end +/-- A variation of the emetric characterization of Cauchy sequences that deals with +`nnreal` upper bounds. -/ +theorem cauchy_seq_iff_nnreal [inhabited β] [semilattice_sup β] {u : β → α} : + cauchy_seq u ↔ ∀ ε : nnreal, 0 < ε → ∃ N, ∀ n, N ≤ n → edist (u N) (u n) < ε := +begin + refine cauchy_seq_iff'.trans + ⟨λ H ε εpos, (H ε (ennreal.coe_pos.2 εpos)).imp $ + λ N hN n hn, edist_comm (u n) (u N) ▸ hN n hn, + λ H ε εpos, _⟩, + specialize H ((min 1 ε).to_nnreal) + (ennreal.to_nnreal_pos_iff.2 ⟨lt_min ennreal.zero_lt_one εpos, + ennreal.lt_top_iff_ne_top.1 $ min_lt_iff.2 $ or.inl ennreal.coe_lt_top⟩), + refine H.imp (λ N hN n hn, edist_comm (u N) (u n) ▸ lt_of_lt_of_le (hN n hn) _), + refine ennreal.coe_le_iff.2 _, + rintros ε rfl, + rw [← ennreal.coe_one, ← ennreal.coe_min, ennreal.to_nnreal_coe], + apply min_le_right +end + theorem totally_bounded_iff {s : set α} : totally_bounded s ↔ ∀ ε > 0, ∃t : set α, finite t ∧ s ⊆ ⋃y∈t, ball y ε := ⟨λ H ε ε0, H _ (edist_mem_uniformity ε0), diff --git a/src/topology/uniform_space/cauchy.lean b/src/topology/uniform_space/cauchy.lean index 3a994028f0f8f..cb8d3b5544af4 100644 --- a/src/topology/uniform_space/cauchy.lean +++ b/src/topology/uniform_space/cauchy.lean @@ -113,6 +113,11 @@ defined on ℝ is Cauchy at +∞ to deduce convergence. Therefore, we define it is general enough to cover both ℕ and ℝ, which are the main motivating examples. -/ def cauchy_seq [semilattice_sup β] (u : β → α) := cauchy (at_top.map u) +lemma cauchy_seq_of_tendsto_nhds [semilattice_sup β] [nonempty β] (f : β → α) {x} + (hx : tendsto f at_top (𝓝 x)) : + cauchy_seq f := +cauchy_downwards cauchy_nhds (map_ne_bot at_top_ne_bot) hx + lemma cauchy_seq_iff_prod_map [inhabited β] [semilattice_sup β] {u : β → α} : cauchy_seq u ↔ map (prod.map u u) at_top ≤ 𝓤 α := iff.trans (and_iff_right (map_ne_bot at_top_ne_bot)) (prod_map_at_top_eq u u ▸ iff.rfl)