## Stream: new members

### Topic: abs_sub

#### Iocta (Jul 20 2020 at 22:42):

Why doesn't rw abs_sub work at the end?

import analysis.specific_limits
import data.int.parity

notation |x| := abs x

variable { φ : ℕ → ℕ}
variables {u : ℕ → ℝ} {a l : ℝ}

def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

lemma eq_of_abs_sub_le_all (x y : ℝ) : (∀ ε > 0, |x - y| ≤ ε) → x = y :=
begin
intro h,
push_neg at H,
specialize h ( |x-y|/2) (by linarith),
linarith,
end

lemma unique_limit {u l l'} : seq_limit u l → seq_limit u l' → l = l' :=
begin
intros hl hl',
apply eq_of_abs_sub_le_all,
intros ε ε_pos,
specialize hl (ε/2) (by linarith),
cases hl with N hN,
specialize hl' (ε/2) (by linarith),
cases hl' with N' hN',
specialize hN (max N N') (le_max_left _ _),
specialize hN' (max N N') (le_max_right _ _),
calc |l - l'| = |(l-u (max N N')) + (u (max N N') -l')| : by ring
... ≤ |l - u (max N N')| + |u (max N N') - l'| : by apply abs_add
... =  |u (max N N') - l| + |u (max N N') - l'| : by rw abs_sub
... ≤ ε/2 + ε/2 : by linarith
... = ε : by ring,
end

/-
The next lemma is proved by an easy induction, but we haven't seen induction
in this tutorial. If you did the natural number game then you can delete
the proof below and try to reconstruct it.
-/
/-- An extraction is greater than id -/
lemma id_le_extraction' : extraction φ → ∀ n, n ≤ φ n :=
begin
intros hyp n,
induction n with n hn,
{ exact nat.zero_le _ },
{ exact nat.succ_le_of_lt (by linarith [hyp n (n+1) (by linarith)]) },
end

/-- Extractions take arbitrarily large values for arbitrarily large
inputs. -/
-- 0039
lemma extraction_ge : extraction φ → ∀ N N', ∃ n ≥ N', φ n ≥ N :=
begin
intros h N N',
use max N N',
split,
{apply le_max_right,},
unfold extraction at h,
calc
N ≤ max N N' : by apply le_max_left
... ≤ φ (max N N') : by apply id_le_extraction' h
end

lemma id_le_extraction {φ}: extraction φ → ∀ n, n ≤ φ n :=
begin
intros hyp n,
induction n with n hn,
{ exact nat.zero_le _ },
{ exact nat.succ_le_of_lt (by linarith [hyp n (n+1) (by linarith)]) },
end

/-- If u tends to l then its subsequences tend to l. -/
-- 0041
lemma subseq_tendsto_of_tendsto' (h : seq_limit u l) (hφ : extraction φ) :
seq_limit (u ∘ φ) l :=
begin
intros ε ε_pos,
cases h ε ε_pos with N h',
use N,
intros n hn,
have φn_ge_n: φ n ≥ n, by apply id_le_extraction hφ,
specialize h' (φ n) (by linarith),
rw [function.comp_app],
exact h',
end

/-- Cauchy_sequence sequence -/
def cauchy_sequence (u : ℕ → ℝ) :=
∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε

-- 0043
example : (∃ l, seq_limit u l) → cauchy_sequence u :=
begin
intro hl,
cases hl with l hl,
intros ε ε_pos,
specialize hl (ε/3) (by linarith),
cases hl with N hN,
use N,
intros p q hp hq,
have up_close: | u p - l | ≤ ε / 3,
{specialize hN p hp, finish},
have uq_close: | u q - l | ≤ ε / 3,
{specialize hN q hq, finish,},
calc | u p - u q | ≤  | ( u p -l )  - ( u q - l) |: by ring
... ≤ | ( u p - l) + (l - u q) | : by ring
... ≤  | u p - l | + | l - u q | : by apply abs_add
... = | u p - l | + | u q - l | :  by rw abs_sub
... ≤ ε / 3 + ε / 3 : by linarith
... ≤ ε : by linarith
end


#### Kevin Buzzard (Jul 20 2020 at 23:10):

Because it rewrites the first occurrence of |x-y| that it sees, which is not the one you want it to rewrite. Tell it which one to rewrite with rw abs_sub l.

#### Iocta (Jul 20 2020 at 23:32):

ah

Last updated: May 18 2021 at 17:44 UTC