From 92531fba16d9207442f9b116e15a9225dc7907c4 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Tue, 19 Apr 2016 18:17:53 -0400 Subject: [PATCH] feat(theories/analysis): intro/elim rules for continuous_on, etc --- .../analysis/bounded_linear_operator.lean | 59 ++++----- library/theories/analysis/ivt.lean | 2 +- library/theories/analysis/metric_space.lean | 113 +++++++++++++++++- library/theories/analysis/real_limit.lean | 39 ++++-- library/theories/analysis/sqrt.lean | 2 +- 5 files changed, 163 insertions(+), 52 deletions(-) diff --git a/library/theories/analysis/bounded_linear_operator.lean b/library/theories/analysis/bounded_linear_operator.lean index 6c7eb0cea..dc8aa7b17 100644 --- a/library/theories/analysis/bounded_linear_operator.lean +++ b/library/theories/analysis/bounded_linear_operator.lean @@ -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 diff --git a/library/theories/analysis/ivt.lean b/library/theories/analysis/ivt.lean index 24d8890ee..edc4ac125 100644 --- a/library/theories/analysis/ivt.lean +++ b/library/theories/analysis/ivt.lean @@ -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} diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index b488dddd8..7d49a14a8 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -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ε, diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index ef875b4e9..36c0656d5 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -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 diff --git a/library/theories/analysis/sqrt.lean b/library/theories/analysis/sqrt.lean index 027e6870a..94de569bf 100644 --- a/library/theories/analysis/sqrt.lean +++ b/library/theories/analysis/sqrt.lean @@ -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