Skip to content
Permalink
Browse files

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

…er completeness
  • Loading branch information...
robertylewis committed Sep 28, 2018
1 parent c199015 commit b72cc01d5c1ea56ee42753595262bf6657b90bb3
@@ -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⌋ :=
@@ -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) :=

This comment has been minimized.

Copy link
@PatrickMassot

PatrickMassot Sep 28, 2018

Collaborator

This up-arrow is useless

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) :=

This comment has been minimized.

Copy link
@PatrickMassot

PatrickMassot Sep 28, 2018

Collaborator

This up-arrow is also useless

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
@@ -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
@@ -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
@@ -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
@@ -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,178 @@ 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?
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 (some_spec (set_seq_of_cau_filter_inhabited 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 : ℕ), (b_1 : ℕ), b_1 a b b_1 ∈ 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 : ∃ n : ℕ, 1 / (↑n + 1) < ε / 2,
from exists_nat_one_div_lt (show ε / 2 > 0, from div_pos hε (by norm_num)),
cases this with n hnε,
have : ε / 2 > 0, from div_pos hε (by norm_num),
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,
apply mem_inter _ hxt2,
apply hx.left
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 -/

0 comments on commit b72cc01

Please sign in to comment.
You can’t perform that action at this time.