michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor/feat(library/theories/analysis/*): reorganize analysis library and add some theorems

Browse source
This commit is contained in:
Jeremy Avigad 2016-01-14 23:57:27 -05:00 committed by Leonardo de Moura
parent 98319139d9
commit 86fc326e08
6 changed files with 603 additions and 582 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
library/algebra/module.lean
View file

@ -18,7 +18,7 @@ structure left_module [class] (R M : Type) [ringR : ring R]
extends has_scalar R M, add_comm_group M :=
(smul_left_distrib : ∀ (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y)))
(smul_right_distrib : ∀ (r s : R) (x : M), smul (ring.add r s) x = (add (smul r x) (smul s x)))
(smul_mul : ∀ r s x, smul (mul r s) x = smul r (smul s x))
(mul_smul : ∀ r s x, smul (mul r s) x = smul r (smul s x))
(one_smul : ∀ x, smul one x = x)
section left_module
@ -32,11 +32,11 @@ section left_module
proposition smul_left_distrib (a : R) (u v : M) : a • (u + v) = a • u + a • v :=
!left_module.smul_left_distrib
proposition smul_right_distrib (a b : R) (u : M) : (a + b)•u = a•u + b•u :=
proposition smul_right_distrib (a b : R) (u : M) : (a + b) • u = a • u + b • u :=
!left_module.smul_right_distrib
proposition smul_mul (a : R) (b : R) (u : M) : (a * b) • u = a • (b • u) :=
!left_module.smul_mul
proposition mul_smul (a : R) (b : R) (u : M) : (a * b) • u = a • (b • u) :=
!left_module.mul_smul
proposition one_smul (u : M) : (1 : R) • u = u := !left_module.one_smul
@ -53,6 +53,15 @@ section left_module
proposition neg_one_smul (u : M) : -(1 : R) • u = -u :=
by rewrite [neg_smul, one_smul]
proposition smul_neg (a : R) (u : M) : a • (-u) = -(a • u) :=
by rewrite [-neg_one_smul, -mul_smul, mul_neg_one_eq_neg, neg_smul]
proposition smul_sub_left_distrib (a : R) (u v : M) : a • (u - v) = a • u - a • v :=
by rewrite [sub_eq_add_neg, smul_left_distrib, smul_neg]
proposition sub_smul_right_distrib (a b : R) (v : M) : (a - b) • v = a • v - b • v :=
by rewrite [sub_eq_add_neg, smul_right_distrib, neg_smul]
end left_module
/- linear maps -/

3
library/theories/analysis/analysis.md
View file

@ -2,5 +2,6 @@ theories.analysis
=================
* [metric_space](metric_space.lean)
* [normed_space](normed_space.lean)
* [real_limit](real_limit.lean)
* [normed_space](normed_space.lean)
* [ivt](ivt.lean) : the intermediate value theorem

237
library/theories/analysis/ivt.lean Normal file
View file

@ -0,0 +1,237 @@
/-
Copyright (c) 2015 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Y. Lewis
The intermediate value theorem.
-/
import .real_limit
open real analysis set classical
noncomputable theory
private definition inter_sup (a b : ℝ) (f : ℝ → ℝ) := sup {x | x < b ∧ f x < 0}
section
parameters {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) (Ha : f a < 0) (Hb : f b > 0)
include Hf Ha Hb Hab
private theorem Hinh : ∃ x, x ∈ {x | x < b ∧ f x < 0} := exists.intro a (and.intro Hab Ha)
private theorem Hmem : ∀ x, x ∈ {x | x < b ∧ f x < 0} → x ≤ b := λ x Hx, le_of_lt (and.left Hx)
private theorem Hsupleb : inter_sup a b f ≤ b := sup_le (Hinh) Hmem
local notation 2 := of_num 1 + of_num 1
private theorem ex_delta_lt {x : ℝ} (Hx : f x < 0) (Hxb : x < b) : ∃ δ : ℝ, δ > 0 ∧ x + δ < b ∧ f (x + δ) < 0 :=
begin
let Hcont := neg_on_nbhd_of_cts_of_neg Hf Hx,
cases Hcont with δ Hδ,
{cases em (x + δ < b) with Haδ Haδ,
existsi δ / 2,
split,
{exact div_pos_of_pos_of_pos (and.left Hδ) two_pos},
split,
{apply lt.trans,
apply add_lt_add_left,
exact div_two_lt_of_pos (and.left Hδ),
exact Haδ},
{apply and.right Hδ,
krewrite [abs_sub, sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg,
abs_of_pos (div_pos_of_pos_of_pos (and.left Hδ) two_pos)],
exact div_two_lt_of_pos (and.left Hδ)},
existsi (b - x) / 2,
split,
{apply div_pos_of_pos_of_pos,
exact sub_pos_of_lt Hxb,
exact two_pos},
split,
{apply add_midpoint Hxb},
{apply and.right Hδ,
krewrite [abs_sub, 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)],
apply lt_of_lt_of_le,
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
private lemma sup_near_b {δ : ℝ} (Hpos : 0 < δ)
(Hgeb : inter_sup a b f + δ / 2 ≥ b) : abs (inter_sup a b f - b) < δ :=
begin
apply abs_lt_of_lt_of_neg_lt,
apply sub_lt_left_of_lt_add,
apply lt_of_le_of_lt,
apply Hsupleb,
apply lt_add_of_pos_right Hpos,
rewrite neg_sub,
apply sub_lt_left_of_lt_add,
apply lt_of_le_of_lt,
apply Hgeb,
apply add_lt_add_left,
apply div_two_lt_of_pos Hpos
end
private lemma delta_of_lt (Hflt : f (inter_sup a b f) < 0) :
∃ δ : ℝ, δ > 0 ∧ inter_sup a b f + δ < b ∧ f (inter_sup a b f + δ) < 0 :=
if Hlt : inter_sup a b f < b then ex_delta_lt Hflt Hlt else
begin
let Heq := eq_of_le_of_ge Hsupleb (le_of_not_gt Hlt),
apply absurd Hflt,
apply not_lt_of_ge,
apply le_of_lt,
rewrite Heq,
exact Hb
end
private theorem sup_fn_interval_aux1 : f (inter_sup a b f) ≥ 0 :=
have ¬ f (inter_sup a b f) < 0, from
(suppose f (inter_sup a b f) < 0,
obtain δ Hδ, from delta_of_lt this,
have inter_sup a b f + δ ∈ {x | x < b ∧ f x < 0},
from and.intro (and.left (and.right Hδ)) (and.right (and.right Hδ)),
have ¬ inter_sup a b f < inter_sup a b f + δ,
from not_lt_of_ge (le_sup this Hmem),
show false, from this (lt_add_of_pos_right (and.left Hδ))),
le_of_not_gt this
private theorem sup_fn_interval_aux2 : f (inter_sup a b f) ≤ 0 :=
have ¬ f (inter_sup a b f) > 0, from
(assume Hfsup : f (inter_sup a b f) > 0,
obtain δ Hδ, from pos_on_nbhd_of_cts_of_pos Hf Hfsup,
have ∀ x, x ∈ {x | x < b ∧ f x < 0} → x ≤ inter_sup a b f - δ / 2, from
(take x, assume Hxset : x ∈ {x | x < b ∧ f x < 0},
have ¬ x > inter_sup a b f - δ / 2, from
(assume Hngt,
have Habs : abs (x - inter_sup a b f) < δ, begin
rewrite abs_sub,
apply abs_lt_of_lt_of_neg_lt,
apply sub_lt_of_sub_lt,
apply gt.trans,
exact Hngt,
apply sub_lt_sub_left,
exact div_two_lt_of_pos (and.left Hδ),
rewrite neg_sub,
apply lt_of_le_of_lt,
rotate 1,
apply and.left Hδ,
apply sub_nonpos_of_le,
apply le_sup,
exact Hxset,
exact Hmem
end,
have f x > 0, from and.right Hδ x Habs,
show false, from (not_lt_of_gt this) (and.right Hxset)),
le_of_not_gt this),
have Hle : inter_sup a b f ≤ inter_sup a b f - δ / 2, from sup_le Hinh this,
show false, from not_le_of_gt
(sub_lt_of_pos _ (div_pos_of_pos_of_pos (and.left Hδ) (two_pos))) Hle),
le_of_not_gt this
private theorem sup_fn_interval : f (inter_sup a b f) = 0 :=
eq_of_le_of_ge sup_fn_interval_aux2 sup_fn_interval_aux1
private theorem intermediate_value_incr_aux2 : ∃ δ : ℝ, δ > 0 ∧ a + δ < b ∧ f (a + δ) < 0 :=
begin
let Hcont := neg_on_nbhd_of_cts_of_neg Hf Ha,
cases Hcont with δ Hδ,
{cases em (a + δ < b) with Haδ Haδ,
existsi δ / 2,
split,
{exact div_pos_of_pos_of_pos (and.left Hδ) two_pos},
split,
{apply lt.trans,
apply add_lt_add_left,
exact div_two_lt_of_pos (and.left Hδ),
exact Haδ},
{apply and.right Hδ,
krewrite [abs_sub, sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg,
abs_of_pos (div_pos_of_pos_of_pos (and.left Hδ) two_pos)],
exact div_two_lt_of_pos (and.left Hδ)},
existsi (b - a) / 2,
split,
{apply div_pos_of_pos_of_pos,
exact sub_pos_of_lt Hab,
exact two_pos},
split,
{apply add_midpoint Hab},
{apply and.right Hδ,
krewrite [abs_sub, 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)],
apply lt_of_lt_of_le,
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
theorem intermediate_value_incr_zero : ∃ c, a < c ∧ c < b ∧ f c = 0 :=
begin
existsi inter_sup a b f,
split,
{cases intermediate_value_incr_aux2 with δ Hδ,
apply lt_of_lt_of_le,
apply lt_add_of_pos_right,
exact and.left Hδ,
apply le_sup,
exact and.right Hδ,
intro x Hx,
apply le_of_lt,
exact and.left Hx},
split,
{cases pos_on_nbhd_of_cts_of_pos Hf Hb with δ Hδ,
apply lt_of_le_of_lt,
rotate 1,
apply sub_lt_of_pos,
exact and.left Hδ,
rotate_right 1,
apply sup_le,
exact exists.intro a (and.intro Hab Ha),
intro x Hx,
apply le_of_not_gt,
intro Hxgt,
have Hxgt' : b - x < δ, from sub_lt_of_sub_lt Hxgt,
krewrite [-(abs_of_pos (sub_pos_of_lt (and.left Hx))) at Hxgt', abs_sub at Hxgt'],
note Hxgt'' := and.right Hδ _ Hxgt',
exact not_lt_of_ge (le_of_lt Hxgt'') (and.right Hx)},
{exact sup_fn_interval}
end
end
theorem intermediate_value_decr_zero {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b)
(Ha : f a > 0) (Hb : f b < 0) : ∃ c, a < c ∧ c < b ∧ f c = 0 :=
begin
have Ha' : - f a < 0, from neg_neg_of_pos Ha,
have Hb' : - f b > 0, from neg_pos_of_neg Hb,
have Hcon : continuous (λ x, - f x), from continuous_neg_of_continuous Hf,
let Hiv := intermediate_value_incr_zero Hcon Hab Ha' Hb',
cases Hiv with c Hc,
existsi c,
split,
exact and.left Hc,
split,
exact and.left (and.right Hc),
apply eq_zero_of_neg_eq_zero,
apply and.right (and.right Hc)
end
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 Hcon : continuous (λ x, f x - v), from continuous_offset_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,
exists.intro c
(and.intro (and.left Hc) (and.intro (and.left (and.right Hc)) (eq_of_sub_eq_zero (and.right (and.right Hc)))))
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 Hcon : continuous (λ x, f x - v), from continuous_offset_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,
exists.intro c
(and.intro (and.left Hc) (and.intro (and.left (and.right Hc)) (eq_of_sub_eq_zero (and.right (and.right Hc)))))

84
library/theories/analysis/metric_space.lean
View file

@ -6,24 +6,35 @@ Author: Jeremy Avigad
Metric spaces.
-/
import data.real.division
open real eq.ops classical
open nat real eq.ops classical
structure metric_space [class] (M : Type) : Type :=
(dist : M → M → ℝ)
(dist_self : ∀ x : M, dist x x = 0)
(eq_of_dist_eq_zero : ∀ {x y : M}, dist x y = 0 → x = y)
(dist_comm : ∀ x y : M, dist x y = dist y x)
(dist_triangle : ∀ x y z : M, dist x y + dist y z ≥ dist x z)
(dist_triangle : ∀ x y z : M, dist x z ≤ dist x y + dist y z)
namespace metric_space
namespace analysis
section metric_space_M
variables {M : Type} [strucM : metric_space M]
include strucM
variables {M : Type} [metric_space M]
definition dist (x y : M) : ℝ := metric_space.dist x y
proposition dist_self (x : M) : dist x x = 0 := metric_space.dist_self x
proposition eq_of_dist_eq_zero {x y : M} (H : dist x y = 0) : x = y :=
metric_space.eq_of_dist_eq_zero H
proposition dist_comm (x y : M) : dist x y = dist y x := metric_space.dist_comm x y
proposition dist_eq_zero_iff (x y : M) : dist x y = 0 ↔ x = y :=
iff.intro eq_of_dist_eq_zero (suppose x = y, this ▸ !dist_self)
proposition dist_triangle (x y z : M) : dist x z ≤ dist x y + dist y z :=
metric_space.dist_triangle x y z
proposition dist_nonneg (x y : M) : 0 ≤ dist x y :=
have dist x y + dist y x ≥ 0, by rewrite -(dist_self x); apply dist_triangle,
have 2 * dist x y ≥ 0, using this,
@ -36,8 +47,6 @@ lt_of_le_of_ne !dist_nonneg (suppose 0 = dist x y, H (iff.mp !dist_eq_zero_iff t
proposition eq_of_forall_dist_le {x y : M} (H : ∀ ε, ε > 0 → dist x y ≤ ε) : x = y :=
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 :=
@ -133,7 +142,7 @@ 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
@converges_to_seq_of_converges_to_seq_offset M _ X y 1 H
proposition converges_to_seq_offset_iff (X : ℕ → M) (y : M) (k : ℕ) :
((λ n, X (n + k)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
@ -180,7 +189,7 @@ variables {M N : Type} [strucM : metric_space M] [strucN : metric_space N]
include strucM strucN
definition converges_to_at (f : M → N) (y : N) (x : M) :=
∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ x', x ≠ x' ∧ dist x x' < δ → dist (f x') y < ε
∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ≠ x ∧ dist x' x < δ → dist (f x') (f x) < ε
notation f `⟶` y `at` x := converges_to_at f y x
@ -194,25 +203,38 @@ proposition converges_to_limit_at (f : M → N) (x : M) [H : converges_at f x] :
(f ⟶ limit_at f x at x) :=
some_spec H
definition continuous_at (f : M → N) (x : M) := converges_to_at f (f x) x
/- continuity at a point -/
definition continuous (f : M → N) := ∀ x, continuous_at f x
definition continuous_at (f : M → N) (x : M) :=
∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε
theorem continuous_at_spec {f : M → N} {x : M} (Hf : continuous_at f x) :
∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ x', dist x x' < δ → dist (f x') (f x) < ε :=
theorem continuous_at_of_converges_to_at {f : M → N} {x : M} (Hf : f ⟶ f x at x) :
continuous_at f x :=
take ε, suppose ε > 0,
obtain δ Hδ, from Hf this,
exists.intro δ (and.intro
(and.left Hδ)
(take x', suppose dist x x' < δ,
if Heq : x = x' then
by rewrite [Heq, dist_self]; assumption
(take x', suppose dist x' x < δ,
if Heq : x' = x then
by rewrite [-Heq, dist_self]; assumption
else
(suffices dist x x' < δ, from and.right Hδ x' (and.intro Heq this),
(suffices dist x' x < δ, from and.right Hδ x' (and.intro Heq this),
this)))
theorem image_seq_converges_of_converges [instance] (X : ℕ → M) [HX : converges_seq X] {f : M → N}
(Hf : continuous f) :
theorem converges_to_at_of_continuous_at {f : M → N} {x : M} (Hf : continuous_at f x) :
f ⟶ f x at x :=
take ε, suppose ε > 0,
obtain δ Hδ, from Hf this,
exists.intro δ (and.intro
(and.left Hδ)
(take x',
assume H : x' ≠ x ∧ dist x' x < δ,
show dist (f x') (f x) < ε, from and.right Hδ x' (and.right H)))
definition continuous (f : M → N) : Prop := ∀ x, continuous_at f x
theorem converges_seq_of_comp [instance] (X : ℕ → M) [HX : converges_seq X] {f : M → N}
(Hf : continuous f) :
converges_seq (λ n, f (X n)) :=
begin
cases HX with xlim Hxlim,
@ -228,23 +250,33 @@ theorem image_seq_converges_of_converges [instance] (X : ℕ → M) [HX : conver
rewrite [a, dist_self],
assumption,
apply and.right Hδ,
split,
exact a,
rewrite dist_comm,
apply HB Hn
end
end metric_space_M_N
end metric_space
end analysis
/- complete metric spaces -/
open metric_space
structure complete_metric_space [class] (M : Type) extends metricM : metric_space M : Type :=
(complete : ∀ X, @cauchy M metricM X → @converges_seq M metricM X)
(complete : ∀ X, @analysis.cauchy M metricM X → @analysis.converges_seq M metricM X)
namespace analysis
proposition complete (M : Type) [cmM : complete_metric_space M] {X : ℕ → M} (H : cauchy X) :
converges_seq X :=
complete_metric_space.complete X H
end analysis
/- the reals form a metris space -/
noncomputable definition metric_space_real [instance] : metric_space ℝ :=
⦃ metric_space,
dist := λ x y, abs (x - y),
dist_self := λ x, abstract by rewrite [sub_self, abs_zero] end,
eq_of_dist_eq_zero := λ x y, eq_of_abs_sub_eq_zero,
dist_comm := abs_sub,
dist_triangle := abs_sub_le
⦄

192
library/theories/analysis/normed_space.lean
View file

@ -5,17 +5,18 @@ Author: Jeremy Avigad
Normed spaces.
-/
import algebra.module .real_limit
open real
import algebra.module .metric_space
open real nat classical
noncomputable theory
structure has_norm [class] (M : Type) : Type :=
(norm : M → ℝ)
definition norm {M : Type} [has_normM : has_norm M] (v : M) : ℝ := has_norm.norm v
namespace analysis
definition norm {M : Type} [has_normM : has_norm M] (v : M) : ℝ := has_norm.norm v
notation `∥`v`∥` := norm v
notation `∥`v`∥` := norm v
end analysis
-- where is the right place to put this?
structure real_vector_space [class] (V : Type) extends vector_space ℝ V
@ -26,9 +27,7 @@ structure normed_vector_space [class] (V : Type) extends real_vector_space V, ha
(norm_triangle : ∀ u v, norm (add u v) ≤ norm u + norm v)
(norm_smul : ∀ (a : ℝ) (v : V), norm (smul a v) = abs a * norm v)
-- what namespace should we put this in?
section normed_vector_space
namespace analysis
variable {V : Type}
variable [normed_vector_space V]
@ -46,28 +45,33 @@ section normed_vector_space
proposition norm_neg (v : V) : ∥ -v ∥ = ∥ v ∥ :=
have abs (1 : ℝ) = 1, from abs_of_nonneg zero_le_one,
by+ rewrite [-@neg_one_smul ℝ V, norm_smul, abs_neg, this, one_mul]
end analysis
section
private definition nvs_dist (u v : V) := ∥ u - v ∥
section
open analysis
variable {V : Type}
variable [normed_vector_space V]
private lemma nvs_dist_self (u : V) : nvs_dist u u = 0 :=
by rewrite [↑nvs_dist, sub_self, norm_zero]
private definition nvs_dist [reducible] (u v : V) := ∥ u - v ∥
private lemma eq_of_nvs_dist_eq_zero (u v : V) (H : nvs_dist u v = 0) : u = v :=
have u - v = 0, from eq_zero_of_norm_eq_zero H,
eq_of_sub_eq_zero this
private lemma nvs_dist_self (u : V) : nvs_dist u u = 0 :=
by rewrite [↑nvs_dist, sub_self, norm_zero]
private lemma nvs_dist_triangle (u v w : V) : nvs_dist u w ≤ nvs_dist u v + nvs_dist v w :=
calc
nvs_dist u w = ∥ (u - v) + (v - w) ∥ : by rewrite [↑nvs_dist, *sub_eq_add_neg, add.assoc,
neg_add_cancel_left]
... ≤ ∥ u - v ∥ + ∥ v - w ∥ : norm_triangle
private lemma eq_of_nvs_dist_eq_zero (u v : V) (H : nvs_dist u v = 0) : u = v :=
have u - v = 0, from eq_zero_of_norm_eq_zero H,
eq_of_sub_eq_zero this
private lemma nvs_dist_comm (u v : V) : nvs_dist u v = nvs_dist v u :=
by rewrite [↑nvs_dist, -norm_neg, neg_sub]
end
private lemma nvs_dist_triangle (u v w : V) : nvs_dist u w ≤ nvs_dist u v + nvs_dist v w :=
calc
nvs_dist u w = ∥ (u - v) + (v - w) ∥ : by rewrite [↑nvs_dist, *sub_eq_add_neg, add.assoc,
neg_add_cancel_left]
... ≤ ∥ u - v ∥ + ∥ v - w ∥ : norm_triangle
private lemma nvs_dist_comm (u v : V) : nvs_dist u v = nvs_dist v u :=
by rewrite [↑nvs_dist, -norm_neg, neg_sub]
definition normed_vector_space_to_metric_space [reducible] [trans_instance] : metric_space V :=
definition normed_vector_space_to_metric_space [reducible] [trans_instance]
(V : Type) [nvsV : normed_vector_space V] :
metric_space V :=
⦃ metric_space,
dist := nvs_dist,
dist_self := nvs_dist_self,
@ -75,42 +79,126 @@ section normed_vector_space
dist_comm := nvs_dist_comm,
dist_triangle := nvs_dist_triangle
⦄
end normed_vector_space
open nat
proposition converges_to_seq_norm_elim {X : ℕ → V} {x : V} (H : X ⟶ x in ℕ) :
∀ {ε : ℝ}, ε > 0 → ∃ N₁ : ℕ, ∀ {n : ℕ}, n ≥ N₁ → ∥ X n - x ∥ < ε := H
proposition dist_eq_norm_sub (u v : V) : dist u v = ∥ u - v ∥ := rfl
proposition norm_eq_dist_zero (u : V) : ∥ u ∥ = dist u 0 :=
by rewrite [dist_eq_norm_sub, sub_zero]
proposition norm_nonneg (u : V) : ∥ u ∥ ≥ 0 :=
by rewrite norm_eq_dist_zero; apply !dist_nonneg
end
structure banach_space [class] (V : Type) extends nvsV : normed_vector_space V :=
(complete : ∀ X, @metric_space.cauchy V (@normed_vector_space_to_metric_space V nvsV) X →
@metric_space.converges_seq V (@normed_vector_space_to_metric_space V nvsV) X)
(complete : ∀ X, @analysis.cauchy V (@normed_vector_space_to_metric_space V nvsV) X →
@analysis.converges_seq V (@normed_vector_space_to_metric_space V nvsV) X)
definition banach_space_to_metric_space [reducible] [trans_instance] (V : Type) [bsV : banach_space V] :
definition banach_space_to_metric_space [reducible] [trans_instance]
(V : Type) [bsV : banach_space V] :
complete_metric_space V :=
⦃ complete_metric_space, normed_vector_space_to_metric_space,
⦃ complete_metric_space, normed_vector_space_to_metric_space V,
complete := banach_space.complete
⦄
section
open metric_space
namespace analysis
variable {V : Type}
variable [normed_vector_space V]
example (V : Type) (vsV : banach_space V) (X : ℕ → V) (H : cauchy X) : converges_seq X :=
complete V H
end
variables {X Y : ℕ → V}
variables {x y : V}
/- the real numbers themselves can be viewed as a banach space -/
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₁ → ∥ X n - x ∥ < ε / 2),
from converges_to_seq_norm_elim HX e2pos,
obtain (N₂ : ℕ) (HN₂ : ∀ {n}, n ≥ N₂ → ∥ Y n - y ∥ < ε / 2),
from converges_to_seq_norm_elim HY e2pos,
let N := max N₁ N₂ in
exists.intro N
(take n,
suppose n ≥ N,
have ngtN₁ : n ≥ N₁, from nat.le_trans !le_max_left `n ≥ N`,
have ngtN₂ : n ≥ N₂, from nat.le_trans !le_max_right `n ≥ N`,
show ∥ (X n + Y n) - (x + y) ∥ < ε, from calc
∥ (X n + Y n) - (x + y) ∥
= ∥ (X n - x) + (Y n - y) ∥ : by rewrite [sub_add_eq_sub_sub, *sub_eq_add_neg,
*add.assoc, add.left_comm (-x)]
... ≤ ∥ X n - x ∥ + ∥ Y n - y ∥ : norm_triangle
... < ε / 2 + ε / 2 : add_lt_add (HN₁ ngtN₁) (HN₂ ngtN₂)
... = ε : add_halves)
definition real_is_real_vector_space [trans_instance] [reducible] : real_vector_space ℝ :=
⦃ real_vector_space, real.discrete_linear_ordered_field,
smul := mul,
smul_left_distrib := left_distrib,
smul_right_distrib := right_distrib,
smul_mul := mul.assoc,
one_smul := one_mul
⦄
private lemma smul_converges_to_seq_aux {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 → norm (X n - x) < ε / abs c), from converges_to_seq_norm_elim HX epos,
exists.intro N
(take n,
suppose n ≥ N,
have H : norm (X n - x) < ε / abs c, from HN this,
show norm (c • X n - c • x) < ε, from calc
norm (c • X n - c • x)
= abs c * norm (X n - x) : by rewrite [-smul_sub_left_distrib, norm_smul]
... < abs c * (ε / abs c) : mul_lt_mul_of_pos_left H abscpos
... = ε : mul_div_cancel' (ne_of_gt abscpos))
definition real_is_banach_space [trans_instance] [reducible] : banach_space ℝ :=
⦃ banach_space, real_is_real_vector_space,
norm := abs,
norm_zero := abs_zero,
eq_zero_of_norm_eq_zero := λ a H, eq_zero_of_abs_eq_zero H,
norm_triangle := abs_add_le_abs_add_abs,
norm_smul := abs_mul,
complete := λ X H, complete ℝ H
⦄
proposition smul_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_smul]),
begin+ rewrite [this, cz, zero_smul], apply converges_to_seq_constant end)
(suppose c ≠ 0, smul_converges_to_seq_aux this HX)
proposition neg_converges_to_seq (HX : X ⟶ x in ℕ) :
(λ n, - X n) ⟶ - x in ℕ :=
take ε, suppose ε > 0,
obtain N (HN : ∀ {n}, n ≥ N → norm (X n - x) < ε), from converges_to_seq_norm_elim HX this,
exists.intro N
(take n,
suppose n ≥ N,
show norm (- X n - (- x)) < ε,
by rewrite [-neg_neg_sub_neg, *neg_neg, norm_neg]; exact HN `n ≥ N`)
proposition neg_converges_to_seq_iff : ((λ 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 norm_converges_to_seq_zero (HX : X ⟶ 0 in ℕ) : (λ n, norm (X n)) ⟶ 0 in ℕ :=
take ε, suppose ε > 0,
obtain N (HN : ∀ n, n ≥ N → norm (X n - 0) < ε), from HX `ε > 0`,
exists.intro N
(take n, assume Hn : n ≥ N,
have norm (X n) < ε, begin rewrite -(sub_zero (X n)), apply HN n Hn end,
show abs (norm (X n) - 0) < ε, using this,
by rewrite [sub_zero, abs_of_nonneg !norm_nonneg]; apply this)
proposition converges_to_seq_zero_of_norm_converges_to_seq_zero
(HX : (λ n, norm (X n)) ⟶ 0 in ℕ) :
X ⟶ 0 in ℕ :=
take ε, suppose ε > 0,
obtain N (HN : ∀ n, n ≥ N → abs (norm (X n) - 0) < ε), from HX `ε > 0`,
exists.intro (N : ℕ)
(take n : ℕ, assume Hn : n ≥ N,
have HN' : abs (norm (X n) - 0) < ε, from HN n Hn,
have norm (X n) < ε,
by+ rewrite [sub_zero at HN', abs_of_nonneg !norm_nonneg at HN']; apply HN',
show norm (X n - 0) < ε, using this,
by rewrite sub_zero; apply this)
proposition norm_converges_to_seq_zero_iff (X : ℕ → V) :
((λ n, norm (X n)) ⟶ 0 in ℕ) ↔ (X ⟶ 0 in ℕ) :=
iff.intro converges_to_seq_zero_of_norm_converges_to_seq_zero norm_converges_to_seq_zero
end analysis

652
library/theories/analysis/real_limit.lean
View file

@ -3,178 +3,21 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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
data.real.complete.
The definitions here are noncomputable, for various reasons:
(1) We rely on the nonconstructive definition of abs.
(2) The theory of the reals uses the "some" operator e.g. to define the ceiling function.
This can't be defined constructively as an operation on the quotient, because
such a function is not continuous.
(3) We use "forall" and "exists" to say that a series converges, rather than carrying
around rates of convergence explicitly. We then use "some" whenever we need to extract
information, such as the limit.
These could be avoided in a constructive theory of analysis, but here we will not
follow that route.
Instantiates the reals as a Banach space.
-/
import .metric_space data.real.complete data.set
open real classical
import .metric_space data.real.complete data.set .normed_space
open real classical analysis nat
noncomputable theory
/- sup and inf -/
-- Expresses completeness, sup, and inf in a manner that is less constructive, but more convenient,
-- than the way it is done in data.real.complete.
-- Issue: real.sup and real.inf conflict with sup and inf in lattice.
-- Perhaps put algebra sup and inf into a namespace?
namespace real
local postfix ⁻¹ := pnat.inv
/- the reals form a metric space -/
protected definition metric_space [instance] : metric_space ℝ :=
⦃ metric_space,
dist := λ x y, abs (x - y),
dist_self := λ x, abstract by rewrite [sub_self, abs_zero] end,
eq_of_dist_eq_zero := λ x y, eq_of_abs_sub_eq_zero,
dist_comm := abs_sub,
dist_triangle := abs_sub_le
⦄
open nat
open [class] rat
definition converges_to_seq (X : ℕ → ℝ) (y : ℝ) : Prop :=
∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε
proposition converges_to_seq.intro {X : ℕ → ℝ} {y : ℝ}
(H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) ≤ ε) :
converges_to_seq X y :=
metric_space.converges_to_seq.intro H
notation X `⟶` y `in` `ℕ` := converges_to_seq X y
definition converges_seq [class] (X : ℕ → ℝ) : Prop := ∃ y, X ⟶ y in ℕ
definition limit_seq (X : ℕ → ℝ) [H : converges_seq X] : ℝ := some H
proposition converges_to_limit_seq (X : ℕ → ℝ) [H : converges_seq X] :
(X ⟶ limit_seq X in ℕ) :=
some_spec H
proposition converges_to_seq_unique {X : ℕ → ℝ} {y₁ y₂ : ℝ}
(H₁ : X ⟶ y₁ in ℕ) (H₂ : X ⟶ y₂ in ℕ) : y₁ = y₂ :=
metric_space.converges_to_seq_unique H₁ H₂
proposition eq_limit_of_converges_to_seq {X : ℕ → ℝ} (y : ℝ) (H : X ⟶ y in ℕ) :
y = @limit_seq X (exists.intro y H) :=
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
section
open pnat subtype
private definition pnat.succ (n : ℕ) : ℕ+ := tag (succ n) !succ_pos
private definition r_seq_of (X : ℕ → ℝ) : r_seq := λ n, X (elt_of n)
private lemma rate_of_cauchy_aux {X : ℕ → ℝ} (H : cauchy X) :
∀ k : ℕ+, ∃ N : ℕ+, ∀ m n : ℕ+,
m ≥ N → n ≥ N → abs (X (elt_of m) - X (elt_of n)) ≤ of_rat k⁻¹ :=
take k : ℕ+,
have H1 : (k⁻¹ > (rat.of_num 0)), from !pnat.inv_pos,
have H2 : (of_rat k⁻¹ > of_rat (rat.of_num 0)), from !of_rat_lt_of_rat_of_lt H1,
obtain (N : ℕ) (H : ∀ m n, m ≥ N → n ≥ N → abs (X m - X n) < of_rat k⁻¹), from H _ H2,
exists.intro (pnat.succ N)
(take m n : ℕ+,
assume Hm : m ≥ (pnat.succ N),
assume Hn : n ≥ (pnat.succ N),
have Hm' : elt_of m ≥ N, begin apply le.trans, apply le_succ, apply Hm end,
have Hn' : elt_of n ≥ N, begin apply le.trans, apply le_succ, apply Hn end,
show abs (X (elt_of m) - X (elt_of n)) ≤ of_rat k⁻¹, from le_of_lt (H _ _ Hm' Hn'))
private definition rate_of_cauchy {X : ℕ → ℝ} (H : cauchy X) (k : ℕ+) : ℕ+ :=
some (rate_of_cauchy_aux H k)
private lemma cauchy_with_rate_of_cauchy {X : ℕ → ℝ} (H : cauchy X) :
cauchy_with_rate (r_seq_of X) (rate_of_cauchy H) :=
take k : ℕ+,
some_spec (rate_of_cauchy_aux H k)
private lemma converges_to_with_rate_of_cauchy {X : ℕ → ℝ} (H : cauchy X) :
∃ l Nb, converges_to_with_rate (r_seq_of X) l Nb :=
begin
apply exists.intro,
apply exists.intro,
apply converges_to_with_rate_of_cauchy_with_rate,
exact cauchy_with_rate_of_cauchy H
end
theorem converges_seq_of_cauchy {X : ℕ → ℝ} (H : cauchy X) : converges_seq X :=
obtain l Nb (conv : converges_to_with_rate (r_seq_of X) l Nb),
from converges_to_with_rate_of_cauchy H,
exists.intro l
(take ε : ℝ,
suppose ε > 0,
obtain (k' : ℕ) (Hn : 1 / succ k' < ε), from archimedean_small `ε > 0`,
let k : ℕ+ := tag (succ k') !succ_pos,
N : ℕ+ := Nb k in
have Hk : real.of_rat k⁻¹ < ε,
by rewrite [↑pnat.inv, of_rat_divide]; exact Hn,
exists.intro (elt_of N)
(take n : ℕ,
assume Hn : n ≥ elt_of N,
let n' : ℕ+ := tag n (nat.lt_of_lt_of_le (has_property N) Hn) in
have abs (X n - l) ≤ real.of_rat k⁻¹, by apply conv k n' Hn,
show abs (X n - l) < ε, from lt_of_le_of_lt this Hk))
protected definition complete_metric_space [reducible] [trans_instance] :
complete_metric_space ℝ :=
⦃complete_metric_space, real.metric_space,
complete := @converges_seq_of_cauchy
⦄
open set
private definition exists_is_sup {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b)) :
@ -299,58 +142,121 @@ have HX : X = {x | -x ∈ negX},
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 real
/- the reals form a complete metric space -/
namespace analysis
theorem dist_eq_abs (x y : real) : dist x y = abs (x - y) := rfl
proposition converges_to_seq_real_intro {X : ℕ → ℝ} {y : ℝ}
(H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε) :
(X ⟶ y in ℕ) := H
proposition converges_to_seq_real_elim {X : ℕ → ℝ} {y : ℝ} (H : X ⟶ y in ℕ) :
∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε := H
proposition converges_to_seq_real_intro' {X : ℕ → ℝ} {y : ℝ}
(H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) ≤ ε) :
converges_to_seq X y :=
converges_to_seq.intro H
open pnat subtype
local postfix ⁻¹ := pnat.inv
private definition pnat.succ (n : ℕ) : ℕ+ := tag (succ n) !succ_pos
private definition r_seq_of (X : ℕ → ℝ) : r_seq := λ n, X (elt_of n)
private lemma rate_of_cauchy_aux {X : ℕ → ℝ} (H : cauchy X) :
∀ k : ℕ+, ∃ N : ℕ+, ∀ m n : ℕ+,
m ≥ N → n ≥ N → abs (X (elt_of m) - X (elt_of n)) ≤ of_rat k⁻¹ :=
take k : ℕ+,
have H1 : (k⁻¹ >[rat] (rat.of_num 0)), from !pnat.inv_pos,
have H2 : (of_rat k⁻¹ > of_rat (rat.of_num 0)), from !of_rat_lt_of_rat_of_lt H1,
obtain (N : ℕ) (H : ∀ m n, m ≥ N → n ≥ N → abs (X m - X n) < of_rat k⁻¹), from H _ H2,
exists.intro (pnat.succ N)
(take m n : ℕ+,
assume Hm : m ≥ (pnat.succ N),
assume Hn : n ≥ (pnat.succ N),
have Hm' : elt_of m ≥ N, begin apply le.trans, apply le_succ, apply Hm end,
have Hn' : elt_of n ≥ N, begin apply le.trans, apply le_succ, apply Hn end,
show abs (X (elt_of m) - X (elt_of n)) ≤ of_rat k⁻¹, from le_of_lt (H _ _ Hm' Hn'))
private definition rate_of_cauchy {X : ℕ → ℝ} (H : cauchy X) (k : ℕ+) : ℕ+ :=
some (rate_of_cauchy_aux H k)
private lemma cauchy_with_rate_of_cauchy {X : ℕ → ℝ} (H : cauchy X) :
cauchy_with_rate (r_seq_of X) (rate_of_cauchy H) :=
take k : ℕ+,
some_spec (rate_of_cauchy_aux H k)
private lemma converges_to_with_rate_of_cauchy {X : ℕ → ℝ} (H : cauchy X) :
∃ l Nb, converges_to_with_rate (r_seq_of X) l Nb :=
begin
apply exists.intro,
apply exists.intro,
apply converges_to_with_rate_of_cauchy_with_rate,
exact cauchy_with_rate_of_cauchy H
end
theorem converges_seq_of_cauchy {X : ℕ → ℝ} (H : cauchy X) : converges_seq X :=
obtain l Nb (conv : converges_to_with_rate (r_seq_of X) l Nb),
from converges_to_with_rate_of_cauchy H,
exists.intro l
(take ε : ℝ,
suppose ε > 0,
obtain (k' : ℕ) (Hn : 1 / succ k' < ε), from archimedean_small `ε > 0`,
let k : ℕ+ := tag (succ k') !succ_pos,
N : ℕ+ := Nb k in
have Hk : real.of_rat k⁻¹ < ε,
by rewrite [↑pnat.inv, of_rat_divide]; exact Hn,
exists.intro (elt_of N)
(take n : ℕ,
assume Hn : n ≥ elt_of N,
let n' : ℕ+ := tag n (nat.lt_of_lt_of_le (has_property N) Hn) in
have abs (X n - l) ≤ real.of_rat k⁻¹, by apply conv k n' Hn,
show abs (X n - l) < ε, from lt_of_le_of_lt this Hk))
end analysis
definition complete_metric_space_real [reducible] [trans_instance] :
complete_metric_space ℝ :=
⦃complete_metric_space, metric_space_real,
complete := @analysis.converges_seq_of_cauchy
⦄
/- the real numbers can be viewed as a banach space -/
definition real_vector_space_real : real_vector_space ℝ :=
⦃ real_vector_space, real.discrete_linear_ordered_field,
smul := mul,
smul_left_distrib := left_distrib,
smul_right_distrib := right_distrib,
mul_smul := mul.assoc,
one_smul := one_mul
⦄
definition banach_space_real [trans_instance] [reducible] : banach_space ℝ :=
⦃ banach_space, real_vector_space_real,
norm := abs,
norm_zero := abs_zero,
eq_zero_of_norm_eq_zero := λ a H, eq_zero_of_abs_eq_zero H,
norm_triangle := abs_add_le_abs_add_abs,
norm_smul := abs_mul,
complete := λ X H, analysis.complete ℝ H
⦄
/- 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 := max N₁ N₂ in
exists.intro N
(take n,
suppose n ≥ N,
have ngtN₁ : n ≥ N₁, from nat.le_trans !le_max_left `n ≥ N`,
have ngtN₂ : n ≥ N₂, from nat.le_trans !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)
smul_converges_to_seq c HX
proposition mul_right_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) :
(λ n, X n * c) ⟶ x * c in ℕ :=
@ -359,44 +265,12 @@ 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) < ε, begin rewrite -(sub_zero (X n)), apply HN n Hn end,
show abs (abs (X n) - 0) < ε, using this,
by rewrite [sub_zero, abs_of_nonneg !abs_nonneg]; apply this)
norm_converges_to_seq_zero HX
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 [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)
converges_to_seq_zero_of_norm_converges_to_seq_zero HX
proposition abs_converges_to_seq_zero_iff (X : ℕ → ℝ) :
((λ n, abs (X n)) ⟶ 0 in ℕ) ↔ (X ⟶ 0 in ℕ) :=
@ -409,8 +283,7 @@ end limit_operations
/- monotone sequences -/
section monotone_sequences
open nat set
open real set
variable {X : ℕ → ℝ}
definition nondecreasing (X : ℕ → ℝ) : Prop := ∀ ⦃i j⦄, i ≤ j → X i ≤ X j
@ -499,12 +372,15 @@ have H₃ : {x : ℝ | -x ∈ X ' univ} = {x : ℝ | x ∈ (λ n, -X n) ' univ},
... = {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],
-- need krewrite here
krewrite [-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
/- x^n converges to 0 if abs x < 1 -/
section xn
open nat set
@ -515,7 +391,7 @@ suffices H' : (λ n, (abs x)^n) ⟶ 0 in ℕ, from
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),
iaX := real.inf (aX ' univ),
asX := (λ n, (abs x)^(succ n)) in
have noninc_aX : nonincreasing aX, from
nonincreasing_of_forall_succ_le
@ -525,8 +401,8 @@ have noninc_aX : nonincreasing aX, from
assert (abs x) * (abs x)^i ≤ (abs x)^i, by krewrite one_mul at this; exact this,
show (abs x) ^ (succ i) ≤ (abs x)^i, by rewrite pow_succ; apply this),
have bdd_aX : ∀ i, 0 ≤ aX i, from take i, !pow_nonneg_of_nonneg !abs_nonneg,
assert 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,
assert aXconv : aX ⟶ iaX in ℕ, proof converges_to_seq_inf_of_nonincreasing noninc_aX bdd_aX qed,
have asXconv : asX ⟶ iaX in ℕ, from 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',
assert iaX = 0, from eq_zero_of_mul_eq_self_left (ne_of_lt H) (eq.symm this),
@ -534,47 +410,57 @@ show aX ⟶ 0 in ℕ, begin rewrite -this, exact aXconv end --from this ▸ aXco
end xn
/- continuity on the reals -/
section continuous
-- this definition should be inherited from metric_space once a migrate is done.
definition continuous (f : ℝ → ℝ) :=
∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (x - x') < δ → abs (f x - f x') < ε
theorem continuous_real_elim {f : ℝ → ℝ} (H : continuous f) :
∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ,
abs (x' - x) < δ → abs (f x' - f x) < ε :=
H
theorem continuous_real_intro {f : ℝ → ℝ}
(H : ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ,
abs (x' - x) < δ → abs (f x' - f x) < ε) :
continuous f :=
H
theorem pos_on_nbhd_of_cts_of_pos {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ} (Hb : f b > 0) :
∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (b - y) < δ → f y > 0 :=
∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (y - b) < δ → f y > 0 :=
begin
let Hcont := Hf b Hb,
let Hcont := continuous_real_elim Hf b Hb,
cases Hcont with δ Hδ,
existsi δ,
split,
exact and.left Hδ,
intro y Hy,
let Hy' := and.right Hδ y Hy,
note Hlt := sub_lt_of_abs_sub_lt_right Hy',
note Hlt := sub_lt_of_abs_sub_lt_left Hy',
rewrite sub_self at Hlt,
assumption
end
theorem neg_on_nbhd_of_cts_of_neg {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ} (Hb : f b < 0) :
∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (b - y) < δ → f y < 0 :=
∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (y - b) < δ → f y < 0 :=
begin
let Hcont := Hf b (neg_pos_of_neg Hb),
let Hcont := continuous_real_elim Hf b (neg_pos_of_neg Hb),
cases Hcont with δ Hδ,
existsi δ,
split,
exact and.left Hδ,
intro y Hy,
let Hy' := and.right Hδ y Hy,
let Hlt := sub_lt_of_abs_sub_lt_left Hy',
note Hlt' := lt_add_of_sub_lt_right Hlt,
rewrite [-sub_eq_add_neg at Hlt', sub_self at Hlt'],
let Hlt := sub_lt_of_abs_sub_lt_right Hy',
note Hlt' := lt_add_of_sub_lt_left Hlt,
rewrite [add.comm at Hlt', -sub_eq_add_neg at Hlt', sub_self at Hlt'],
assumption
end
theorem neg_continuous_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) : continuous (λ x, - f x) :=
theorem continuous_neg_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) : continuous (λ x, - f x) :=
begin
apply continuous_real_intro,
intros x ε Hε,
cases Hcon x Hε with δ Hδ,
cases continuous_real_elim Hcon x Hε with δ Hδ,
cases Hδ with Hδ₁ Hδ₂,
existsi δ,
split,
@ -585,11 +471,12 @@ theorem neg_continuous_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) : c
exact HD
end
theorem translate_continuous_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) (a : ℝ) :
theorem continuous_offset_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) (a : ℝ) :
continuous (λ x, (f x) + a) :=
begin
apply continuous_real_intro,
intros x ε Hε,
cases Hcon x Hε with δ Hδ,
cases continuous_real_elim Hcon x Hε with δ Hδ,
cases Hδ with Hδ₁ Hδ₂,
existsi δ,
split,
@ -599,239 +486,9 @@ theorem translate_continuous_of_continuous {f : ℝ → ℝ} (Hcon : continuous
apply Hδ₂,
assumption
end
end continuous
section inter_val
open set
private definition inter_sup (a b : ℝ) (f : ℝ → ℝ) := sup {x | x < b ∧ f x < 0}
section
parameters {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) (Ha : f a < 0) (Hb : f b > 0)
include Hf Ha Hb Hab
private theorem Hinh : ∃ x, x ∈ {x | x < b ∧ f x < 0} := exists.intro a (and.intro Hab Ha)
private theorem Hmem : ∀ x, x ∈ {x | x < b ∧ f x < 0} → x ≤ b := λ x Hx, le_of_lt (and.left Hx)
private theorem Hsupleb : inter_sup a b f ≤ b := sup_le (Hinh) Hmem
local notation 2 := of_num 1 + of_num 1
private theorem ex_delta_lt {x : ℝ} (Hx : f x < 0) (Hxb : x < b) : ∃ δ : ℝ, δ > 0 ∧ x + δ < b ∧ f (x + δ) < 0 :=
begin
let Hcont := neg_on_nbhd_of_cts_of_neg Hf Hx,
cases Hcont with δ Hδ,
{cases em (x + δ < b) with Haδ Haδ,
existsi δ / 2,
split,
{exact div_pos_of_pos_of_pos (and.left Hδ) two_pos},
split,
{apply lt.trans,
apply add_lt_add_left,
exact div_two_lt_of_pos (and.left Hδ),
exact Haδ},
{apply and.right Hδ,
krewrite [sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg,
abs_of_pos (div_pos_of_pos_of_pos (and.left Hδ) two_pos)],
exact div_two_lt_of_pos (and.left Hδ)},
existsi (b - x) / 2,
split,
{apply div_pos_of_pos_of_pos,
exact sub_pos_of_lt Hxb,
exact two_pos},
split,
{apply add_midpoint Hxb},
{apply and.right Hδ,
krewrite [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)],
apply lt_of_lt_of_le,
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
private lemma sup_near_b {δ : ℝ} (Hpos : 0 < δ)
(Hgeb : inter_sup a b f + δ / 2 ≥ b) : abs (inter_sup a b f - b) < δ :=
begin
apply abs_lt_of_lt_of_neg_lt,
apply sub_lt_left_of_lt_add,
apply lt_of_le_of_lt,
apply Hsupleb,
apply lt_add_of_pos_right Hpos,
rewrite neg_sub,
apply sub_lt_left_of_lt_add,
apply lt_of_le_of_lt,
apply Hgeb,
apply add_lt_add_left,
apply div_two_lt_of_pos Hpos
end
private lemma delta_of_lt (Hflt : f (inter_sup a b f) < 0) :
∃ δ : ℝ, δ > 0 ∧ inter_sup a b f + δ < b ∧ f (inter_sup a b f + δ) < 0 :=
if Hlt : inter_sup a b f < b then ex_delta_lt Hflt Hlt else
begin
let Heq := eq_of_le_of_ge Hsupleb (le_of_not_gt Hlt),
apply absurd Hflt,
apply not_lt_of_ge,
apply le_of_lt,
rewrite Heq,
exact Hb
end
private theorem sup_fn_interval_aux1 : f (inter_sup a b f) ≥ 0 :=
have ¬ f (inter_sup a b f) < 0, from
(suppose f (inter_sup a b f) < 0,
obtain δ Hδ, from delta_of_lt this,
have inter_sup a b f + δ ∈ {x | x < b ∧ f x < 0},
from and.intro (and.left (and.right Hδ)) (and.right (and.right Hδ)),
have ¬ inter_sup a b f < inter_sup a b f + δ,
from not_lt_of_ge (le_sup this Hmem),
show false, from this (lt_add_of_pos_right (and.left Hδ))),
le_of_not_gt this
private theorem sup_fn_interval_aux2 : f (inter_sup a b f) ≤ 0 :=
have ¬ f (inter_sup a b f) > 0, from
(assume Hfsup : f (inter_sup a b f) > 0,
obtain δ Hδ, from pos_on_nbhd_of_cts_of_pos Hf Hfsup,
have ∀ x, x ∈ {x | x < b ∧ f x < 0} → x ≤ inter_sup a b f - δ / 2, from
(take x, assume Hxset : x ∈ {x | x < b ∧ f x < 0},
have ¬ x > inter_sup a b f - δ / 2, from
(assume Hngt,
have Habs : abs (inter_sup a b f - x) < δ, begin
apply abs_lt_of_lt_of_neg_lt,
apply sub_lt_of_sub_lt,
apply gt.trans,
exact Hngt,
apply sub_lt_sub_left,
exact div_two_lt_of_pos (and.left Hδ),
rewrite neg_sub,
apply lt_of_le_of_lt,
rotate 1,
apply and.left Hδ,
apply sub_nonpos_of_le,
apply le_sup,
exact Hxset,
exact Hmem
end,
have f x > 0, from and.right Hδ x Habs,
show false, from (not_lt_of_gt this) (and.right Hxset)),
le_of_not_gt this),
have Hle : inter_sup a b f ≤ inter_sup a b f - δ / 2, from sup_le Hinh this,
show false, from not_le_of_gt
(sub_lt_of_pos _ (div_pos_of_pos_of_pos (and.left Hδ) (two_pos))) Hle),
le_of_not_gt this
private theorem sup_fn_interval : f (inter_sup a b f) = 0 :=
eq_of_le_of_ge sup_fn_interval_aux2 sup_fn_interval_aux1
private theorem intermediate_value_incr_aux2 : ∃ δ : ℝ, δ > 0 ∧ a + δ < b ∧ f (a + δ) < 0 :=
begin
let Hcont := neg_on_nbhd_of_cts_of_neg Hf Ha,
cases Hcont with δ Hδ,
{cases em (a + δ < b) with Haδ Haδ,
existsi δ / 2,
split,
{exact div_pos_of_pos_of_pos (and.left Hδ) two_pos},
split,
{apply lt.trans,
apply add_lt_add_left,
exact div_two_lt_of_pos (and.left Hδ),
exact Haδ},
{apply and.right Hδ,
krewrite [sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg,
abs_of_pos (div_pos_of_pos_of_pos (and.left Hδ) two_pos)],
exact div_two_lt_of_pos (and.left Hδ)},
existsi (b - a) / 2,
split,
{apply div_pos_of_pos_of_pos,
exact sub_pos_of_lt Hab,
exact two_pos},
split,
{apply add_midpoint Hab},
{apply and.right Hδ,
krewrite [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)],
apply lt_of_lt_of_le,
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
theorem intermediate_value_incr_zero : ∃ c, a < c ∧ c < b ∧ f c = 0 :=
begin
existsi inter_sup a b f,
split,
{cases intermediate_value_incr_aux2 with δ Hδ,
apply lt_of_lt_of_le,
apply lt_add_of_pos_right,
exact and.left Hδ,
apply le_sup,
exact and.right Hδ,
intro x Hx,
apply le_of_lt,
exact and.left Hx},
split,
{cases pos_on_nbhd_of_cts_of_pos Hf Hb with δ Hδ,
apply lt_of_le_of_lt,
rotate 1,
apply sub_lt_of_pos,
exact and.left Hδ,
rotate_right 1,
apply sup_le,
exact exists.intro a (and.intro Hab Ha),
intro x Hx,
apply le_of_not_gt,
intro Hxgt,
have Hxgt' : b - x < δ, from sub_lt_of_sub_lt Hxgt,
krewrite -(abs_of_pos (sub_pos_of_lt (and.left Hx))) at Hxgt',
note Hxgt'' := and.right Hδ _ Hxgt',
exact not_lt_of_ge (le_of_lt Hxgt'') (and.right Hx)},
{exact sup_fn_interval}
end
end
theorem intermediate_value_decr_zero {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b)
(Ha : f a > 0) (Hb : f b < 0) : ∃ c, a < c ∧ c < b ∧ f c = 0 :=
begin
have Ha' : - f a < 0, from neg_neg_of_pos Ha,
have Hb' : - f b > 0, from neg_pos_of_neg Hb,
have Hcon : continuous (λ x, - f x), from neg_continuous_of_continuous Hf,
let Hiv := intermediate_value_incr_zero Hcon Hab Ha' Hb',
cases Hiv with c Hc,
existsi c,
split,
exact and.left Hc,
split,
exact and.left (and.right Hc),
apply eq_zero_of_neg_eq_zero,
apply and.right (and.right Hc)
end
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 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,
exists.intro c
(and.intro (and.left Hc) (and.intro (and.left (and.right Hc)) (eq_of_sub_eq_zero (and.right (and.right Hc)))))
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 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,
exists.intro c
(and.intro (and.left Hc) (and.intro (and.left (and.right Hc)) (eq_of_sub_eq_zero (and.right (and.right Hc)))))
end inter_val
/-
proposition converges_to_at_unique {f : M → N} {y₁ y₂ : N} {x : M}
(H₁ : f ⟶ y₁ '[at x]) (H₂ : f ⟶ y₂ '[at x]) : y₁ = y₂ :=
@ -844,7 +501,4 @@ eq_of_forall_dist_le
from H₂ e2pos,
let δ := min δ₁ δ₂ in
have δ > 0, from lt_min δ₁pos δ₂pos,
-/
end real