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

feat(theories/analysis): intro/elim rules for continuous_on, etc

Browse source
This commit is contained in:
Rob Lewis 2016-04-19 18:17:53 -04:00 committed by Leonardo de Moura
parent 963c9e8977
commit 92531fba16
5 changed files with 163 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
library/theories/analysis/bounded_linear_operator.lean
View file

@ -6,14 +6,13 @@ Author: Robert Y. Lewis
Bounded linear operators
-/
import .normed_space .real_limit algebra.module algebra.homomorphism
open real nat classical
open real nat classical topology
noncomputable theory
namespace analysis
-- define bounded linear operators and basic instances
section bdd_lin_op
set_option pp.universes true
structure is_bdd_linear_map [class] {V W : Type} [normed_vector_space V] [normed_vector_space W] (f : V → W)
extends is_module_hom ℝ f :=
(op_norm : ℝ) (op_norm_pos : op_norm > 0) (op_norm_bound : ∀ v : V, ∥f v∥ ≤ op_norm * ∥v∥)
@ -31,13 +30,11 @@ theorem is_bdd_linear_map_zero [instance] (V W : Type) [normed_vector_space V] [
is_bdd_linear_map (λ x : V, (0 : W)) :=
begin
fapply is_bdd_linear_map.mk,
intros,
all_goals intros,
rewrite zero_add,
intros,
rewrite smul_zero,
exact 1,
exact zero_lt_one,
intros,
rewrite [norm_zero, one_mul],
apply norm_nonneg
end
@ -47,16 +44,14 @@ theorem is_bdd_linear_map_add [instance] {V W : Type} [normed_vector_space V] [n
is_bdd_linear_map (λ x, f x + g x) :=
begin
fapply is_bdd_linear_map.mk,
{intros,
rewrite [hom_add f, hom_add g],-- (this takes 4 seconds!!)rewrite [2 hom_add],
all_goals intros,
{rewrite [hom_add f, hom_add g],-- (this takes 4 seconds: rewrite [2 hom_add])
simp},
{intros,
rewrite [hom_smul f, hom_smul g, smul_left_distrib]},
{rewrite [hom_smul f, hom_smul g, smul_left_distrib]},
{exact is_bdd_linear_map.op_norm _ _ f + is_bdd_linear_map.op_norm _ _ g},
{apply add_pos,
repeat apply is_bdd_linear_map.op_norm_pos},
{intro,
apply le.trans,
{apply le.trans,
apply norm_triangle,
rewrite right_distrib,
apply add_le_add,
@ -75,18 +70,15 @@ theorem is_bdd_linear_map_smul [instance] {V W : Type} [normed_vector_space V] [
apply is_bdd_linear_map_zero},
intro Hcnz,
fapply is_bdd_linear_map.mk,
{intros,
rewrite [hom_add f, smul_left_distrib]},--rewrite [linear_map_additive ℝ f, smul_left_distrib]},
{intros,
rewrite [hom_smul f, -*mul_smul, {c*r}mul.comm]},
--rewrite [linear_map_homogeneous f, -*mul_smul, {c * a}mul.comm]},
all_goals intros,
{rewrite [hom_add f, smul_left_distrib]},
{rewrite [hom_smul f, -*mul_smul, {c*r}mul.comm]},
{exact (abs c) * is_bdd_linear_map.op_norm _ _ f},
{have Hpos : abs c > 0, from abs_pos_of_ne_zero Hcnz,
apply mul_pos,
assumption,
apply is_bdd_linear_map.op_norm_pos},
{intro,
rewrite [norm_smul, mul.assoc],
{rewrite [norm_smul, mul.assoc],
apply mul_le_mul_of_nonneg_left,
apply is_bdd_linear_map.op_norm_bound,
apply abs_nonneg}
@ -106,14 +98,12 @@ theorem is_bdd_linear_map_comp {U V W : Type} [normed_vector_space U] [normed_ve
is_bdd_linear_map (λ u, f (g u)) :=
begin
fapply is_bdd_linear_map.mk,
{intros,
rewrite [hom_add g, hom_add f]},--rewrite [linear_map_additive ℝ g, linear_map_additive ℝ f]},
{intros,
rewrite [hom_smul g, hom_smul f]},--rewrite [linear_map_homogeneous g, linear_map_homogeneous f]},
all_goals intros,
{rewrite [hom_add g, hom_add f]},
{rewrite [hom_smul g, hom_smul f]},
{exact is_bdd_linear_map.op_norm _ _ f * is_bdd_linear_map.op_norm _ _ g},
{apply mul_pos, repeat apply is_bdd_linear_map.op_norm_pos},
{intros,
apply le.trans,
{apply le.trans,
apply is_bdd_linear_map.op_norm_bound _ _ f,
apply le.trans,
apply mul_le_mul_of_nonneg_left,
@ -138,6 +128,7 @@ theorem op_norm_bound (v : V) : ∥f v∥ ≤ (op_norm f) * ∥v∥ := is_bdd_li
theorem bounded_linear_operator_continuous : continuous f :=
begin
apply continuous_of_forall_continuous_at,
intro x,
apply normed_vector_space.continuous_at_intro,
intro ε Hε,
@ -145,7 +136,7 @@ theorem bounded_linear_operator_continuous : continuous f :=
split,
apply div_pos_of_pos_of_pos Hε !op_norm_pos,
intro x' Hx',
rewrite [-hom_sub f],--[-linear_map_sub f],
rewrite [-hom_sub f],
apply lt_of_le_of_lt,
apply op_norm_bound f,
rewrite [-@mul_div_cancel' _ _ ε (op_norm f) (ne_of_gt !op_norm_pos)],
@ -283,7 +274,7 @@ theorem frechet_deriv_at_smul {c : ℝ} {A : V → W} [is_bdd_linear_map A]
end
end
theorem is_frechet_deriv_at_neg {A : V → W} [is_bdd_linear_map A]
theorem frechet_deriv_at_neg {A : V → W} [is_bdd_linear_map A]
(Hf : is_frechet_deriv_at f A x) : is_frechet_deriv_at (λ y, - f y) (λ y, - A y) x :=
begin
apply is_frechet_deriv_at_intro,
@ -299,11 +290,10 @@ theorem is_frechet_deriv_at_neg {A : V → W} [is_bdd_linear_map A]
assumption
end
theorem is_frechet_deriv_at_add (A B : V → W) [is_bdd_linear_map A] [is_bdd_linear_map B]
theorem frechet_deriv_at_add (A B : V → W) [is_bdd_linear_map A] [is_bdd_linear_map B]
(Hf : is_frechet_deriv_at f A x) (Hg : is_frechet_deriv_at g B x) :
is_frechet_deriv_at (λ y, f y + g y) (λ y, A y + B y) x :=
begin
rewrite ↑is_frechet_deriv_at,
have Hle : ∀ h, ∥f (x + h) + g (x + h) - (f x + g x) - (A h + B h)∥ / ∥h∥ ≤
∥f (x + h) - f x - A h∥ / ∥h∥ + ∥g (x + h) - g x - B h∥ / ∥h∥, begin
intro h,
@ -344,13 +334,13 @@ theorem continuous_at_of_diffable_at [Hf : frechet_diffable_at f x] : continuous
cases Hδ with Hδ Hδ',
existsi min δ ((ε / 2) / (ε + op_norm (frechet_deriv_at f x))),
split,
apply lt_min,
{apply lt_min,
exact Hδ,
repeat apply div_pos_of_pos_of_pos,
exact Hε,
apply two_pos,
apply add_pos Hε !op_norm_pos,
intro x' Hx',
apply add_pos Hε !op_norm_pos},
{intro x' Hx',
cases em (x' - x = 0) with Heq Hneq,
rewrite [eq_of_sub_eq_zero Heq, sub_self, norm_zero], assumption,
have Hx'x : x' - x ≠ 0 ∧ dist (x' - x) 0 < δ, from and.intro Hneq begin
@ -366,11 +356,12 @@ theorem continuous_at_of_diffable_at [Hf : frechet_diffable_at f x] : continuous
from div_nonneg_of_nonneg_of_nonneg !norm_nonneg !norm_nonneg,
rewrite [sub_zero at Hδ'', abs_of_nonneg Hnn at Hδ'', add.comm at Hδ'', sub_add_cancel at Hδ''],
note H1 := lt_mul_of_div_lt_of_pos Hx'xp Hδ'',
have H2 : f x' - f x = f x' - f x - frechet_deriv_at f x (x' - x) + frechet_deriv_at f x (x' - x), by simp,
have H2 : f x' - f x = f x' - f x - frechet_deriv_at f x (x' - x) + frechet_deriv_at f x (x' - x),
by rewrite sub_add_cancel, --by simp, (simp takes .5 seconds to do this!)
rewrite H2,
apply lt_of_le_of_lt,
apply norm_triangle,
apply lt.trans, --lt_of_lt_of_le,
apply lt.trans,
apply add_lt_add_of_lt_of_le,
apply H1,
apply op_norm_bound (!frechet_deriv_at),
@ -384,7 +375,7 @@ theorem continuous_at_of_diffable_at [Hf : frechet_diffable_at f x] : continuous
exact calc
on * ∥x' - x∥ < on * min δ ((ε / 2) / (ε + on)) : mul_lt_mul_of_pos_left Hx' !op_norm_pos
... ≤ on * ((ε / 2) / (ε + on)) : mul_le_mul_of_nonneg_left !min_le_right (le_of_lt !op_norm_pos)
... < ε / 2 : mul_div_add_self_lt (div_pos_of_pos_of_pos Hε two_pos) Hε !op_norm_pos,
... < ε / 2 : mul_div_add_self_lt (div_pos_of_pos_of_pos Hε two_pos) Hε !op_norm_pos}
end
end frechet_deriv

2
library/theories/analysis/ivt.lean
View file

@ -6,7 +6,7 @@ Authors: Robert Y. Lewis
The intermediate value theorem.
-/
import .real_limit
open real analysis set classical
open real analysis set classical topology
noncomputable theory
private definition inter_sup (a b : ℝ) (f : ℝ → ℝ) := sup {x | x < b ∧ f x < 0}

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

@ -1,8 +1,6 @@
/-
Copyright (c) 2015 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Robert Lewis
Metric spaces.
-/
import data.real.complete data.pnat ..topology.continuous ..topology.limit data.set
@ -553,6 +551,31 @@ section continuity
variables {M N : Type} [Hm : metric_space M] [Hn : metric_space N]
include Hm Hn
open topology set
/- begin
intros x Hx ε Hε,
rewrite [↑continuous_on at Hfs],
cases @Hfs (open_ball (f x) ε) !open_ball_open with t Ht,
cases Ht with Ht Htx,
cases @Hfx (open_ball (f x) ε) !open_ball_open (mem_open_ball _ Hε) with V HV,
cases HV with HV HVx,
cases HVx with HVx HVf,
cases ex_Open_ball_subset_of_Open_of_nonempty HV HVx with δ Hδ,
cases Hδ with Hδ Hδx,
existsi δ,
split,
exact Hδ,
intro x' Hx',
rewrite dist_comm,
apply and.right,
apply HVf,
apply Hδx,
apply and.intro !mem_univ,
rewrite dist_comm,
apply Hx',
end-/
/- continuity at a point -/
-- the ε - δ definition of continuity is equivalent to the topological definition
@ -598,7 +621,88 @@ theorem continuous_at_elim {f : M → N} {x : M} (Hfx : continuous_at f x) :
apply Hx',
end
--<<<<<<< HEAD
theorem continuous_at_of_converges_to_at {f : M → N} {x : M} (Hf : f ⟶ f x [at x]) :
/-=======
theorem continuous_at_on_intro {f : M → N} {x : M} {s : set M}
(H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀₀ x' ∈ s, dist x' x < δ → dist (f x') (f x) < ε) :
continuous_at_on f x s :=
begin
intro t HOt Hfxt,
cases ex_Open_ball_subset_of_Open_of_nonempty HOt Hfxt with ε Hε,
cases H (and.left Hε) with δ Hδ,
existsi (open_ball x δ),
split,
apply open_ball_open,
split,
apply mem_open_ball,
apply and.left Hδ,
intro x' Hx',
apply mem_preimage,
apply mem_of_subset_of_mem,
apply and.right Hε,
apply and.intro !mem_univ,
rewrite dist_comm,
apply and.right Hδ,
apply and.right Hx',
rewrite dist_comm,
apply and.right (and.left Hx')
end
theorem continuous_at_on_elim {f : M → N} {x : M} {s : set M} (Hfs : continuous_at_on f x s) :
∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀₀ x' ∈ s, dist x' x < δ → dist (f x') (f x) < ε :=
begin
intro ε Hε,
unfold continuous_at_on at Hfs,
cases @Hfs (open_ball (f x) ε) !open_ball_open (mem_open_ball _ Hε) with u Hu,
cases Hu with Huo Hu,
cases Hu with Hxu Hu,
cases ex_Open_ball_subset_of_Open_of_nonempty Huo Hxu with δ Hδ,
existsi δ,
split,
exact and.left Hδ,
intros x' Hx's Hx'x,
have Hims : f ' (u ∩ s) ⊆ open_ball (f x) ε, begin
apply subset.trans (image_subset f Hu),
apply image_preimage_subset
end,
have Hx'int : x' ∈ u ∩ s, begin
apply and.intro,
apply mem_of_subset_of_mem,
apply and.right Hδ,
apply and.intro !mem_univ,
rewrite dist_comm,
repeat assumption
end,
have Hxx' : f x' ∈ open_ball (f x) ε, begin
apply mem_of_subset_of_mem,
apply Hims,
apply mem_image_of_mem,
apply Hx'int
end,
rewrite dist_comm,
apply and.right Hxx'
end
theorem continuous_on_intro {f : M → N} {s : set M}
(H : ∀ x, ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀₀ x' ∈ s, dist x' x < δ → dist (f x') (f x) < ε) :
continuous_on f s :=
begin
apply continuous_on_of_forall_continuous_at_on,
intro x,
apply continuous_at_on_intro,
apply H
end
theorem continuous_on_elim {f : M → N} {s : set M} (Hfs : continuous_on f s) :
∀₀ x ∈ s, ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀₀ x' ∈ s, dist x' x < δ → dist (f x') (f x) < ε :=
begin
intros x Hx,
exact continuous_at_on_elim (continuous_at_on_of_continuous_on Hfs Hx)
end-/
--theorem continuous_at_of_converges_to_at {f : M → N} {x : M} (Hf : f ⟶ f x at x) :
-->>>>>>> feat(theories/analysis): intro/elim rules for continuous_on, etc
continuous_at f x :=
continuous_at_intro
(take ε, suppose ε > 0,
@ -619,7 +723,7 @@ approaches_at_intro
obtain δ [δpos Hδ], from continuous_at_elim Hf this,
exists.intro δ (and.intro δpos (λ x' Hx' xnex', Hδ x' Hx')))
definition continuous (f : M → N) : Prop := ∀ x, continuous_at f x
--definition continuous (f : M → N) : Prop := ∀ x, continuous_at f x
theorem converges_seq_comp_of_converges_seq_of_cts (X : ℕ → M) [HX : converges_seq X] {f : M → N}
(Hf : continuous f) :
@ -629,7 +733,7 @@ theorem converges_seq_comp_of_converges_seq_of_cts (X : ℕ → M) [HX : converg
existsi f xlim,
apply approaches_at_infty_intro,
intros ε Hε,
let Hcont := (continuous_at_elim (Hf xlim)) Hε,
let Hcont := (continuous_at_elim (forall_continuous_at_of_continuous Hf xlim)) Hε,
cases Hcont with δ Hδ,
cases approaches_at_infty_dest Hxlim (and.left Hδ) with B HB,
existsi B,
@ -641,6 +745,7 @@ theorem converges_seq_comp_of_converges_seq_of_cts (X : ℕ → M) [HX : converg
omit Hn
theorem id_continuous : continuous (λ x : M, x) :=
begin
apply continuous_of_forall_continuous_at,
intros x,
apply continuous_at_intro,
intro ε Hε,

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

@ -508,19 +508,32 @@ end xn
/- continuity on the reals -/
section continuous
open topology
variable {f : ℝ → ℝ}
theorem continuous_real_elim {f : ℝ → ℝ} (H : continuous f) :
theorem continuous_real_elim (H : continuous f) :
∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ,
abs (x' - x) < δ → abs (f x' - f x) < ε :=
take x, continuous_at_elim (H x)
take x, continuous_at_elim (forall_continuous_at_of_continuous H x)
theorem continuous_real_intro {f : ℝ → ℝ}
theorem continuous_real_intro
(H : ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ,
abs (x' - x) < δ → abs (f x' - f x) < ε) :
continuous f :=
take x, continuous_at_intro (H x)
continuous_of_forall_continuous_at (take x, continuous_at_intro (H x))
theorem pos_on_nbhd_of_cts_of_pos {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ} (Hb : f b > 0) :
section
open set
variable {s : set ℝ}
--theorem continuous_on_real_elim (H : continuous_on f s) :
-- ∀₀ x ∈ s, x = x := sorry
end
variable (Hf : continuous f)
include Hf
theorem pos_on_nbhd_of_cts_of_pos {b : ℝ} (Hb : f b > 0) :
∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (y - b) < δ → f y > 0 :=
begin
let Hcont := continuous_real_elim Hf b Hb,
@ -535,7 +548,7 @@ theorem pos_on_nbhd_of_cts_of_pos {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ
assumption
end
theorem neg_on_nbhd_of_cts_of_neg {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ} (Hb : f b < 0) :
theorem neg_on_nbhd_of_cts_of_neg {b : ℝ} (Hb : f b < 0) :
∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (y - b) < δ → f y < 0 :=
begin
let Hcont := continuous_real_elim Hf b (neg_pos_of_neg Hb),
@ -551,11 +564,11 @@ theorem neg_on_nbhd_of_cts_of_neg {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ
assumption
end
theorem continuous_neg_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) : continuous (λ x, - f x) :=
theorem continuous_neg_of_continuous : continuous (λ x, - f x) :=
begin
apply continuous_real_intro,
intros x ε Hε,
cases continuous_real_elim Hcon x Hε with δ Hδ,
cases continuous_real_elim Hf x Hε with δ Hδ,
cases Hδ with Hδ₁ Hδ₂,
existsi δ,
split,
@ -566,12 +579,12 @@ theorem continuous_neg_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) : c
exact HD
end
theorem continuous_offset_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) (a : ℝ) :
theorem continuous_offset_of_continuous (a : ℝ) :
continuous (λ x, (f x) + a) :=
begin
apply continuous_real_intro,
intros x ε Hε,
cases continuous_real_elim Hcon x Hε with δ Hδ,
cases continuous_real_elim Hf x Hε with δ Hδ,
cases Hδ with Hδ₁ Hδ₂,
existsi δ,
split,
@ -582,14 +595,16 @@ theorem continuous_offset_of_continuous {f : ℝ → ℝ} (Hcon : continuous f)
assumption
end
theorem continuous_mul_of_continuous {f g : ℝ → ℝ} (Hconf : continuous f) (Hcong : continuous g) :
theorem continuous_mul_of_continuous {g : ℝ → ℝ} (Hcong : continuous g) :
continuous (λ x, f x * g x) :=
begin
apply continuous_of_forall_continuous_at,
intro x,
apply continuous_at_of_converges_to_at,
apply mul_converges_to_at,
all_goals apply converges_to_at_of_continuous_at,
apply Hconf,
all_goals apply forall_continuous_at_of_continuous,
apply Hf,
apply Hcong
end

2
library/theories/analysis/sqrt.lean
View file

@ -6,7 +6,7 @@ Authors: Robert Y. Lewis, Jeremy Avigad
The square root function.
-/
import .ivt
open analysis real classical
open analysis real classical topology
noncomputable theory
private definition sqr_lb (x : ℝ) : ℝ := 0