feat(data/real/cau_seq): relate cauchy sequence completeness and filt…

…er completeness

algebra/archimedean.lean

@@ -235,6 +235,18 @@ begin
        ← div_lt_iff' (sub_pos.2 h), one_div_eq_inv]
 end
 
+theorem exists_nat_one_div_lt {ε : α} (hε : ε > 0) : ∃ n : ℕ, 1 / (n + 1: α) < ε :=
+begin
+  cases archimedean_iff_nat_lt.1 (by apply_instance) (1/ε) with n hn,
+  existsi n,
+  apply div_lt_of_mul_lt_of_pos,
+  { simp, apply add_pos_of_pos_of_nonneg zero_lt_one, apply nat.cast_nonneg },
+  { apply (div_lt_iff' hε).1,
+    transitivity,
+    { exact hn },
+    { simp [zero_lt_one] }}
+end
+
 include α
 @[simp] theorem rat.cast_floor (x : ℚ) :
   by haveI := archimedean.floor_ring α; exact ⌊(x:α)⌋ = ⌊x⌋ :=

algebra/field_power.lean

@@ -6,7 +6,7 @@ Authors: Robert Y. Lewis
 Integer power operation on fields.
 -/
 
-import algebra.group_power tactic.wlog tactic.find
+import algebra.group_power tactic.wlog
 
 universe u
 

analysis/limits.lean

@@ -144,6 +144,11 @@ tendsto_coe_iff.1 $
   have hr : (k : ℝ) > 1, from show (k : ℝ) > (1 : ℕ), from nat.cast_lt.2 h,
   by simpa using tendsto_pow_at_top_at_top_of_gt_1 hr
 
+lemma tendsto_inverse_at_top_nhds_0_nat : tendsto (λ n : ℕ, (n : ℝ)⁻¹) at_top (nhds 0) :=
+tendsto.comp (tendsto_coe_iff.2 tendsto_id) tendsto_inverse_at_top_nhds_0
+
+lemma tendsto_one_div_at_top_nhds_0_nat : tendsto (λ n : ℕ, 1/(n : ℝ)) at_top (nhds 0) :=
+by simpa only [inv_eq_one_div] using tendsto_inverse_at_top_nhds_0_nat
 
 lemma sum_geometric' {r : ℝ} (h : r ≠ 0) :
   ∀{n}, (finset.range n).sum (λi, (r + 1) ^ i) = ((r + 1) ^ n - 1) / r

data/padics/padic_integers.lean

@@ -6,7 +6,9 @@ Authors: Robert Y. Lewis
 Define the p-adic integers ℤ_p as a subtype of ℚ_p. Construct algebraic structures on ℤ_p.
 -/
 
-import data.padics.padic_numbers tactic.subtype_instance ring_theory.ideals data.int.modeq
+import data.padics.padic_numbers ring_theory.ideals data.int.modeq
+import tactic.linarith tactic.subtype_instance
+
 open nat padic
 noncomputable theory
 local attribute [instance] classical.prop_decidable
@@ -275,19 +277,19 @@ private def cau_seq_to_rat_cau_seq (f : cau_seq ℤ_[hp] norm) :
 ⟨ λ n, f n,
   λ _ hε, by simpa [norm, padic_norm_z] using f.cauchy hε ⟩
 
-theorem complete (f : cau_seq ℤ_[hp] norm) :
+protected theorem complete (f : cau_seq ℤ_[hp] norm) :
   ∃ z : ℤ_[hp], ∀ ε > 0, ∃ N, ∀ i ≥ N, ∥z - f i∥ < ε :=
 have hqn : ∥padic.cau_seq_lim (cau_seq_to_rat_cau_seq f)∥ ≤ 1,
   from padic_norm_e_lim_le zero_lt_one (λ _, padic_norm_z.le_one _),
 ⟨ ⟨_, hqn⟩,
   by simpa [norm, padic_norm_z] using padic.cau_seq_lim_spec (cau_seq_to_rat_cau_seq f) ⟩
 
-def cau_seq_lim (f : cau_seq ℤ_[hp] norm) : ℤ_[hp] := classical.some (complete f)
+def cau_seq_lim (f : cau_seq ℤ_[hp] norm) : ℤ_[hp] := classical.some (padic_int.complete f)
 
 lemma cau_seq_lim_spec (f : cau_seq ℤ_[hp] norm) : ∀ ε > 0, ∃ N, ∀ i ≥ N, ∥cau_seq_lim f - f i∥ < ε :=
-classical.some_spec (complete f)
+classical.some_spec (padic_int.complete f)
 
-open filter
+open set filter
 lemma tendsto_limit (f : cau_seq ℤ_[hp] norm) : tendsto f at_top (nhds (cau_seq_lim f)) :=
 tendsto_nhds
 begin

data/padics/padic_numbers.lean

@@ -7,7 +7,8 @@ Define the p-adic numbers (rationals) ℚ_p as the completion of ℚ wrt the p-a
 Show that the p-adic norm extends to ℚ_p, that ℚ is embedded in ℚ_p, and that ℚ_p is complete
 -/
 
-import data.real.cau_seq_completion data.padics.padic_norm algebra.archimedean analysis.normed_space
+import data.real.cau_seq_completion data.real.cau_seq_filter
+import data.padics.padic_norm algebra.archimedean analysis.normed_space
 noncomputable theory
 local attribute [instance, priority 1] classical.prop_decidable
 
@@ -719,7 +720,7 @@ end padic_norm_e
 namespace padic
 variables {p : ℕ} {hp : p.prime}
 
-protected theorem complete (f : cau_seq ℚ_[hp] (λ a, ∥a∥)):
+protected theorem complete (f : cau_seq ℚ_[hp] norm):
         ∃ q : ℚ_[hp], ∀ ε > 0, ∃ N, ∀ i ≥ N, ∥q - f i∥ < ε :=
 let f' : cau_seq ℚ_[hp] padic_norm_e :=
   ⟨λ n, f n, λ ε hε,
@@ -730,14 +731,14 @@ let ⟨q, hq⟩ := padic.complete' f' in
       ⟨N, hN⟩ := hq _ (by simpa using hε'l) in
   ⟨N, λ i hi, lt.trans (rat.cast_lt.2 (hN _ hi)) hε'r ⟩⟩
 
-def cau_seq_lim (f : cau_seq ℚ_[hp] (λ a, ∥a∥)) : ℚ_[hp] :=
+def cau_seq_lim (f : cau_seq ℚ_[hp] norm) : ℚ_[hp] :=
 classical.some (padic.complete f)
 
-lemma cau_seq_lim_spec (f : cau_seq ℚ_[hp] (λ a, ∥a∥)) :
+lemma cau_seq_lim_spec (f : cau_seq ℚ_[hp] norm) :
       ∀ ε > 0, ∃ N, ∀ i ≥ N, ∥(cau_seq_lim f) - f i∥ < ε :=
 classical.some_spec (padic.complete f)
 
-lemma padic_norm_e_lim_le {f : cau_seq ℚ_[hp] (λ a, ∥a∥)} {a : ℝ} (ha : a > 0)
+lemma padic_norm_e_lim_le {f : cau_seq ℚ_[hp] norm} {a : ℝ} (ha : a > 0)
       (hf : ∀ i, ∥f i∥ ≤ a) : ∥cau_seq_lim f∥ ≤ a :=
 let ⟨N, hN⟩ := cau_seq_lim_spec f _ ha in
 calc ∥cau_seq_lim f∥ = ∥cau_seq_lim f - f N + f N∥ : by simp
@@ -759,4 +760,6 @@ begin
   solve_by_elim
 end
 
+instance : complete_space ℚ_[hp] := complete_space_of_cauchy_complete padic.complete
+
 end padic

data/real/cau_seq_completion.lean

@@ -3,20 +3,20 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Robert Y. Lewis
 
-Generalizes the Cauchy completion of (ℚ, abs) to the completion of a 
-commutative ring with absolute value. 
+Generalizes the Cauchy completion of (ℚ, abs) to the completion of a
+commutative ring with absolute value.
 -/
 
 import data.real.cau_seq
 
-namespace cau_seq.completion 
+namespace cau_seq.completion
 open cau_seq
 
 section
 parameters {α : Type*} [discrete_linear_ordered_field α]
 parameters {β : Type*} [comm_ring β] {abv : β → α} [is_absolute_value abv]
 
-def Cauchy := @quotient (cau_seq _ abv) cau_seq.equiv 
+def Cauchy := @quotient (cau_seq _ abv) cau_seq.equiv
 
 def mk : cau_seq _ abv → Cauchy := quotient.mk
 
@@ -112,13 +112,13 @@ congr_arg mk $ by rw dif_pos; [refl, exact zero_lim_zero]
 @[simp] theorem inv_mk {f} (hf) : (@mk α _ β _ abv _ f)⁻¹ = mk (inv f hf) :=
 congr_arg mk $ by rw dif_neg
 
-lemma cau_seq_zero_ne_one : ¬ (0 : cau_seq _ abv) ≈ 1 := λ h, 
+lemma cau_seq_zero_ne_one : ¬ (0 : cau_seq _ abv) ≈ 1 := λ h,
 have lim_zero (1 - 0), from setoid.symm h,
 have lim_zero 1, by simpa,
-one_ne_zero $ const_lim_zero.1 this 
+one_ne_zero $ const_lim_zero.1 this
 
 lemma zero_ne_one : (0 : Cauchy) ≠ 1 :=
-λ h, cau_seq_zero_ne_one $ mk_eq.1 h 
+λ h, cau_seq_zero_ne_one $ mk_eq.1 h
 
 
 protected theorem inv_mul_cancel {x : Cauchy} : x ≠ 0 → x⁻¹ * x = 1 :=
@@ -144,5 +144,5 @@ congr_arg mk $ by split_ifs with h; try {simp [const_lim_zero.1 h]}; refl
 theorem of_rat_div (x y : β) : of_rat (x / y) = (of_rat x / of_rat y : Cauchy) :=
 by simp only [div_eq_inv_mul, of_rat_inv, of_rat_mul]
 
-end 
+end
 end cau_seq.completion

data/real/cau_seq_filter.lean

@@ -6,11 +6,11 @@ Authors: Robert Y. Lewis
 Reconcile the filter notion of Cauchy-ness with the cau_seq notion on normed spaces.
 -/
 
-import analysis.topology.uniform_space analysis.normed_space data.real.cau_seq
-section
+import analysis.topology.uniform_space analysis.normed_space data.real.cau_seq analysis.limits
+import tactic.linarith
 
-variables
-  {β : Type*} [normed_field β]
+section
+variables {β : Type*} [normed_field β]
 
 instance normed_field.is_absolute_value : is_absolute_value (norm : β → ℝ) :=
 { abv_nonneg := norm_nonneg,
@@ -54,5 +54,181 @@ begin
   { apply_instance }
 end
 
+end
+
+section
+/-
+ This section shows that if we have a uniform space generated by an absolute value, topological
+ completeness and Cauchy sequence completeness coincide. The problem is that there isn't
+ a good notion of "uniform space generated by an absolute value", so right now this is
+ specific to norm. Furthermore, norm only instantiates is_absolute_value on normed_field.
+
+ This needs to be fixed, since it prevents showing that ℤ_[hp] is complete
+-/
+
+variables {β : Type*} [normed_field β] {f : filter β} (hf : cauchy f)
+open set filter classical
+
+private lemma one_div_succ (n : ℕ) : 1 / ((n : ℝ) + 1) > 0 :=
+one_div_pos_of_pos (by linarith using [show (↑n : ℝ) ≥ 0, from nat.cast_nonneg _])
+
+def set_seq_of_cau_filter : ℕ → set β
+| 0 := some ((cauchy_of_metric.1 hf).2 _ (one_div_succ 0))
+| (n+1) := (set_seq_of_cau_filter n) ∩ some ((cauchy_of_metric.1 hf).2 _ (one_div_succ (n + 1)))
+
+lemma set_seq_of_cau_filter_mem_sets : ∀ n, set_seq_of_cau_filter hf n ∈ f.sets
+| 0 := some (some_spec ((cauchy_of_metric.1 hf).2 _ (one_div_succ 0)))
+| (n+1) := inter_mem_sets (set_seq_of_cau_filter_mem_sets n)
+             (some (some_spec ((cauchy_of_metric.1 hf).2 _ (one_div_succ (n + 1)))))
+
+lemma set_seq_of_cau_filter_inhabited (n : ℕ) : ∃ x, x ∈ set_seq_of_cau_filter hf n :=
+inhabited_of_mem_sets (cauchy_of_metric.1 hf).1 (set_seq_of_cau_filter_mem_sets hf n)
+
+lemma set_seq_of_cau_filter_spec : ∀ n, ∀ {x y},
+  x ∈ set_seq_of_cau_filter hf n → y ∈ set_seq_of_cau_filter hf n → dist x y < 1/((n : ℝ) + 1)
+| 0 := some_spec (some_spec ((cauchy_of_metric.1 hf).2 _ (one_div_succ 0)))
+| (n+1) := λ x y hx hy,
+  some_spec (some_spec ((cauchy_of_metric.1 hf).2 _ (one_div_succ (n+1)))) x y
+    (mem_of_mem_inter_right hx) (mem_of_mem_inter_right hy)
+
+-- this must exist somewhere, no?
+private lemma mono_of_mono_succ_aux {α} [partial_order α] (f : ℕ → α) (h : ∀ n, f (n+1) ≤ f n) (m : ℕ) :
+  ∀ n, f (m + n) ≤ f m
+| 0 := le_refl _
+| (k+1) := le_trans (h _) (mono_of_mono_succ_aux _)
+
+lemma mono_of_mono_succ {α} [partial_order α] (f : ℕ → α) (h : ∀ n, f (n+1) ≤ f n) {m n : ℕ}
+  (hmn : m ≤ n) : f n ≤ f m :=
+let ⟨k, hk⟩ := nat.exists_eq_add_of_le hmn in
+by simpa [hk] using mono_of_mono_succ_aux f h m k
+
+lemma set_seq_of_cau_filter_monotone' (n : ℕ) :
+  set_seq_of_cau_filter hf (n+1) ⊆ set_seq_of_cau_filter hf n :=
+inter_subset_left _ _
+
+lemma set_seq_of_cau_filter_monotone {n k : ℕ} (hle : n ≤ k) : 
+  set_seq_of_cau_filter hf k ⊆ set_seq_of_cau_filter hf n :=
+mono_of_mono_succ (set_seq_of_cau_filter hf) (set_seq_of_cau_filter_monotone' hf) hle
+
+noncomputable def seq_of_cau_filter (n : ℕ) : β :=
+some (set_seq_of_cau_filter_inhabited hf n)
+
+lemma seq_of_cau_filter_mem_set_seq (n : ℕ) : seq_of_cau_filter hf n ∈ set_seq_of_cau_filter hf n :=
+some_spec (set_seq_of_cau_filter_inhabited hf n)
+
+lemma seq_of_cau_filter_is_cauchy' {n k : ℕ} (hle : n ≤ k) :
+  dist (seq_of_cau_filter hf n) (seq_of_cau_filter hf k) < 1 / ((n : ℝ) + 1) :=
+set_seq_of_cau_filter_spec hf _
+  (seq_of_cau_filter_mem_set_seq hf n)
+  (set_seq_of_cau_filter_monotone hf hle (seq_of_cau_filter_mem_set_seq hf k))
+
+lemma is_cau_seq_of_dist_tendsto_0 {s : ℕ → β} {b : ℕ → ℝ} (h : ∀ {n k : ℕ}, n ≤ k → dist (s n) (s k) < b n)
+  (hb : tendsto b at_top (nhds 0)) : is_cau_seq norm s :=
+λ ε hε,
+begin
+  have hb : ∀ (i : set ℝ), (0:ℝ) ∈ i → is_open i → (∃ (a : ℕ), ∀ (c : ℕ), c ≥ a → b c ∈ i),
+  { simpa [tendsto, nhds] using hb },
+  cases hb (ball 0 ε) (mem_ball_self hε) (is_open_ball) with N hN,
+  existsi N,
+  intros k hk,
+  rw [←dist_eq_norm, dist_comm],
+  apply lt.trans,
+  apply h hk,
+  have := hN _ (le_refl _),
+  have bnn : ∀ n, b n ≥ 0, from λ n, le_of_lt (lt_of_le_of_lt dist_nonneg (h (le_refl n))),
+  simpa [real.norm_eq_abs, abs_of_nonneg (bnn _)] using this
+end
+
+lemma tendsto_div : tendsto (λ n : ℕ, 1 / ((n : ℝ) + 1)) at_top (nhds 0) :=
+suffices tendsto (λ n : ℕ, 1 / (↑(n + 1) : ℝ)) at_top (nhds 0), by simpa,
+tendsto_comp_succ_at_top_iff.2 tendsto_one_div_at_top_nhds_0_nat
+
+lemma seq_of_cau_filter_is_cauchy :
+  is_cau_seq norm (seq_of_cau_filter hf) :=
+is_cau_seq_of_dist_tendsto_0 (@seq_of_cau_filter_is_cauchy' _ _ _ hf) tendsto_div
+
+noncomputable def cau_seq_of_cau_filter : cau_seq β norm :=
+⟨seq_of_cau_filter hf, seq_of_cau_filter_is_cauchy hf⟩
+
+lemma cau_seq_of_cau_filter_mem_set_seq (n : ℕ) : cau_seq_of_cau_filter hf n ∈ set_seq_of_cau_filter hf n :=
+seq_of_cau_filter_mem_set_seq hf n
+
+variable complete : ∀ s : cau_seq β norm, ∃ b : β, ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, ∥b - s.val n∥ < ε
+include complete
+
+noncomputable def cau_seq_lim (s : cau_seq β norm) : β := some (complete s)
+
+lemma cau_seq_lim_spec (s : cau_seq β norm) : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, ∥cau_seq_lim complete s - s.val n∥ < ε :=
+some_spec (complete s)
+
+noncomputable def cau_filter_lim : β := cau_seq_lim complete (cau_seq_of_cau_filter hf)
+
+lemma cau_filter_lim_spec : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, ∥cau_filter_lim hf complete - cau_seq_of_cau_filter hf n∥ < ε :=
+cau_seq_lim_spec complete _
+
+/-
+Let lim be the limit of the Cauchy sequence seq that is derived from the Cauchy filter f.
+Given t1 in the filter f and t2 a neighborhood of lim, it suffices to show that t1 ∩ t2 is nonempty.
+Pick ε so that the eps-ball around lim is contained in t2.
+Pick n with 1/n < ε/2, and n2 such that dist(seq n2, lim) < ε/2. Let N = max(n, n2).
+We defined seq by looking at a decreasing sequence of sets of f with shrinking radius.
+The Nth one has radius < 1/N < ε/2. This set is in f, so we can find an element x that's also in t1.
+dist(x, seq N) < ε/2 since seq N is in this set, and dist (seq N, lim) < ε/2,
+so x is in the ε-ball of lim, and thus in t2.
+-/
+lemma le_nhds_cau_seq_lim : f ≤ nhds (cau_seq_lim complete (cau_seq_of_cau_filter hf)) :=
+begin
+  apply (le_nhds_iff_adhp_of_cauchy hf).2,
+  apply forall_sets_neq_empty_iff_neq_bot.1,
+  intros s hs,
+  simp at hs,
+  rcases hs with ⟨t1, ht1, t2, ht2, ht1t2⟩,
+  apply ne_empty_iff_exists_mem.2,
+  rcases mem_nhds_iff_metric.1 ht2 with ⟨ε, hε, ht2'⟩,
+  cases cauchy_of_metric.1 hf with hfb _,
+  have : ε / 2 > 0, from div_pos hε (by norm_num),
+  have : ∃ n : ℕ, 1 / (↑n + 1) < ε / 2, from exists_nat_one_div_lt this,
+  cases this with n hnε,
+  cases cau_filter_lim_spec hf complete _ this with n2 hn2,
+  let N := max n n2,
+  have hNε : 1 / (↑N+1) < ε / 2,
+  { apply lt_of_le_of_lt _ hnε,
+    apply one_div_le_one_div_of_le,
+    { exact add_pos_of_nonneg_of_pos (nat.cast_nonneg _) zero_lt_one },
+    { apply add_le_add_right, simp [le_max_left] }},
+  have ht1sn : t1 ∩ set_seq_of_cau_filter hf N ∈ f.sets, 
+    from inter_mem_sets ht1 (set_seq_of_cau_filter_mem_sets hf _),
+  have hts1n_ne : t1 ∩ set_seq_of_cau_filter hf N ≠ ∅, 
+    from forall_sets_neq_empty_iff_neq_bot.2 hfb _ ht1sn,
+  cases exists_mem_of_ne_empty hts1n_ne with x hx,
+  have hdist1 := set_seq_of_cau_filter_spec hf _ hx.2 (cau_seq_of_cau_filter_mem_set_seq hf N),
+  have hdist2 := hn2 N (le_max_right _ _),
+  replace hdist1 := lt_trans hdist1 hNε,
+  rw [←dist_eq_norm, dist_comm] at hdist2,
+  have hdist : dist x (cau_filter_lim hf complete) < ε,
+  { apply lt_of_le_of_lt,
+    { apply metric_space.dist_triangle,
+      exact (cau_seq_of_cau_filter hf) N },
+    { rw ←add_halves ε,
+      apply add_lt_add; assumption }},
+  have hxt2 : x ∈ t2, from ht2' hdist,
+  existsi x,
+  apply ht1t2,
+  exact mem_inter hx.left hxt2
+end
+
+theorem complete_space_of_cauchy_complete : complete_space β :=
+⟨λ _ hf, ⟨cau_seq_lim complete (cau_seq_of_cau_filter hf), le_nhds_cau_seq_lim hf complete⟩⟩
+
+end
+
+/- TODO
+
+section
+variables {β : Type*} [normed_field β] [complete_space β]
+
+theorem cauchy_complete_of_complete_space (s : cau_seq β norm) :
+  ∃ b : β, ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, ∥b - s.val n∥ < ε :=
+sorry
 
-end
+end -/