feat(library/theories/analysis/{metric_space,real_limit}: add convergence theorems
This commit is contained in:
Jeremy Avigad
parent
aa8dfba5a5
commit
42c9bdc463
2 changed files with 415 additions and 23 deletions
library/theories/analysis
|
|
@ -38,8 +38,10 @@ eq_of_dist_eq_zero (eq_zero_of_nonneg_of_forall_le !dist_nonneg H)
|
|||
|
||||
open nat
|
||||
|
||||
/- convergence of a sequence -/
|
||||
|
||||
definition converges_to_seq (X : ℕ → M) (y : M) : Prop :=
|
||||
∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → dist (X n) y < ε
|
||||
∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ ⦃n⦄, n ≥ N → dist (X n) y < ε
|
||||
|
||||
-- the same, with ≤ in place of <; easier to prove, harder to use
|
||||
definition converges_to_seq.intro {X : ℕ → M} {y : M}
|
||||
|
|
@ -81,17 +83,71 @@ eq_of_forall_dist_le
|
|||
... = ε : add_halves,
|
||||
show dist y₁ y₂ ≤ ε, from le_of_lt this)
|
||||
|
||||
proposition eq_limit_of_converges_to_seq {X : ℕ → M} (y : M) (H : X ⟶ y in ℕ) :
|
||||
proposition eq_limit_of_converges_to_seq {X : ℕ → M} {y : M} (H : X ⟶ y in ℕ) :
|
||||
y = @limit_seq M _ X (exists.intro y H) :=
|
||||
converges_to_seq_unique H (@converges_to_limit_seq M _ X (exists.intro y H))
|
||||
|
||||
proposition converges_to_seq_constant (y : M) : (λn, y) ⟶ y in ℕ :=
|
||||
take ε, assume egt0 : ε > 0,
|
||||
exists.intro 0
|
||||
(take n, suppose n ≥ 0,
|
||||
calc
|
||||
dist y y = 0 : !dist_self
|
||||
... < ε : egt0)
|
||||
exists.intro 0
|
||||
(take n, suppose n ≥ 0,
|
||||
calc
|
||||
dist y y = 0 : !dist_self
|
||||
... < ε : egt0)
|
||||
|
||||
proposition converges_to_seq_offset {X : ℕ → M} {y : M} (k : ℕ) (H : X ⟶ y in ℕ) :
|
||||
(λ n, X (n + k)) ⟶ y in ℕ :=
|
||||
take ε, suppose ε > 0,
|
||||
obtain N HN, from H `ε > 0`,
|
||||
exists.intro N
|
||||
(take n : ℕ, assume ngtN : n ≥ N,
|
||||
show dist (X (n + k)) y < ε, from HN (n + k) (le.trans ngtN !le_add_right))
|
||||
|
||||
proposition converges_to_seq_offset_left {X : ℕ → M} {y : M} (k : ℕ) (H : X ⟶ y in ℕ) :
|
||||
(λ n, X (k + n)) ⟶ y in ℕ :=
|
||||
have aux : (λ n, X (k + n)) = (λ n, X (n + k)), from funext (take n, by rewrite nat.add.comm),
|
||||
by+ rewrite aux; exact converges_to_seq_offset k H
|
||||
|
||||
proposition converges_to_seq_offset_succ {X : ℕ → M} {y : M} (H : X ⟶ y in ℕ) :
|
||||
(λ n, X (succ n)) ⟶ y in ℕ :=
|
||||
converges_to_seq_offset 1 H
|
||||
|
||||
proposition converges_to_seq_of_converges_to_seq_offset
|
||||
{X : ℕ → M} {y : M} {k : ℕ} (H : (λ n, X (n + k)) ⟶ y in ℕ) :
|
||||
X ⟶ y in ℕ :=
|
||||
take ε, suppose ε > 0,
|
||||
obtain N HN, from H `ε > 0`,
|
||||
exists.intro (N + k)
|
||||
(take n : ℕ, assume nge : n ≥ N + k,
|
||||
have n - k ≥ N, from le_sub_of_add_le nge,
|
||||
have dist (X (n - k + k)) y < ε, from HN (n - k) this,
|
||||
show dist (X n) y < ε, using this,
|
||||
by rewrite [(nat.sub_add_cancel (le.trans !le_add_left nge)) at this]; exact this)
|
||||
|
||||
proposition converges_to_seq_of_converges_to_seq_offset_left
|
||||
{X : ℕ → M} {y : M} {k : ℕ} (H : (λ n, X (k + n)) ⟶ y in ℕ) :
|
||||
X ⟶ y in ℕ :=
|
||||
have aux : (λ n, X (k + n)) = (λ n, X (n + k)), from funext (take n, by rewrite nat.add.comm),
|
||||
by+ rewrite aux at H; exact converges_to_seq_of_converges_to_seq_offset H
|
||||
|
||||
proposition converges_to_seq_of_converges_to_seq_offset_succ
|
||||
{X : ℕ → M} {y : M} (H : (λ n, X (succ n)) ⟶ y in ℕ) :
|
||||
X ⟶ y in ℕ :=
|
||||
@converges_to_seq_of_converges_to_seq_offset M strucM X y 1 H
|
||||
|
||||
proposition converges_to_seq_offset_iff (X : ℕ → M) (y : M) (k : ℕ) :
|
||||
((λ n, X (n + k)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
|
||||
iff.intro converges_to_seq_of_converges_to_seq_offset !converges_to_seq_offset
|
||||
|
||||
proposition converges_to_seq_offset_left_iff (X : ℕ → M) (y : M) (k : ℕ) :
|
||||
((λ n, X (k + n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
|
||||
iff.intro converges_to_seq_of_converges_to_seq_offset_left !converges_to_seq_offset_left
|
||||
|
||||
proposition converges_to_seq_offset_succ_iff (X : ℕ → M) (y : M) :
|
||||
((λ n, X (succ n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
|
||||
iff.intro converges_to_seq_of_converges_to_seq_offset_succ !converges_to_seq_offset_succ
|
||||
|
||||
/- cauchy sequences -/
|
||||
|
||||
definition cauchy (X : ℕ → M) : Prop :=
|
||||
∀ ε : ℝ, ε > 0 → ∃ N, ∀ m n, m ≥ N → n ≥ N → dist (X m) (X n) < ε
|
||||
|
|
@ -117,6 +173,8 @@ take ε, suppose ε > 0,
|
|||
|
||||
end metric_space_M
|
||||
|
||||
/- convergence of a function at a point -/
|
||||
|
||||
section metric_space_M_N
|
||||
variables {M N : Type} [strucM : metric_space M] [strucN : metric_space N]
|
||||
include strucM strucN
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
/-
|
||||
Copyright (c) 2015 Jeremy Avigad. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Jeremy Avigad
|
||||
Authors: Jeremy Avigad, Robert Y. Lewis
|
||||
|
||||
Instantiates the reals as a metric space, and expresses completeness, sup, and inf in
|
||||
a manner that is less constructive, but more convenient, than the way it is done in
|
||||
|
|
@ -37,7 +37,6 @@ protected definition to_metric_space [instance] : metric_space ℝ :=
|
|||
dist_triangle := abs_sub_le
|
||||
⦄
|
||||
|
||||
section nat
|
||||
open nat
|
||||
|
||||
definition converges_to_seq (X : ℕ → ℝ) (y : ℝ) : Prop :=
|
||||
|
|
@ -69,6 +68,45 @@ converges_to_seq_unique H (@converges_to_limit_seq X (exists.intro y H))
|
|||
proposition converges_to_seq_constant (y : ℝ) : (λn, y) ⟶ y in ℕ :=
|
||||
metric_space.converges_to_seq_constant y
|
||||
|
||||
proposition converges_to_seq_offset {X : ℕ → ℝ} {y : ℝ} (k : ℕ) (H : X ⟶ y in ℕ) :
|
||||
(λ n, X (n + k)) ⟶ y in ℕ :=
|
||||
metric_space.converges_to_seq_offset k H
|
||||
|
||||
proposition converges_to_seq_offset_left {X : ℕ → ℝ} {y : ℝ} (k : ℕ) (H : X ⟶ y in ℕ) :
|
||||
(λ n, X (k + n)) ⟶ y in ℕ :=
|
||||
metric_space.converges_to_seq_offset_left k H
|
||||
|
||||
proposition converges_to_set_offset_succ {X : ℕ → ℝ} {y : ℝ} (H : X ⟶ y in ℕ) :
|
||||
(λ n, X (succ n)) ⟶ y in ℕ :=
|
||||
metric_space.converges_to_seq_offset_succ H
|
||||
|
||||
proposition converges_to_seq_of_converges_to_seq_offset
|
||||
{X : ℕ → ℝ} {y : ℝ} {k : ℕ} (H : (λ n, X (n + k)) ⟶ y in ℕ) :
|
||||
X ⟶ y in ℕ :=
|
||||
metric_space.converges_to_seq_of_converges_to_seq_offset H
|
||||
|
||||
proposition converges_to_seq_of_converges_to_seq_offset_left
|
||||
{X : ℕ → ℝ} {y : ℝ} {k : ℕ} (H : (λ n, X (k + n)) ⟶ y in ℕ) :
|
||||
X ⟶ y in ℕ :=
|
||||
metric_space.converges_to_seq_of_converges_to_seq_offset_left H
|
||||
|
||||
proposition converges_to_seq_of_converges_to_seq_offset_succ
|
||||
{X : ℕ → ℝ} {y : ℝ} (H : (λ n, X (succ n)) ⟶ y in ℕ) :
|
||||
X ⟶ y in ℕ :=
|
||||
metric_space.converges_to_seq_of_converges_to_seq_offset_succ H
|
||||
|
||||
proposition converges_to_seq_offset_iff (X : ℕ → ℝ) (y : ℝ) (k : ℕ) :
|
||||
((λ n, X (n + k)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
|
||||
metric_space.converges_to_seq_offset_iff X y k
|
||||
|
||||
proposition converges_to_seq_offset_left_iff (X : ℕ → ℝ) (y : ℝ) (k : ℕ) :
|
||||
((λ n, X (k + n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
|
||||
metric_space.converges_to_seq_offset_left_iff X y k
|
||||
|
||||
proposition converges_to_seq_offset_succ_iff (X : ℕ → ℝ) (y : ℝ) :
|
||||
((λ n, X (succ n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
|
||||
metric_space.converges_to_seq_offset_succ_iff X y
|
||||
|
||||
/- the completeness of the reals, "translated" from data.real.complete -/
|
||||
|
||||
definition cauchy (X : ℕ → ℝ) := metric_space.cauchy X
|
||||
|
|
@ -159,6 +197,14 @@ have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b),
|
|||
from and.intro HX (exists.intro b Hb),
|
||||
by+ rewrite [↑sup, dif_pos H]; exact and.right (sup_aux_spec H) b Hb
|
||||
|
||||
proposition exists_mem_and_lt_of_lt_sup {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : b < sup X) :
|
||||
∃ x, x ∈ X ∧ b < x :=
|
||||
have ¬ ∀ x, x ∈ X → x ≤ b, from assume H, not_le_of_gt Hb (sup_le HX H),
|
||||
obtain x (Hx : ¬ (x ∈ X → x ≤ b)), from exists_not_of_not_forall this,
|
||||
exists.intro x
|
||||
(have x ∈ X ∧ ¬ x ≤ b, by rewrite [-not_implies_iff_and_not]; apply Hx,
|
||||
and.intro (and.left this) (lt_of_not_ge (and.right this)))
|
||||
|
||||
private definition exists_is_inf {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x)) :
|
||||
∃ y, is_inf X y :=
|
||||
let x := some (and.left H), b := some (and.right H) in
|
||||
|
|
@ -186,9 +232,297 @@ have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x),
|
|||
from and.intro HX (exists.intro b Hb),
|
||||
by+ rewrite [↑inf, dif_pos H]; exact and.right (inf_aux_spec H) b Hb
|
||||
|
||||
proposition exists_mem_and_lt_of_inf_lt {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : inf X < b) :
|
||||
∃ x, x ∈ X ∧ x < b :=
|
||||
have ¬ ∀ x, x ∈ X → b ≤ x, from assume H, not_le_of_gt Hb (le_inf HX H),
|
||||
obtain x (Hx : ¬ (x ∈ X → b ≤ x)), from exists_not_of_not_forall this,
|
||||
exists.intro x
|
||||
(have x ∈ X ∧ ¬ b ≤ x, by rewrite [-not_implies_iff_and_not]; apply Hx,
|
||||
and.intro (and.left this) (lt_of_not_ge (and.right this)))
|
||||
|
||||
-- TODO: is there a better place to put this?
|
||||
proposition image_neg_eq (X : set ℝ) : (λ x, -x) '[X] = {x | -x ∈ X} :=
|
||||
set.ext (take x, iff.intro
|
||||
(assume H, obtain y [(Hy₁ : y ∈ X) (Hy₂ : -y = x)], from H,
|
||||
show -x ∈ X, by rewrite [-Hy₂, neg_neg]; exact Hy₁)
|
||||
(assume H : -x ∈ X, exists.intro (-x) (and.intro H !neg_neg)))
|
||||
|
||||
proposition sup_neg {X : set ℝ} (nonempty_X : ∃ x, x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → b ≤ x) :
|
||||
sup {x | -x ∈ X} = - inf X :=
|
||||
let negX := {x | -x ∈ X} in
|
||||
have nonempty_negX : ∃ x, x ∈ negX, from
|
||||
obtain x Hx, from nonempty_X,
|
||||
have -(-x) ∈ X,
|
||||
by rewrite neg_neg; apply Hx,
|
||||
exists.intro (-x) this,
|
||||
have H₁ : ∀ x, x ∈ negX → x ≤ - inf X, from
|
||||
take x,
|
||||
assume H,
|
||||
have inf X ≤ -x,
|
||||
from inf_le H Hb,
|
||||
show x ≤ - inf X,
|
||||
from le_neg_of_le_neg this,
|
||||
have H₂ : ∀ x, x ∈ X → -sup negX ≤ x, from
|
||||
take x,
|
||||
assume H,
|
||||
have -(-x) ∈ X, by rewrite neg_neg; apply H,
|
||||
have -x ≤ sup negX, from le_sup this H₁,
|
||||
show -sup negX ≤ x,
|
||||
from !neg_le_of_neg_le this,
|
||||
eq_of_le_of_ge
|
||||
(show sup negX ≤ - inf X,
|
||||
from sup_le nonempty_negX H₁)
|
||||
(show -inf X ≤ sup negX,
|
||||
from !neg_le_of_neg_le (le_inf nonempty_X H₂))
|
||||
|
||||
proposition inf_neg {X : set ℝ} (nonempty_X : ∃ x, x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → x ≤ b) :
|
||||
inf {x | -x ∈ X} = - sup X :=
|
||||
let negX := {x | -x ∈ X} in
|
||||
have nonempty_negX : ∃ x, x ∈ negX, from
|
||||
obtain x Hx, from nonempty_X,
|
||||
have -(-x) ∈ X,
|
||||
by rewrite neg_neg; apply Hx,
|
||||
exists.intro (-x) this,
|
||||
have Hb' : ∀ x, x ∈ negX → -b ≤ x,
|
||||
from take x, assume H, !neg_le_of_neg_le (Hb _ H),
|
||||
have HX : X = {x | -x ∈ negX},
|
||||
from set.ext (take x, by rewrite [↑set_of, ↑mem, +neg_neg]),
|
||||
show inf {x | -x ∈ X} = - sup X,
|
||||
using HX Hb' nonempty_negX, by rewrite [HX at {2}, sup_neg nonempty_negX Hb', neg_neg]
|
||||
|
||||
end
|
||||
|
||||
end nat
|
||||
/- limits under pointwise operations -/
|
||||
|
||||
section limit_operations
|
||||
open nat
|
||||
|
||||
variables {X Y : ℕ → ℝ}
|
||||
variables {x y : ℝ}
|
||||
|
||||
proposition add_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) :
|
||||
(λ n, X n + Y n) ⟶ x + y in ℕ :=
|
||||
take ε, suppose ε > 0,
|
||||
have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos,
|
||||
obtain N₁ (HN₁ : ∀ {n}, n ≥ N₁ → abs (X n - x) < ε / 2), from HX e2pos,
|
||||
obtain N₂ (HN₂ : ∀ {n}, n ≥ N₂ → abs (Y n - y) < ε / 2), from HY e2pos,
|
||||
let N := nat.max N₁ N₂ in
|
||||
exists.intro N
|
||||
(take n,
|
||||
suppose n ≥ N,
|
||||
have ngtN₁ : n ≥ N₁, from nat.le.trans !nat.le_max_left `n ≥ N`,
|
||||
have ngtN₂ : n ≥ N₂, from nat.le.trans !nat.le_max_right `n ≥ N`,
|
||||
show abs ((X n + Y n) - (x + y)) < ε, from calc
|
||||
abs ((X n + Y n) - (x + y))
|
||||
= abs ((X n - x) + (Y n - y)) : by rewrite [sub_add_eq_sub_sub, *sub_eq_add_neg,
|
||||
*add.assoc, add.left_comm (-x)]
|
||||
... ≤ abs (X n - x) + abs (Y n - y) : abs_add_le_abs_add_abs
|
||||
... < ε / 2 + ε / 2 : add_lt_add (HN₁ ngtN₁) (HN₂ ngtN₂)
|
||||
... = ε : add_halves)
|
||||
|
||||
private lemma mul_left_converges_to_seq_of_pos {c : ℝ} (cnz : c ≠ 0) (HX : X ⟶ x in ℕ) :
|
||||
(λ n, c * X n) ⟶ c * x in ℕ :=
|
||||
take ε, suppose ε > 0,
|
||||
have abscpos : abs c > 0, from abs_pos_of_ne_zero cnz,
|
||||
have epos : ε / abs c > 0, from div_pos_of_pos_of_pos `ε > 0` abscpos,
|
||||
obtain N (HN : ∀ {n}, n ≥ N → abs (X n - x) < ε / abs c), from HX epos,
|
||||
exists.intro N
|
||||
(take n,
|
||||
suppose n ≥ N,
|
||||
have H : abs (X n - x) < ε / abs c, from HN this,
|
||||
show abs (c * X n - c * x) < ε, from calc
|
||||
abs (c * X n - c * x) = abs c * abs (X n - x) : by rewrite [-mul_sub_left_distrib, abs_mul]
|
||||
... < abs c * (ε / abs c) : mul_lt_mul_of_pos_left H abscpos
|
||||
... = ε : mul_div_cancel' (ne_of_gt abscpos))
|
||||
|
||||
proposition mul_left_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) :
|
||||
(λ n, c * X n) ⟶ c * x in ℕ :=
|
||||
by_cases
|
||||
(assume cz : c = 0,
|
||||
have (λ n, c * X n) = (λ n, 0), from funext (take x, by rewrite [cz, zero_mul]),
|
||||
by+ rewrite [this, cz, zero_mul]; apply converges_to_seq_constant)
|
||||
(suppose c ≠ 0, mul_left_converges_to_seq_of_pos this HX)
|
||||
|
||||
proposition mul_right_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) :
|
||||
(λ n, X n * c) ⟶ x * c in ℕ :=
|
||||
have (λ n, X n * c) = (λ n, c * X n), from funext (take x, !mul.comm),
|
||||
by+ rewrite [this, mul.comm]; apply mul_left_converges_to_seq c HX
|
||||
|
||||
-- TODO: converges_to_seq_div, converges_to_seq_mul_left_iff, etc.
|
||||
|
||||
proposition neg_converges_to_seq (HX : X ⟶ x in ℕ) :
|
||||
(λ n, - X n) ⟶ - x in ℕ :=
|
||||
take ε, suppose ε > 0,
|
||||
obtain N (HN : ∀ {n}, n ≥ N → abs (X n - x) < ε), from HX this,
|
||||
exists.intro N
|
||||
(take n,
|
||||
suppose n ≥ N,
|
||||
show abs (- X n - (- x)) < ε,
|
||||
by rewrite [-neg_neg_sub_neg, *neg_neg, abs_neg]; exact HN `n ≥ N`)
|
||||
|
||||
proposition neg_converges_to_seq_iff (X : ℕ → ℝ) :
|
||||
((λ n, - X n) ⟶ - x in ℕ) ↔ (X ⟶ x in ℕ) :=
|
||||
have aux : X = λ n, (- (- X n)), from funext (take n, by rewrite neg_neg),
|
||||
iff.intro
|
||||
(assume H : (λ n, -X n)⟶ -x in ℕ,
|
||||
show X ⟶ x in ℕ, by+ rewrite [aux, -neg_neg x]; exact neg_converges_to_seq H)
|
||||
neg_converges_to_seq
|
||||
|
||||
proposition abs_converges_to_seq_zero (HX : X ⟶ 0 in ℕ) : (λ n, abs (X n)) ⟶ 0 in ℕ :=
|
||||
take ε, suppose ε > 0,
|
||||
obtain N (HN : ∀ n, n ≥ N → abs (X n - 0) < ε), from HX `ε > 0`,
|
||||
exists.intro N
|
||||
(take n, assume Hn : n ≥ N,
|
||||
have abs (X n) < ε, from (!sub_zero ▸ HN n Hn),
|
||||
show abs (abs (X n) - 0) < ε, using this,
|
||||
by rewrite [sub_zero, abs_of_nonneg !abs_nonneg]; apply this)
|
||||
|
||||
proposition converges_to_seq_zero_of_abs_converges_to_seq_zero (HX : (λ n, abs (X n)) ⟶ 0 in ℕ) :
|
||||
X ⟶ 0 in ℕ :=
|
||||
take ε, suppose ε > 0,
|
||||
obtain N (HN : ∀ n, n ≥ N → abs (abs (X n) - 0) < ε), from HX `ε > 0`,
|
||||
exists.intro (N : ℕ)
|
||||
(take n : ℕ, assume Hn : n ≥ N,
|
||||
have HN' : abs (abs (X n) - 0) < ε, from HN n Hn,
|
||||
have abs (X n) < ε,
|
||||
by+ rewrite [real.sub_zero at HN', abs_of_nonneg !abs_nonneg at HN']; apply HN',
|
||||
show abs (X n - 0) < ε, using this,
|
||||
by rewrite sub_zero; apply this)
|
||||
|
||||
proposition abs_converges_to_seq_zero_iff (X : ℕ → ℝ) :
|
||||
((λ n, abs (X n)) ⟶ 0 in ℕ) ↔ (X ⟶ 0 in ℕ) :=
|
||||
iff.intro converges_to_seq_zero_of_abs_converges_to_seq_zero abs_converges_to_seq_zero
|
||||
|
||||
-- TODO: products of two sequences, converges_seq, limit_seq
|
||||
|
||||
end limit_operations
|
||||
|
||||
/- monotone sequences -/
|
||||
|
||||
section monotone_sequences
|
||||
open nat set
|
||||
|
||||
variable {X : ℕ → ℝ}
|
||||
|
||||
definition nondecreasing (X : ℕ → ℝ) : Prop := ∀ ⦃i j⦄, i ≤ j → X i ≤ X j
|
||||
|
||||
proposition nondecreasing_of_forall_le_succ (H : ∀ i, X i ≤ X (succ i)) : nondecreasing X :=
|
||||
take i j, suppose i ≤ j,
|
||||
have ∀ n, X i ≤ X (i + n), from
|
||||
take n, nat.induction_on n
|
||||
(by rewrite nat.add_zero; apply le.refl)
|
||||
(take n, assume ih, le.trans ih (H (i + n))),
|
||||
have X i ≤ X (i + (j - i)), from !this,
|
||||
by+ rewrite [add_sub_of_le `i ≤ j` at this]; exact this
|
||||
|
||||
proposition converges_to_seq_sup_of_nondecreasing (nondecX : nondecreasing X) {b : ℝ}
|
||||
(Hb : ∀ i, X i ≤ b) : X ⟶ sup (X '[univ]) in ℕ :=
|
||||
let sX := sup (X '[univ]) in
|
||||
have Xle : ∀ i, X i ≤ sX, from
|
||||
take i,
|
||||
have ∀ x, x ∈ X '[univ] → x ≤ b, from
|
||||
(take x, assume H,
|
||||
obtain i [H' (Hi : X i = x)], from H,
|
||||
by rewrite -Hi; exact Hb i),
|
||||
show X i ≤ sX, from le_sup (mem_image_of_mem X !mem_univ) this,
|
||||
have exX : ∃ x, x ∈ X '[univ],
|
||||
from exists.intro (X 0) (mem_image_of_mem X !mem_univ),
|
||||
take ε, assume epos : ε > 0,
|
||||
have sX - ε < sX, from !sub_lt_of_pos epos,
|
||||
obtain x' [(H₁x' : x' ∈ X '[univ]) (H₂x' : sX - ε < x')],
|
||||
from exists_mem_and_lt_of_lt_sup exX this,
|
||||
obtain i [H' (Hi : X i = x')], from H₁x',
|
||||
have Hi' : ∀ j, j ≥ i → sX - ε < X j, from
|
||||
take j, assume Hj, lt_of_lt_of_le (Hi⁻¹ ▸ H₂x') (nondecX Hj),
|
||||
exists.intro i
|
||||
(take j, assume Hj : j ≥ i,
|
||||
have X j - sX ≤ 0, from sub_nonpos_of_le (Xle j),
|
||||
have eq₁ : abs (X j - sX) = sX - X j, using this, by rewrite [abs_of_nonpos this, neg_sub],
|
||||
have sX - ε < X j, from lt_of_lt_of_le (Hi⁻¹ ▸ H₂x') (nondecX Hj),
|
||||
have sX < X j + ε, from lt_add_of_sub_lt_right this,
|
||||
have sX - X j < ε, from sub_lt_left_of_lt_add this,
|
||||
show (abs (X j - sX)) < ε, using eq₁ this, by rewrite eq₁; exact this)
|
||||
|
||||
definition nonincreasing (X : ℕ → ℝ) : Prop := ∀ ⦃i j⦄, i ≤ j → X i ≥ X j
|
||||
|
||||
proposition nodecreasing_of_nonincreasing_neg (nonincX : nonincreasing (λ n, - X n)) :
|
||||
nondecreasing (λ n, X n) :=
|
||||
take i j, suppose i ≤ j,
|
||||
show X i ≤ X j, from le_of_neg_le_neg (nonincX this)
|
||||
|
||||
proposition noincreasing_neg_of_nondecreasing (nondecX : nondecreasing X) :
|
||||
nonincreasing (λ n, - X n) :=
|
||||
take i j, suppose i ≤ j,
|
||||
show - X i ≥ - X j, from neg_le_neg (nondecX this)
|
||||
|
||||
proposition nonincreasing_neg_iff (X : ℕ → ℝ) : nonincreasing (λ n, - X n) ↔ nondecreasing X :=
|
||||
iff.intro nodecreasing_of_nonincreasing_neg noincreasing_neg_of_nondecreasing
|
||||
|
||||
proposition nonincreasing_of_nondecreasing_neg (nondecX : nondecreasing (λ n, - X n)) :
|
||||
nonincreasing (λ n, X n) :=
|
||||
take i j, suppose i ≤ j,
|
||||
show X i ≥ X j, from le_of_neg_le_neg (nondecX this)
|
||||
|
||||
proposition nodecreasing_neg_of_nonincreasing (nonincX : nonincreasing X) :
|
||||
nondecreasing (λ n, - X n) :=
|
||||
take i j, suppose i ≤ j,
|
||||
show - X i ≤ - X j, from neg_le_neg (nonincX this)
|
||||
|
||||
proposition nondecreasing_neg_iff (X : ℕ → ℝ) : nondecreasing (λ n, - X n) ↔ nonincreasing X :=
|
||||
iff.intro nonincreasing_of_nondecreasing_neg nodecreasing_neg_of_nonincreasing
|
||||
|
||||
proposition nonincreasing_of_forall_succ_le (H : ∀ i, X (succ i) ≤ X i) : nonincreasing X :=
|
||||
begin
|
||||
rewrite -nondecreasing_neg_iff,
|
||||
show nondecreasing (λ n : ℕ, - X n), from
|
||||
nondecreasing_of_forall_le_succ (take i, neg_le_neg (H i))
|
||||
end
|
||||
|
||||
proposition converges_to_seq_inf_of_nonincreasing (nonincX : nonincreasing X) {b : ℝ}
|
||||
(Hb : ∀ i, b ≤ X i) : X ⟶ inf (X '[univ]) in ℕ :=
|
||||
have H₁ : ∃ x, x ∈ X '[univ], from exists.intro (X 0) (mem_image_of_mem X !mem_univ),
|
||||
have H₂ : ∀ x, x ∈ X '[univ] → b ≤ x, from
|
||||
(take x, assume H,
|
||||
obtain i [Hi₁ (Hi₂ : X i = x)], from H,
|
||||
show b ≤ x, by rewrite -Hi₂; apply Hb i),
|
||||
have H₃ : {x : ℝ | -x ∈ X '[univ]} = {x : ℝ | x ∈ (λ n, -X n) '[univ]}, from calc
|
||||
{x : ℝ | -x ∈ X '[univ]} = (λ y, -y) '[X '[univ]] : !image_neg_eq⁻¹
|
||||
... = {x : ℝ | x ∈ (λ n, -X n) '[univ]} : !image_compose⁻¹,
|
||||
have H₄ : ∀ i, - X i ≤ - b, from take i, neg_le_neg (Hb i),
|
||||
begin+
|
||||
rewrite [-neg_converges_to_seq_iff, -sup_neg H₁ H₂, H₃, -nondecreasing_neg_iff at nonincX],
|
||||
apply converges_to_seq_sup_of_nondecreasing nonincX H₄
|
||||
end
|
||||
|
||||
end monotone_sequences
|
||||
|
||||
section xn
|
||||
open nat set
|
||||
|
||||
theorem pow_converges_to_seq_zero {x : ℝ} (H : abs x < 1) :
|
||||
(λ n, x^n) ⟶ 0 in ℕ :=
|
||||
suffices H' : (λ n, (abs x)^n) ⟶ 0 in ℕ, from
|
||||
have (λ n, (abs x)^n) = (λ n, abs (x^n)), from funext (take n, !abs_pow⁻¹),
|
||||
using this,
|
||||
by rewrite this at H'; exact converges_to_seq_zero_of_abs_converges_to_seq_zero H',
|
||||
let aX := (λ n, (abs x)^n),
|
||||
iaX := inf (aX '[univ]),
|
||||
asX := (λ n, (abs x)^(succ n)) in
|
||||
have noninc_aX : nonincreasing aX, from
|
||||
nonincreasing_of_forall_succ_le
|
||||
(take i,
|
||||
have (abs x) * (abs x)^i ≤ 1 * (abs x)^i,
|
||||
from mul_le_mul_of_nonneg_right (le_of_lt H) (!pow_nonneg_of_nonneg !abs_nonneg),
|
||||
show (abs x) * (abs x)^i ≤ (abs x)^i, from !one_mul ▸ this),
|
||||
have bdd_aX : ∀ i, 0 ≤ aX i, from take i, !pow_nonneg_of_nonneg !abs_nonneg,
|
||||
have aXconv : aX ⟶ iaX in ℕ, from converges_to_seq_inf_of_nonincreasing noninc_aX bdd_aX,
|
||||
have asXconv : asX ⟶ iaX in ℕ, from metric_space.converges_to_seq_offset_succ aXconv,
|
||||
have asXconv' : asX ⟶ (abs x) * iaX in ℕ, from mul_left_converges_to_seq (abs x) aXconv,
|
||||
have iaX = (abs x) * iaX, from converges_to_seq_unique asXconv asXconv',
|
||||
have iaX = 0, from eq_zero_of_mul_eq_self_left (ne_of_lt H) this⁻¹,
|
||||
show aX ⟶ 0 in ℕ, from this ▸ aXconv
|
||||
|
||||
end xn
|
||||
|
||||
section continuous
|
||||
|
||||
|
|
@ -222,7 +556,7 @@ theorem neg_on_nbhd_of_cts_of_neg {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ
|
|||
intro y Hy,
|
||||
let Hy' := and.right Hδ y Hy,
|
||||
let Hlt := sub_lt_of_abs_sub_lt_left Hy',
|
||||
let Hlt' := lt_add_of_sub_lt_right _ _ _ Hlt,
|
||||
let Hlt' := lt_add_of_sub_lt_right Hlt,
|
||||
rewrite [-sub_eq_add_neg at Hlt', sub_self at Hlt'],
|
||||
assumption
|
||||
end
|
||||
|
|
@ -294,15 +628,15 @@ private theorem ex_delta_lt {x : ℝ} (Hx : f x < 0) (Hxb : x < b) : ∃ δ :
|
|||
existsi (b - x) / 2,
|
||||
split,
|
||||
{apply div_pos_of_pos_of_pos,
|
||||
exact sub_pos_of_lt _ _ Hxb,
|
||||
exact sub_pos_of_lt Hxb,
|
||||
exact two_pos},
|
||||
split,
|
||||
{apply add_midpoint Hxb},
|
||||
{apply and.right Hδ,
|
||||
rewrite [sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg,
|
||||
abs_of_pos (div_pos_of_pos_of_pos (sub_pos_of_lt _ _ Hxb) two_pos)],
|
||||
abs_of_pos (div_pos_of_pos_of_pos (sub_pos_of_lt Hxb) two_pos)],
|
||||
apply lt_of_lt_of_le,
|
||||
apply div_two_lt_of_pos (sub_pos_of_lt _ _ Hxb),
|
||||
apply div_two_lt_of_pos (sub_pos_of_lt Hxb),
|
||||
apply sub_left_le_of_le_add,
|
||||
apply le_of_not_gt Haδ}}
|
||||
end
|
||||
|
|
@ -402,15 +736,15 @@ private theorem intermediate_value_incr_aux2 : ∃ δ : ℝ, δ > 0 ∧ a + δ <
|
|||
existsi (b - a) / 2,
|
||||
split,
|
||||
{apply div_pos_of_pos_of_pos,
|
||||
exact sub_pos_of_lt _ _ Hab,
|
||||
exact sub_pos_of_lt Hab,
|
||||
exact two_pos},
|
||||
split,
|
||||
{apply add_midpoint Hab},
|
||||
{apply and.right Hδ,
|
||||
rewrite [sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg,
|
||||
abs_of_pos (div_pos_of_pos_of_pos (sub_pos_of_lt _ _ Hab) two_pos)],
|
||||
abs_of_pos (div_pos_of_pos_of_pos (sub_pos_of_lt Hab) two_pos)],
|
||||
apply lt_of_lt_of_le,
|
||||
apply div_two_lt_of_pos (sub_pos_of_lt _ _ Hab),
|
||||
apply div_two_lt_of_pos (sub_pos_of_lt Hab),
|
||||
apply sub_left_le_of_le_add,
|
||||
apply le_of_not_gt Haδ}}
|
||||
end
|
||||
|
|
@ -440,8 +774,8 @@ theorem intermediate_value_incr_zero : ∃ c, a < c ∧ c < b ∧ f c = 0 :=
|
|||
intro x Hx,
|
||||
apply le_of_not_gt,
|
||||
intro Hxgt,
|
||||
have Hxgt' : b - x < δ, from sub_lt_of_sub_lt _ _ _ Hxgt,
|
||||
rewrite -(abs_of_pos (sub_pos_of_lt _ _ (and.left Hx))) at Hxgt',
|
||||
have Hxgt' : b - x < δ, from sub_lt_of_sub_lt Hxgt,
|
||||
rewrite -(abs_of_pos (sub_pos_of_lt (and.left Hx))) at Hxgt',
|
||||
let Hxgt'' := and.right Hδ _ Hxgt',
|
||||
exact not_lt_of_ge (le_of_lt Hxgt'') (and.right Hx)},
|
||||
{exact sup_fn_interval}
|
||||
|
|
@ -468,8 +802,8 @@ theorem intermediate_value_decr_zero {f : ℝ → ℝ} (Hf : continuous f) {a b
|
|||
|
||||
theorem intermediate_value_incr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) {v : ℝ}
|
||||
(Hav : f a < v) (Hbv : f b > v) : ∃ c, a < c ∧ c < b ∧ f c = v :=
|
||||
have Hav' : f a - v < 0, from sub_neg_of_lt _ _ Hav,
|
||||
have Hbv' : f b - v > 0, from sub_pos_of_lt _ _ Hbv,
|
||||
have Hav' : f a - v < 0, from sub_neg_of_lt Hav,
|
||||
have Hbv' : f b - v > 0, from sub_pos_of_lt Hbv,
|
||||
have Hcon : continuous (λ x, f x - v), from translate_continuous_of_continuous Hf _,
|
||||
have Hiv : ∃ c, a < c ∧ c < b ∧ f c - v = 0, from intermediate_value_incr_zero Hcon Hab Hav' Hbv',
|
||||
obtain c Hc, from Hiv,
|
||||
|
|
@ -478,8 +812,8 @@ theorem intermediate_value_incr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ
|
|||
|
||||
theorem intermediate_value_decr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) {v : ℝ}
|
||||
(Hav : f a > v) (Hbv : f b < v) : ∃ c, a < c ∧ c < b ∧ f c = v :=
|
||||
have Hav' : f a - v > 0, from sub_pos_of_lt _ _ Hav,
|
||||
have Hbv' : f b - v < 0, from sub_neg_of_lt _ _ Hbv,
|
||||
have Hav' : f a - v > 0, from sub_pos_of_lt Hav,
|
||||
have Hbv' : f b - v < 0, from sub_neg_of_lt Hbv,
|
||||
have Hcon : continuous (λ x, f x - v), from translate_continuous_of_continuous Hf _,
|
||||
have Hiv : ∃ c, a < c ∧ c < b ∧ f c - v = 0, from intermediate_value_decr_zero Hcon Hab Hav' Hbv',
|
||||
obtain c Hc, from Hiv,
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue