abs_sub

Stream: new members

[Iocta]

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,
  apply  decidable_linear_ordered_add_comm_group.eq_of_abs_sub_nonpos,
  by_contradiction 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]

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]

ah