From 5a439942dd43e5a910c3f9bab74fb1eed81e43fa Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Wed, 25 May 2016 15:32:24 -0400 Subject: [PATCH] feat(library/theories): adapt analysis theory to use new topological limits --- .../analysis/bounded_linear_operator.lean | 246 +++++++- library/theories/analysis/ivt.lean | 6 +- library/theories/analysis/metric_space.lean | 398 +++++-------- library/theories/analysis/normed_space.lean | 385 +++++++++---- library/theories/analysis/real_deriv.lean | 42 +- library/theories/analysis/real_limit.lean | 537 +++++++++++------- library/theories/analysis/sqrt.lean | 2 +- library/theories/move.lean | 34 ++ library/theories/topology/continuous.lean | 37 +- library/theories/topology/limit.lean | 10 + 10 files changed, 1050 insertions(+), 647 deletions(-) diff --git a/library/theories/analysis/bounded_linear_operator.lean b/library/theories/analysis/bounded_linear_operator.lean index 924e9d8ef..60619b51a 100644 --- a/library/theories/analysis/bounded_linear_operator.lean +++ b/library/theories/analysis/bounded_linear_operator.lean @@ -6,7 +6,8 @@ Author: Robert Y. Lewis Bounded linear operators -/ import .normed_space .real_limit algebra.module algebra.homomorphism -open real nat classical topology +open real nat classical topology set +--open normed_vector_space (this confuses lots of stuff??) noncomputable theory namespace analysis @@ -156,21 +157,60 @@ variables [HV : normed_vector_space V] [HW : normed_vector_space W] include HV HW definition is_frechet_deriv_at (f A : V → W) [is_bdd_linear_map A] (x : V) := - (λ h : V, ∥f (x + h) - f x - A h ∥ / ∥ h ∥) ⟶ 0 at 0 + (λ h : V, ∥f (x + h) - f x - A h ∥ / ∥ h ∥) ⟶ 0 [at 0] + +lemma diff_quot_cts {f A : V → W} [HA : is_bdd_linear_map A] {y : V} (Hf : is_frechet_deriv_at f A y) : + continuous_at (λ h, ∥f (y + h) - f y - A h∥ / ∥h∥) 0 := + begin + apply normed_vector_space.continuous_at_intro, + intro ε Hε, + cases normed_vector_space.approaches_at_dest Hf Hε with δ Hδ, + existsi δ, + split, + exact and.left Hδ, + intro x' Hx', + cases em (x' = 0) with Heq Hneq, + {rewrite [Heq, norm_zero, div_zero, sub_zero, norm_zero], apply Hε}, + {rewrite [norm_zero, div_zero], + apply and.right Hδ, + repeat assumption} + end + +theorem is_bdd_linear_map_of_eq {A B : V → W} [HA : is_bdd_linear_map A] (HAB : A = B) : + is_bdd_linear_map B := + begin + fapply is_bdd_linear_map.mk, + all_goals try rewrite -HAB, + {apply hom_add}, + {apply hom_smul}, + {exact op_norm A}, + {exact op_norm_pos A}, + {rewrite -HAB, apply op_norm_bound} + end + +definition is_frechet_deriv_at_of_eq {f A : V → W} [is_bdd_linear_map A] {x : V} + (Hfd : is_frechet_deriv_at f A x) {B : V → W} (HAB : A = B) : + @is_frechet_deriv_at _ _ _ _ f B (is_bdd_linear_map_of_eq HAB) x := + begin + unfold is_frechet_deriv_at, + rewrite -HAB, + apply Hfd + end + theorem is_frechet_deriv_at_intro {f A : V → W} [is_bdd_linear_map A] {x : V} (H : ∀ ⦃ε : ℝ⦄, ε > 0 → (∃ δ : ℝ, δ > 0 ∧ ∀ ⦃x' : V⦄, x' ≠ 0 ∧ ∥x'∥ < δ → ∥f (x + x') - f x - A x'∥ / ∥x'∥ < ε)) : is_frechet_deriv_at f A x := begin + apply normed_vector_space.approaches_at_intro, intros ε Hε, cases H Hε with δ Hδ, cases Hδ with Hδ Hδ', existsi δ, split, assumption, - intros x' Hx', - cases Hx' with Hx'1 Hx'2, + intros x' Hx'1 Hx'2, show abs (∥f (x + x') - f x - A x'∥ / ∥x'∥ - 0) < ε, begin have H : ∥f (x + x') - f x - A x'∥ / ∥x'∥ ≥ 0, from div_nonneg_of_nonneg_of_nonneg !norm_nonneg !norm_nonneg, @@ -179,7 +219,7 @@ theorem is_frechet_deriv_at_intro {f A : V → W} [is_bdd_linear_map A] {x : V} split, assumption, rewrite [-sub_zero x'], - apply Hx'2 + apply Hx'1 end end @@ -188,14 +228,14 @@ theorem is_frechet_deriv_at_elim {f A : V → W} [is_bdd_linear_map A] {x : V} ( (∃ δ : ℝ, δ > 0 ∧ ∀ ⦃x' : V⦄, x' ≠ 0 ∧ ∥x'∥ < δ → ∥f (x + x') - f x - A x'∥ / ∥x'∥ < ε) := begin intros ε Hε, - cases H Hε with δ Hδ, + cases normed_vector_space.approaches_at_dest H Hε with δ Hδ, cases Hδ with Hδ Hδ', existsi δ, split, assumption, intros x' Hx', rewrite [-sub_zero x' at Hx' {2}], - have Hδ'' : abs (∥f (x + x') - f x - A x'∥ / ∥x'∥ - 0) < ε, from Hδ' Hx', + have Hδ'' : abs (∥f (x + x') - f x - A x'∥ / ∥x'∥ - 0) < ε, from Hδ' (and.right Hx') (and.left Hx'), have Hpos : ∥f (x + x') - f x - A x'∥ / ∥x'∥ ≥ 0, from div_nonneg_of_nonneg_of_nonneg !norm_nonneg !norm_nonneg, rewrite [sub_zero at Hδ'', abs_of_nonneg Hpos at Hδ''], assumption @@ -215,22 +255,36 @@ definition frechet_deriv_at_is_bdd_linear_map [instance] (f : V → W) (x : V) [ frechet_diffable_at.HA _ _ f x theorem frechet_deriv_spec [Hf : frechet_diffable_at f x] : - (λ h : V, ∥f (x + h) - f x - (frechet_deriv_at f x h) ∥ / ∥ h ∥) ⟶ 0 at 0 := + (λ h : V, ∥f (x + h) - f x - (frechet_deriv_at f x h) ∥ / ∥ h ∥) ⟶ 0 [at 0] := frechet_diffable_at.is_fr_der _ _ f x theorem frechet_deriv_at_const (w : W) : is_frechet_deriv_at (λ v : V, w) (λ v : V, 0) x := begin + apply normed_vector_space.approaches_at_intro, intros ε Hε, existsi 1, split, exact zero_lt_one, - intros x' Hx', - rewrite [sub_self, sub_zero, norm_zero], - krewrite [zero_div, dist_self], + intros x' Hx' _, + rewrite [2 sub_self, norm_zero], + krewrite [zero_div, sub_zero, norm_zero], assumption end -theorem frechet_deriv_at_smul {c : ℝ} {A : V → W} [is_bdd_linear_map A] +theorem frechet_deriv_at_id : is_frechet_deriv_at (λ v : V, v) (λ v : V, v) x := + begin + apply normed_vector_space.approaches_at_intro, + intros ε Hε, + existsi 1, + split, + exact zero_lt_one, + intros x' Hx' _, + have x + x' - x - x' = 0, by simp, + rewrite [this, norm_zero, zero_div, sub_self, norm_zero], + exact Hε + end + +theorem frechet_deriv_at_smul (c : ℝ) {A : V → W} [is_bdd_linear_map A] (Hf : is_frechet_deriv_at f A x) : is_frechet_deriv_at (λ y, c • f y) (λ y, c • A y) x := begin eapply @decidable.cases_on (abs c = 0), @@ -240,31 +294,32 @@ theorem frechet_deriv_at_smul {c : ℝ} {A : V → W} [is_bdd_linear_map A] have Hfz : (λ y : V, (0 : ℝ) • f y) = (λ y : V, 0), from funext (λ y, !zero_smul), --have Hfz' : (λ x : V, (0 : ℝ) • A x) = (λ x : V, 0), from funext (λ y, !zero_smul), -- rewriting Hfz' produces type-incorrect term - rewrite [Hz, Hfz, ↑is_frechet_deriv_at], + rewrite [Hz, Hfz], + apply metric_space.approaches_at_intro, intro ε Hε, existsi 1, split, exact zero_lt_one, - intro x' Hx', + intro x' Hx' _, rewrite [zero_smul, *sub_zero, norm_zero], krewrite [zero_div, dist_self], exact Hε}, intro Hcnz, - rewrite ↑is_frechet_deriv_at, + apply normed_vector_space.approaches_at_intro, intros ε Hε, have Hεc : ε / abs c > 0, from div_pos_of_pos_of_pos Hε (lt_of_le_of_ne !abs_nonneg (ne.symm Hcnz)), - cases Hf Hεc with δ Hδ, + cases normed_vector_space.approaches_at_dest Hf Hεc with δ Hδ, cases Hδ with Hδp Hδ, existsi δ, split, assumption, - intro x' Hx', + intro x' Hx' _, show abs ((∥c • f (x + x') - c • f x - c • A x'∥ / ∥x'∥ - 0)) < ε, begin rewrite [sub_zero, -2 smul_sub_left_distrib, norm_smul], krewrite mul_div_assoc, rewrite [abs_mul, abs_abs, -{ε}mul_div_cancel' Hcnz], apply mul_lt_mul_of_pos_left, - have Hδ' : abs (∥f (x + x') - f x - A x'∥ / ∥x'∥ - 0) < ε / abs c, from Hδ Hx', + have Hδ' : abs (∥f (x + x') - f x - A x'∥ / ∥x'∥ - 0) < ε / abs c, from Hδ Hx' a, rewrite sub_zero at Hδ', apply Hδ', apply lt_of_le_of_ne, @@ -309,17 +364,19 @@ theorem frechet_deriv_at_add (A B : V → W) [is_bdd_linear_map A] [is_bdd_linea krewrite [Hhe, *div_zero, zero_add], eapply le.refl end, - have Hlimge : (λ h, ∥f (x + h) - f x - A h∥ / ∥h∥ + ∥g (x + h) - g x - B h∥ / ∥h∥) ⟶ 0 at 0, begin + have Hlimge : (λ h, ∥f (x + h) - f x - A h∥ / ∥h∥ + ∥g (x + h) - g x - B h∥ / ∥h∥) ⟶ 0 [at 0], begin rewrite [-zero_add 0], - apply add_converges_to_at, + apply add_approaches, apply Hf, apply Hg end, - have Hlimle : (λ (h : V), (0 : ℝ)) ⟶ 0 at 0, from converges_to_at_constant 0 0, - apply converges_to_at_squeeze Hlimle Hlimge, + have Hlimle : (λ (h : V), (0 : ℝ)) ⟶ 0 [at 0], by apply approaches_constant, + apply approaches_squeeze Hlimle Hlimge, + apply filter.eventually_of_forall, intro y, apply div_nonneg_of_nonneg_of_nonneg, repeat apply norm_nonneg, + apply filter.eventually_of_forall, apply Hle end @@ -329,7 +386,7 @@ theorem continuous_at_of_diffable_at [Hf : frechet_diffable_at f x] : continuous begin apply normed_vector_space.continuous_at_intro, intros ε Hε, - note Hfds := frechet_deriv_spec f x Hε, + note Hfds := normed_vector_space.approaches_at_dest (frechet_deriv_spec f x) Hε, cases Hfds with δ Hδ, cases Hδ with Hδ Hδ', existsi min δ ((ε / 2) / (ε + op_norm (frechet_deriv_at f x))), @@ -343,15 +400,15 @@ theorem continuous_at_of_diffable_at [Hf : frechet_diffable_at f x] : continuous {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 - change ∥(x' - x) - 0∥ < δ, + have Hx'x : x' - x ≠ 0 ∧ ∥(x' - x) - 0∥ < δ, from and.intro Hneq begin rewrite sub_zero, apply lt_of_lt_of_le, apply Hx', apply min_le_left end, have Hx'xp : ∥x' - x∥ > 0, from norm_pos_of_ne_zero Hneq, - have Hδ'' : abs (∥f (x + (x' - x)) - f x - frechet_deriv_at f x (x' - x)∥ / ∥x' - x∥ - 0) < ε, from Hδ' Hx'x, + have Hδ'' : abs (∥f (x + (x' - x)) - f x - frechet_deriv_at f x (x' - x)∥ / ∥x' - x∥ - 0) < ε, + from Hδ' (and.right Hx'x) (and.left Hx'x), have Hnn : ∥f (x + (x' - x)) - f x - frechet_deriv_at f x (x' - x)∥ / ∥x' - x∥ ≥ 0, 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δ''], @@ -378,9 +435,31 @@ theorem continuous_at_of_diffable_at [Hf : frechet_diffable_at f x] : continuous ... < ε / 2 : mul_div_add_self_lt (div_pos_of_pos_of_pos Hε two_pos) Hε !op_norm_pos} end +theorem continuous_at_of_is_frechet_deriv_at {A : V → W} [is_bdd_linear_map A] + (H : is_frechet_deriv_at f A x) : continuous_at f x := + begin + apply @continuous_at_of_diffable_at, + existsi A, + exact H + end + end frechet_deriv -/-section comp +section comp + +lemma div_mul_div_cancel {A : Type} [field A] (a b : A) {c : A} (Hc : c ≠ 0) : (a / c) * (c / b) = a / b := + by rewrite [-mul_div_assoc, div_mul_cancel _ Hc] + +lemma div_add_eq_add_mul_div {A : Type} [field A] (a b c : A) (Hb : b ≠ 0) : (a / b) + c = (a + c * b) / b := + by rewrite [-div_add_div_same, mul_div_cancel _ Hb] + +-- I'm not sure why smul_approaches doesn't unify where I use this? +lemma real_limit_helper {U : Type} [normed_vector_space U] {f : U → ℝ} {a : ℝ} {x : U} + (Hf : f ⟶ a [at x]) (c : ℝ) : (λ y, c * f y) ⟶ c * a [at x] := + begin + apply smul_approaches, + exact Hf + end variables {U V W : Type} variables [HU : normed_vector_space U] [HV : normed_vector_space V] [HW : normed_vector_space W] @@ -388,15 +467,122 @@ variables {f : V → W} {g : U → V} variables {A : V → W} {B : U → V} variables [HA : is_bdd_linear_map A] [HB : is_bdd_linear_map B] variable {x : U} + include HU HV HW HA HB +-- this takes 2 seconds without clearing the contexts before simp theorem frechet_derivative_at_comp (Hg : is_frechet_deriv_at g B x) (Hf : is_frechet_deriv_at f A (g x)) : @is_frechet_deriv_at _ _ _ _ (λ y, f (g y)) (λ y, A (B y)) !is_bdd_linear_map_comp x := begin - rewrite ↑is_frechet_deriv_at, - intros ε Hε, + unfold is_frechet_deriv_at, + note Hf' := is_frechet_deriv_at_elim Hf, + note Hg' := is_frechet_deriv_at_elim Hg, + have H : ∀ h, f (g (x + h)) - f (g x) - A (B h) = + (A (g (x + h) - g x - B h)) + (-f (g x) + f (g (x + h)) + A (g x - g (x + h))), + begin intro; rewrite [3 hom_sub A], clear [Hf, Hg, Hf', Hg'], simp end, -- .5 seconds for simp + have H' : (λ h, ∥f (g (x + h)) - f (g x) - A (B h)∥ / ∥h∥) = + (λ h, ∥(A (g (x + h) - g x - B h)) + (-f (g x) + f (g (x + h)) + A (g x - g (x + h)))∥ / ∥h∥), + from funext (λ h, by rewrite H), + rewrite H', + clear [H, H'], + apply approaches_squeeze, -- show the limit holds by bounding it by something that vanishes + {apply approaches_constant}, + rotate 1, + {apply filter.eventually_of_forall, intro, apply div_nonneg_of_nonneg_of_nonneg, repeat apply norm_nonneg}, + {apply filter.eventually_of_forall, intro, + apply div_le_div_of_le_of_nonneg, + apply norm_triangle, + apply norm_nonneg}, + have H : (λ (y : U), (∥A (g (x + y) - g x - B y)∥ + ∥-f (g x) + f (g (x + y)) + A (g x - g (x + y))∥) / ∥y∥) = + (λ (y : U), (∥A (g (x + y) - g x - B y)∥ / ∥y∥ + ∥-f (g x) + f (g (x + y)) + A (g x - g (x + y))∥ / ∥y∥)), + from funext (λ y, by rewrite [div_add_div_same]), + rewrite [H, -zero_add 0], -- the function is a sum of two things that both vanish + clear H, + apply add_approaches, + {apply approaches_squeeze, -- show the lhs vanishes by squeezing it again + {apply approaches_constant}, + rotate 1, + {apply filter.eventually_of_forall, intro, apply div_nonneg_of_nonneg_of_nonneg, repeat apply norm_nonneg}, + {apply filter.eventually_of_forall, intro y, + show ∥A (g (x + y) - g x - B y)∥ / ∥y∥ ≤ op_norm A * (∥(g (x + y) - g x - B y)∥ / ∥y∥), begin + rewrite -mul_div_assoc, + apply div_le_div_of_le_of_nonneg, + apply op_norm_bound A, + apply norm_nonneg + end}, + {rewrite [-mul_zero (op_norm A)], + apply real_limit_helper, + apply Hg}}, -- we have shown the lhs vanishes. now the rhs + {have H : ∀ y, (∥-f (g x) + f (g (x + y)) + A (g x - g (x + y))∥ / ∥y∥) = + ((∥(f (g (x + y)) - f (g x)) - A (g (x + y) - g x) ∥ / ∥g (x + y) - g x∥) * (∥g (x + y) - g x∥ / ∥y∥)), + begin + intro, + cases em (g (x + y) - g x = 0) with Heq Hneq, + {note Heq' := eq_of_sub_eq_zero Heq, + rewrite [Heq', neg_add_eq_sub, *sub_self, hom_zero A, add_zero, *norm_zero, div_zero, zero_div]}, + {rewrite [div_mul_div_cancel _ _ (norm_ne_zero_of_ne_zero Hneq), *sub_eq_add_neg, + -hom_neg A], + simp} --(.5 seconds) + end, + apply approaches_squeeze, -- again, by squeezing + {apply approaches_constant}, + rotate 1, + {apply filter.eventually_of_forall, intro, apply div_nonneg_of_nonneg_of_nonneg, repeat apply norm_nonneg}, + {apply filter.eventually_of_forall, intro y, rewrite H, + apply mul_le_mul_of_nonneg_left, + {show ∥g (x + y) - g x∥ / ∥y∥ ≤ ∥g (x + y) - g x - B y∥ / ∥y∥ + op_norm B, begin + cases em (y = 0) with Heq Hneq, + {rewrite [Heq, norm_zero, *div_zero, zero_add], apply le_of_lt, apply op_norm_pos}, + rewrite [div_add_eq_add_mul_div _ _ _ (norm_ne_zero_of_ne_zero Hneq)], + apply div_le_div_of_le_of_nonneg, + apply le.trans, + rotate 1, + apply add_le_add_left, + apply op_norm_bound, + apply norm_nonneg, + rewrite [-neg_add_cancel_right (g (x + y) - g x) (B y) at {1}, -sub_eq_add_neg], + apply norm_triangle + end}, + {apply div_nonneg_of_nonneg_of_nonneg, repeat apply norm_nonneg}}, + -- now to show the bounding function vanishes. it is a product of a vanishing function and a convergent one + apply mul_approaches_zero_of_approaches_zero_of_approaches, + {have H' : (λ (y : U), ∥f (g (x + y)) - f (g x) - A (g (x + y) - g x)∥ / ∥g (x + y) - g x∥) = + (λ (y : U), ∥f (g x + (g (x + y) - g x)) - f (g x) - A (g (x + y) - g x)∥ / ∥g (x + y) - g x∥), + from funext (λ y, by rewrite [add.comm (g x), sub_add_cancel]), -- first, show lhs vanishes + rewrite H', + have Hgcts : continuous_at (λ y, g (x + y) - g x) 0, begin + apply normed_vector_space.continuous_at_intro, + intro ε Hε, + cases normed_vector_space.continuous_at_dest (continuous_at_of_is_frechet_deriv_at g x Hg) _ Hε with δ Hδ, + existsi δ, + split, + exact and.left Hδ, + intro x' Hx', + rewrite [add_zero, sub_self], + rewrite sub_zero, + apply and.right Hδ, + have (x + x') - x = x' - 0, begin clear [Hg, Hf, Hf', Hg', H, H', Hδ, Hx'], simp end, -- (.6 seconds w/o clear, .1 with) + rewrite this, + apply Hx' + end, + have Hfcts : continuous_at (λ (x' : V), ∥f (g x + x') - f (g x) - A x'∥ / ∥x'∥) (g (x + 0) - g x), begin + rewrite [add_zero, sub_self], + apply diff_quot_cts, + exact Hf + end, + have Heqz : ∥f (g x + (g (x + 0) - g x)) - f (g x) - A (g (x + 0) - g x)∥ / ∥g (x + 0) - g x∥ = 0, + by rewrite [*add_zero, sub_self, norm_zero, div_zero], + apply @tendsto_comp _ _ _ (λ y, g (x + y) - g x), + apply tendsto_inf_left, + apply tendsto_at_of_continuous_at Hgcts, + note Hfcts' := tendsto_at_of_continuous_at Hfcts, + rewrite Heqz at Hfcts', + exact Hfcts'}, -- finally, show rhs converges to op_norm B + {apply add_approaches, + apply Hg, + apply approaches_constant}} end -end comp-/ +end comp end analysis diff --git a/library/theories/analysis/ivt.lean b/library/theories/analysis/ivt.lean index edc4ac125..527a3ebfc 100644 --- a/library/theories/analysis/ivt.lean +++ b/library/theories/analysis/ivt.lean @@ -204,7 +204,7 @@ theorem intermediate_value_decr_zero {f : ℝ → ℝ} (Hf : continuous f) {a b 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, + have Hcon : continuous (λ x, - f x), from neg_continuous Hf, let Hiv := intermediate_value_incr_zero Hcon Hab Ha' Hb', cases Hiv with c Hc, existsi c, @@ -220,7 +220,7 @@ theorem intermediate_value_incr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ (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 Hcon : continuous (λ x, f x - v), from sub_continuous Hf (continuous_const _), 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 @@ -230,7 +230,7 @@ theorem intermediate_value_decr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ (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 Hcon : continuous (λ x, f x - v), from sub_continuous Hf (continuous_const _), 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 diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index 0bf37e813..c6b36609e 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -2,6 +2,8 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Metric spaces. + +Authors: Jeremy Avigad, Robert Y. Lewis -/ import data.real.complete data.pnat ..topology.continuous ..topology.limit data.set open nat real eq.ops classical set prod set.filter topology interval @@ -215,6 +217,11 @@ proposition eventually_at_iff (P : M → Prop) (x : M) : eventually P [at x] ↔ ∃ ε, ε > 0 ∧ ∀ ⦃x'⦄, dist x' x < ε → x' ≠ x → P x' := iff.intro eventually_at_dest (λ H, obtain ε [εpos Hε], from H, eventually_at_intro εpos Hε) +end metric_space_M + +namespace metric_space +variables {M : Type} [metric_space M] + section approaches variables {X : Type} {F : filter X} {f : X → M} {y : M} @@ -236,13 +243,11 @@ section approaches proposition approaches_iff : (f ⟶ y) F ↔ (∀ ε, ε > 0 → eventually (λ x, dist (f x) y < ε) F) := iff.intro approaches_dest approaches_intro - -- TODO: prove this in greater generality in topology.limit - proposition approaches_constant : ((λ x, y) ⟶ y) F := - approaches_intro (λ ε εpos, eventually_of_forall F (λ x, - show dist y y < ε, by rewrite dist_self; apply εpos)) end approaches -- here we full unwrap two particular kinds of convergence3 +-- TODO: put these in metric space namespace? (will have similar in normed_space + proposition approaches_at_infty_intro {f : ℕ → M} {y : M} (H : ∀ ε, ε > 0 → ∃ N, ∀ n, n ≥ N → dist (f n) y < ε) : @@ -282,8 +287,13 @@ proposition approaches_at_iff (f : M → N) (y : N) (x : M) : f ⟶ y [at x] ↔ iff.intro approaches_at_dest approaches_at_intro end metric_space_N +end metric_space -- close namespace --- TODO: remove this. It is only here temporarily, because it is used in normed_space +section metric_space_M +variables {M : Type} [metric_space M] +-- TODO: remove this. It is only here temporarily, because it is used in normed_space (JA) +-- It is used in the definition of a complete metric space below, but I think it doesn't +-- have to be a class (RL) abbreviation converges_seq [class] (X : ℕ → M) : Prop := ∃ y, X ⟶ y [at ∞] -- TODO: refactor @@ -291,7 +301,7 @@ abbreviation converges_seq [class] (X : ℕ → M) : Prop := ∃ y, X ⟶ y [at definition approaches_at_infty_intro' {X : ℕ → M} {y : M} (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → dist (X n) y ≤ ε) : (X ⟶ y) [at ∞] := -approaches_at_infty_intro +metric_space.approaches_at_infty_intro take ε, assume epos : ε > 0, have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos, obtain N HN, from H e2pos, @@ -308,9 +318,9 @@ eq_of_forall_dist_le (take ε, suppose ε > 0, have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos, obtain N₁ (HN₁ : ∀ {n}, n ≥ N₁ → dist (X n) y₁ < ε / 2), - from approaches_at_infty_dest H₁ e2pos, + from metric_space.approaches_at_infty_dest H₁ e2pos, obtain N₂ (HN₂ : ∀ {n}, n ≥ N₂ → dist (X n) y₂ < ε / 2), - from approaches_at_infty_dest H₂ e2pos, + from metric_space.approaches_at_infty_dest H₂ e2pos, let N := max N₁ N₂ in have dN₁ : dist (X N) y₁ < ε / 2, from HN₁ !le_max_left, have dN₂ : dist (X N) y₂ < ε / 2, from HN₂ !le_max_right, @@ -347,11 +357,10 @@ have aux : (λ n, X (k + n)) = (λ n, X (n + k)), from funext (take n, by rewrit by rewrite aux at H; exact converges_to_seq_of_converges_to_seq_offset H -/ ---<<<<<<< HEAD proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x [at ∞]) : ∃ K : ℝ, ∀ n : ℕ, dist (X n) x ≤ K := have eventually (λ n, dist (X n) x < 1) [at ∞], - from approaches_dest H zero_lt_one, + from metric_space.approaches_dest H zero_lt_one, obtain N (HN : ∀ n, n ≥ N → dist (X n) x < 1), from eventually_at_infty_dest this, let K := max 1 (Max i ∈ '(-∞, N), dist (X i) x) in @@ -363,12 +372,22 @@ proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x [at else show dist (X n) x ≤ K, from le.trans (le_of_lt (HN n (le_of_not_gt Hn))) !le_max_left) ---======= -/-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 _ X y 1 H +proposition bounded_of_converges {A : Type} {X : A → M} {x : M} {F} (H : (X ⟶ x) F) : + ∃ K : ℝ, eventually (λ n, dist (X n) x ≤ K) F := + begin + note H' := metric_space.approaches_dest H zero_lt_one, + existsi 1, + apply eventually_mono H', + intro x' Hx', + apply le_of_lt Hx' + end + +/-proposition converges_to_seq_of_converges_to_seq_offset_succ + {X : ℕ → M} {y : M} (H : (λ n, X (succ n)) ⟶ y [at ∞]) : + X ⟶ y [at ∞] := +@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 ℕ) := iff.intro converges_to_seq_of_converges_to_seq_offset !converges_to_seq_offset @@ -380,49 +399,7 @@ iff.intro converges_to_seq_of_converges_to_seq_offset_left !converges_to_seq_off 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 - -section -open list -private definition r_trans : transitive (@le ℝ _) := λ a b c, !le.trans -private definition r_refl : reflexive (@le ℝ _) := λ a, !le.refl - -proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x in ℕ) : - ∃ K : ℝ, ∀ n : ℕ, dist (X n) x ≤ K := - begin - cases H zero_lt_one with N HN, - cases em (N = 0), - existsi 1, - intro n, - apply le_of_lt, - apply HN, - rewrite a, - apply zero_le, - let l := map (λ n : ℕ, -dist (X n) x) (upto N), - have Hnenil : l ≠ nil, from (map_ne_nil_of_ne_nil _ (upto_ne_nil_of_ne_zero a)), - existsi max (-list.min (λ a b : ℝ, le a b) l Hnenil) 1, - intro n, - have Hsmn : ∀ m : ℕ, m < N → dist (X m) x ≤ max (-list.min (λ a b : ℝ, le a b) l Hnenil) 1, begin - intro m Hm, - apply le.trans, - rotate 1, - apply le_max_left, - note Hall := min_lemma real.le_total r_trans r_refl Hnenil, - have Hmem : -dist (X m) x ∈ (map (λ (n : ℕ), -dist (X n) x) (upto N)), from mem_map _ (mem_upto_of_lt Hm), - note Hallm' := of_mem_of_all Hmem Hall, - apply le_neg_of_le_neg, - exact Hallm' - end, - cases em (n < N) with Elt Ege, - apply Hsmn, - exact Elt, - apply le_of_lt, - apply lt_of_lt_of_le, - apply HN, - apply le_of_not_gt Ege, - apply le_max_right - end -end ->>>>>>> feat(library/analysis): basic properties about real derivatives-/ +-/ /- cauchy sequences -/ @@ -433,7 +410,7 @@ proposition cauchy_of_converges_seq {X : ℕ → M} (H : ∃ y, X ⟶ y [at ∞] take ε, suppose ε > 0, obtain y (Hy : X ⟶ y [at ∞]), from H, have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos, - have eventually (λ n, dist (X n) y < ε / 2) [at ∞], from approaches_dest Hy e2pos, + have eventually (λ n, dist (X n) y < ε / 2) [at ∞], from metric_space.approaches_dest Hy e2pos, obtain N (HN : ∀ {n}, n ≥ N → dist (X n) y < ε / 2), from eventually_at_infty_dest this, exists.intro N (take m n, suppose m ≥ N, suppose n ≥ N, @@ -452,41 +429,10 @@ end metric_space_M section metric_space_M_N variables {M N : Type} [metric_space M] [metric_space N] -/- -definition converges_to_at (f : M → N) (y : N) (x : M) := -∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ≠ x ∧ dist x' x < δ → dist (f x') y < ε - -notation f `⟶` y `at` x := converges_to_at f y x - -theorem converges_to_at_constant (y : N) (x : M) : (λ m, y) ⟶ y at x := - begin - intros ε Hε, - existsi 1, - split, - exact zero_lt_one, - intros x' Hx', - rewrite dist_self, - apply Hε - end - -definition converges_at [class] (f : M → N) (x : M) := -∃ y, converges_to_at f y x - -noncomputable definition limit_at (f : M → N) (x : M) [H : converges_at f x] : N := -some H - -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 - --/ -- TODO: refactor section open pnat rat -private lemma of_rat_rat_of_pnat_eq_of_nat_nat_of_pnat (p : pnat) : - of_rat (rat_of_pnat p) = of_nat (nat_of_pnat p) := - rfl theorem cnv_real_of_cnv_nat {X : ℕ → M} {c : M} (H : ∀ n : ℕ, dist (X n) c < 1 / (real.of_nat n + 1)) : ∀ ε : ℝ, ε > 0 → ∃ N : ℕ, ∀ n : ℕ, n ≥ N → dist (X n) c < ε := @@ -512,51 +458,33 @@ theorem cnv_real_of_cnv_nat {X : ℕ → M} {c : M} (H : ∀ n : ℕ, dist (X n) krewrite -of_rat_zero, apply of_rat_lt_of_rat_of_lt, apply rat_of_pnat_is_pos, - krewrite [of_rat_rat_of_pnat_eq_of_nat_nat_of_pnat, -real.of_nat_add], + change of_nat (nat_of_pnat p) ≤ n + 1, + krewrite [-real.of_nat_add], apply real.of_nat_le_of_nat_of_le, apply le_add_of_le_right, assumption end end --- a nice illustration of the limit library: [at c] and [at ∞] can be replaced by any filters -theorem comp_approaches_at_infty {f : M → N} {c : M} {l : N} (Hf : f ⟶ l [at c]) - {X : ℕ → M} (HX₁ : X ⟶ c [at ∞]) (HX₂ : eventually (λ n, X n ≠ c) [at ∞]) : - (λ n, f (X n)) ⟶ l [at ∞] := - tendsto_comp_of_approaches_of_tendsto_at HX₁ HX₂ Hf - --- TODO: refactor - +-- TODO : refactor theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N) - (Hseq : ∀ X : ℕ → M, ((∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c [at ∞])) → ((λ n : ℕ, f (X n)) ⟶ l [at ∞]))) + (Hseq : ∀ X : ℕ → M, (eventually (λ n, X n ≠ c) [at ∞] ∧ (X ⟶ c [at ∞])) → ((λ n : ℕ, f (X n)) ⟶ l [at ∞])) : f ⟶ l [at c] := - by_contradiction - (assume Hnot : ¬ (f ⟶ l [at c]), - obtain ε Hε, from exists_not_of_not_forall (λ H, Hnot (approaches_at_intro H)), - let Hε' := and_not_of_not_implies Hε in - obtain (H1 : ε > 0) H2, from Hε', - have H3 : ∀ δ : ℝ, (δ > 0 → ∃ x' : M, x' ≠ c ∧ dist x' c < δ ∧ dist (f x') l ≥ ε), begin -- tedious!! - intros δ Hδ, - note Hε'' := forall_not_of_not_exists H2, - note H4 := forall_not_of_not_exists H2 δ, - have ¬ (∀ x' : M, dist x' c < δ → x' ≠ c → dist (f x') l < ε), - from λ H', H4 (and.intro Hδ H'), - note H5 := exists_not_of_not_forall this, - cases H5 with x' Hx', + begin + eapply by_contradiction, + intro Hnot, + cases exists_not_of_not_forall (λ H, Hnot (metric_space.approaches_at_intro H)) with ε Hε, + cases and_not_of_not_implies Hε with H1 H2, + note H3' := forall_not_of_not_exists H2, + have H3 : ∀ δ, δ > 0 → (∃ x', dist x' c < δ ∧ x' ≠ c ∧ dist (f x') l ≥ ε), begin + intro δ Hδ, + cases exists_not_of_not_forall (or.resolve_left (not_or_not_of_not_and' (H3' δ)) (not_not_intro Hδ)) + with x' Hx', existsi x', - note H6 := and_not_of_not_implies Hx', --- rewrite and.assoc at H6, - cases H6 with H6a H6b, - split, - cases (and_not_of_not_implies H6b), - assumption, - split, - assumption, - apply le_of_not_gt, - cases (and_not_of_not_implies H6b), - assumption + rewrite [2 not_implies_iff_and_not at Hx', ge_iff_not_lt], + exact Hx' end, - let S : ℕ → M → Prop := λ n x, 0 < dist x c ∧ dist x c < 1 / (of_nat n + 1) ∧ dist (f x) l ≥ ε in + let S := λ (n : ℕ) (x : M), 0 < dist x c ∧ dist x c < 1 / (of_nat n + 1) ∧ dist (f x) l ≥ ε, have HS : ∀ n : ℕ, ∃ m : M, S n m, begin intro k, have Hpos : 0 < of_nat k + 1, from of_nat_succ_pos k, @@ -571,55 +499,57 @@ theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N) split, repeat assumption end, - let X : ℕ → M := λ n, some (HS n) in - have H4 : ∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c [at ∞]), from - (take n, and.intro - (begin - note Hspec := some_spec (HS n), - esimp, esimp at Hspec, - cases Hspec, - apply ne_of_dist_pos, - assumption - end) - (begin - apply approaches_at_infty_intro, - apply cnv_real_of_cnv_nat, - intro m, - note Hspec := some_spec (HS m), - esimp, esimp at Hspec, - cases Hspec with Hspec1 Hspec2, - cases Hspec2, - assumption - end)), - have H5 : (λ n : ℕ, f (X n)) ⟶ l [at ∞], from Hseq X H4, - begin - note H6 := approaches_at_infty_dest H5 H1, - cases H6 with Q HQ, - note HQ' := HQ !le.refl, - esimp at HQ', - apply absurd HQ', - apply not_lt_of_ge, - note H7 := some_spec (HS Q), - esimp at H7, - cases H7 with H71 H72, - cases H72, - assumption - end) + let X := λ n, some (HS n), + have H4 : (eventually (λ n, X n ≠ c) [at ∞]) ∧ (X ⟶ c [at ∞]), begin + split, + {fapply @eventually_at_infty_intro, + exact 0, + intro n Hn, + note Hspec := some_spec (HS n), + esimp, esimp at Hspec, + cases Hspec, + apply ne_of_dist_pos, + assumption}, + {intro, + apply metric_space.approaches_at_infty_intro, + apply cnv_real_of_cnv_nat, + intro m, + note Hspec := some_spec (HS m), + esimp, esimp at Hspec, + cases Hspec with Hspec1 Hspec2, + cases Hspec2, + assumption} + end, + have H5 : (λ n, f (X n)) ⟶ l [at ∞], from Hseq X H4, + note H6 := metric_space.approaches_at_infty_dest H5 H1, + cases H6 with Q HQ, + note HQ' := HQ !le.refl, + esimp at HQ', + apply absurd HQ', + apply not_lt_of_ge, + note H7 := some_spec (HS Q), + esimp at H7, + cases H7 with H71 H72, + cases H72, + assumption + end end metric_space_M_N +namespace metric_space + section continuity variables {M N : Type} [Hm : metric_space M] [Hn : metric_space N] include Hm Hn open topology set -- the ε - δ definition of continuity is equivalent to the topological definition -theorem continuous_at_intro {f : M → N} {x : M} - (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε) : - continuous_at f x := + +theorem continuous_at_within_intro {f : M → N} {x : M} {s : set M} + (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → dist x' x < δ → dist (f x') (f x) < ε) : + continuous_at_on f x s := begin - rewrite ↑continuous_at, - intros U Uopen HfU, + intro U Uopen HfU, cases exists_open_ball_subset_of_Open_of_mem Uopen HfU with r Hr, cases Hr with Hr HUr, cases H Hr with δ Hδ, @@ -633,15 +563,15 @@ theorem continuous_at_intro {f : M → N} {x : M} intro y Hy, apply mem_preimage, apply HUr, - note Hy'' := Hx'δ Hy, - exact Hy'' + apply Hx'δ, + apply and.right Hy, + apply and.left Hy end -theorem continuous_at_elim {f : M → N} {x : M} (Hfx : continuous_at f x) : - ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε := +theorem continuous_at_on_dest {f : M → N} {x : M} {s : set M} (Hfx : continuous_at_on f x s) : + ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → dist x' x < δ → dist (f x') (f x) < ε := begin intros ε Hε, - rewrite [↑continuous_at at Hfx], cases @Hfx (open_ball (f x) ε) !Open_open_ball (mem_open_ball _ Hε) with V HV, cases HV with HV HVx, cases HVx with HVx HVf, @@ -650,94 +580,58 @@ theorem continuous_at_elim {f : M → N} {x : M} (Hfx : continuous_at f x) : existsi δ, split, exact Hδ, - intro x' Hx', + intro x' Hx's Hx', apply HVf, + apply and.intro, apply Hδx, - apply Hx', + exact Hx', + exact Hx's 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_intro {f : M → N} {x : M} + (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε) : + continuous_at f x := + continuous_at_of_continuous_at_on_univ + (continuous_at_within_intro + (take ε, suppose ε > 0, + obtain δ (Hδ : δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε), from H this, + exists.intro δ (and.intro + (show δ > 0, from and.left Hδ) + (take x' H' Hx', and.right Hδ _ Hx')))) -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) < ε := +theorem continuous_at_dest {f : M → N} {x : M} (Hfx : continuous_at f x) : + ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, 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δ, + cases continuous_at_on_dest (continuous_at_on_univ_of_continuous_at Hfx) Hε 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' + intro x' Hx', + apply and.right Hδ, + apply mem_univ, + apply Hx' 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) < ε) : + (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, 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 + continuous_on_of_forall_continuous_at_on (λ x, continuous_at_within_intro (H x)) -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_on_dest {f : M → N} {s : set M} (H : continuous_on f s) {x : M} (Hxs : x ∈ s) : + ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → dist x' x < δ → dist (f x') (f x) < ε := + continuous_at_on_dest (continuous_at_on_of_continuous_on H Hxs) ---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 +theorem continuous_intro {f : M → N} + (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε) : + continuous f := + continuous_of_forall_continuous_at (λ x, continuous_at_intro (H x)) + +theorem continuous_dest {f : M → N} (H : continuous f) (x : M) : + ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε := + continuous_at_dest (forall_continuous_at_of_continuous H x) + +theorem continuous_at_of_converges_to_at {f : M → N} {x : M} (Hf : f ⟶ f x [at x]) : continuous_at f x := continuous_at_intro (take ε, suppose ε > 0, @@ -755,11 +649,9 @@ theorem converges_to_at_of_continuous_at {f : M → N} {x : M} (Hf : continuous_ f ⟶ f x [at x] := approaches_at_intro (take ε, suppose ε > 0, - obtain δ [δpos Hδ], from continuous_at_elim Hf this, + obtain δ [δpos Hδ], from continuous_at_dest Hf this, exists.intro δ (and.intro δpos (λ x' Hx' xnex', Hδ x' Hx'))) ---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) : converges_seq (λ n, f (X n)) := @@ -768,7 +660,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 (forall_continuous_at_of_continuous Hf xlim)) Hε, + let Hcont := (continuous_at_dest (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, @@ -777,22 +669,10 @@ theorem converges_seq_comp_of_converges_seq_of_cts (X : ℕ → M) [HX : converg apply HB Hn end -omit Hn -theorem id_continuous : continuous (λ x : M, x) := - begin - apply continuous_of_forall_continuous_at, - intros x, - apply continuous_at_intro, - intro ε Hε, - existsi ε, - split, - assumption, - intros, - assumption - end - end continuity +end metric_space + end analysis diff --git a/library/theories/analysis/normed_space.lean b/library/theories/analysis/normed_space.lean index 4deacc0bd..04e29781e 100644 --- a/library/theories/analysis/normed_space.lean +++ b/library/theories/analysis/normed_space.lean @@ -6,7 +6,7 @@ Author: Jeremy Avigad Normed spaces. -/ import algebra.module .metric_space -open real nat classical topology analysis +open real nat classical topology analysis analysis.metric_space noncomputable theory structure has_norm [class] (M : Type) : Type := @@ -79,6 +79,8 @@ namespace analysis proposition norm_sub (u v : V) : ∥u - v∥ = ∥v - u∥ := by rewrite [-norm_neg, neg_sub] + proposition norm_ne_zero_of_ne_zero {u : V} (H : u ≠ 0) : ∥u∥ ≠ 0 := + suppose ∥u∥ = 0, H (eq_zero_of_norm_eq_zero this) end analysis @@ -117,7 +119,7 @@ section open nat - proposition converges_to_seq_norm_elim {X : ℕ → V} {x : V} (H : X ⟶ x [at ∞]) : + proposition approaches_seq_norm_elim {X : ℕ → V} {x : V} (H : X ⟶ x [at ∞]) : ∀ {ε : ℝ}, ε > 0 → ∃ N₁ : ℕ, ∀ {n : ℕ}, n ≥ N₁ → ∥ X n - x ∥ < ε := approaches_at_infty_dest H @@ -147,137 +149,274 @@ definition banach_space_to_metric_space [trans_instance] (V : Type) [bsV : banac ⦄ namespace analysis + +-- unfold some common definitions fully (copied from metric space, updated for normed_space notation) +-- TODO: copy these for ℝ as well? +namespace normed_vector_space +section +open set topology set.filter +variables {M N : Type} +--variable [HU : normed_vector_space U] +variable [normed_vector_space M] +--variables {f g : U → V} + +section approaches + variables {X : Type} {F : filter X} {f : X → M} {y : M} + + proposition approaches_intro (H : ∀ ε, ε > 0 → eventually (λ x, ∥(f x) - y∥ < ε) F) : + (f ⟶ y) F := + approaches_intro H + + proposition approaches_dest (H : (f ⟶ y) F) {ε : ℝ} (εpos : ε > 0) : + eventually (λ x, ∥(f x) - y∥ < ε) F := + approaches_dest H εpos + + variables (F f y) + + proposition approaches_iff : ((f ⟶ y) F) ↔ (∀ ε, ε > 0 → eventually (λ x, ∥(f x) - y∥ < ε) F) := + iff.intro approaches_dest approaches_intro + +end approaches + +proposition approaches_at_infty_intro {f : ℕ → M} {y : M} + (H : ∀ ε, ε > 0 → ∃ N, ∀ n, n ≥ N → ∥(f n) - y∥ < ε) : + f ⟶ y [at ∞] := +approaches_at_infty_intro H + +proposition approaches_at_infty_dest {f : ℕ → M} {y : M} + (H : f ⟶ y [at ∞]) ⦃ε : ℝ⦄ (εpos : ε > 0) : + ∃ N, ∀ ⦃n⦄, n ≥ N → ∥(f n) - y∥ < ε := +approaches_at_infty_dest H εpos + +proposition approaches_at_infty_iff (f : ℕ → M) (y : M) : + f ⟶ y [at ∞] ↔ (∀ ε, ε > 0 → ∃ N, ∀ ⦃n⦄, n ≥ N → ∥(f n) - y∥ < ε) := +iff.intro approaches_at_infty_dest approaches_at_infty_intro + +variable [normed_vector_space N] + +proposition approaches_at_dest {f : M → N} {y : N} {x : M} + (H : f ⟶ y [at x]) ⦃ε : ℝ⦄ (εpos : ε > 0) : + ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, ∥x' - x∥ < δ → x' ≠ x → ∥(f x') - y∥ < ε := +approaches_at_dest H εpos + +proposition approaches_at_intro {f : M → N} {y : N} {x : M} + (H : ∀ ε, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, ∥x' - x∥ < δ → x' ≠ x → ∥(f x') - y∥ < ε) : + f ⟶ y [at x] := +approaches_at_intro H + +proposition approaches_at_iff (f : M → N) (y : N) (x : M) : f ⟶ y [at x] ↔ + (∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, ∥x' - x∥ < δ → x' ≠ x → ∥(f x') - y∥ < ε) := +iff.intro approaches_at_dest approaches_at_intro + +end +end normed_vector_space + + +section variable {V : Type} variable [normed_vector_space V] +variable {A : Type} +variables {X : A → V} +variables {x : V} -variables {X Y : ℕ → V} -variables {x y : V} - -proposition add_converges_to_seq (HX : X ⟶ x [at ∞]) (HY : Y ⟶ y [at ∞]) : - (λ n, X n + Y n) ⟶ x + y [at ∞] := -approaches_at_infty_intro -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) - -private lemma smul_converges_to_seq_aux {c : ℝ} (cnz : c ≠ 0) (HX : X ⟶ x [at ∞]) : - (λ n, c • X n) ⟶ c • x [at ∞] := -approaches_at_infty_intro -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)) - -proposition smul_converges_to_seq (c : ℝ) (HX : X ⟶ x [at ∞]) : - (λ n, c • X n) ⟶ c • x [at ∞] := -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 approaches_constant end) - (suppose c ≠ 0, smul_converges_to_seq_aux this HX) - -proposition neg_converges_to_seq (HX : X ⟶ x [at ∞]) : - (λ n, - X n) ⟶ - x [at ∞] := -approaches_at_infty_intro -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 [at ∞]) ↔ (X ⟶ x [at ∞]) := -have aux : X = λ n, (- (- X n)), from funext (take n, by rewrite neg_neg), -iff.intro - (assume H : (λ n, -X n)⟶ -x [at ∞], - show X ⟶ x [at ∞], 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 [at ∞]) : (λ n, norm (X n)) ⟶ 0 [at ∞] := -approaches_at_infty_intro -take ε, suppose ε > 0, -obtain N (HN : ∀ n, n ≥ N → norm (X n - 0) < ε), from approaches_at_infty_dest 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) < ε, - 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 [at ∞]) : - X ⟶ 0 [at ∞] := -approaches_at_infty_intro -take ε, suppose ε > 0, -obtain N (HN : ∀ n, n ≥ N → abs (norm (X n) - 0) < ε), from approaches_at_infty_dest 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) < ε, - by rewrite sub_zero; apply this) - -proposition norm_converges_to_seq_zero_iff (X : ℕ → V) : - ((λ n, norm (X n)) ⟶ 0 [at ∞]) ↔ (X ⟶ 0 [at ∞]) := -iff.intro converges_to_seq_zero_of_norm_converges_to_seq_zero norm_converges_to_seq_zero - -end analysis - -namespace analysis -variables {U V : Type} -variable [HU : normed_vector_space U] -variable [HV : normed_vector_space V] -variables f g : U → V - -include HU HV - -theorem add_converges_to_at {lf lg : V} {x : U} (Hf : f ⟶ lf at x) (Hg : g ⟶ lg at x) : - (λ y, f y + g y) ⟶ lf + lg at x := +proposition neg_approaches {F} (HX : (X ⟶ x) F) : + ((λ n, - X n) ⟶ - x) F := begin - apply converges_to_at_of_all_conv_seqs, - intro X HX, - apply add_converges_to_seq, - apply all_conv_seqs_of_converges_to_at Hf, - apply HX, - apply all_conv_seqs_of_converges_to_at Hg, - apply HX + apply normed_vector_space.approaches_intro, + intro ε Hε, + apply set.filter.eventually_mono (approaches_dest HX Hε), + intro x' Hx', + rewrite [-norm_neg, neg_neg_sub_neg], + apply Hx' end -open topology +proposition approaches_neg {F} (Hx : ((λ n, - X n) ⟶ - x) F) : (X ⟶ x) F := + have aux : X = λ n, (- (- X n)), from funext (take n, by rewrite neg_neg), + by rewrite [aux, -neg_neg x]; exact neg_approaches Hx -theorem normed_vector_space.continuous_at_intro {x : U} +proposition neg_approaches_iff {F} : (((λ n, - X n) ⟶ - x) F) ↔ ((X ⟶ x) F) := +have aux : X = λ n, (- (- X n)), from funext (take n, by rewrite neg_neg), +iff.intro approaches_neg neg_approaches + +proposition norm_approaches_zero_of_approaches_zero {F} (HX : (X ⟶ 0) F) : ((λ n, norm (X n)) ⟶ 0) F := + begin + apply metric_space.approaches_intro, + intro ε Hε, + apply set.filter.eventually_mono (approaches_dest HX Hε), + intro x Hx, + change abs (∥X x∥ - 0) < ε, + rewrite [sub_zero, abs_of_nonneg !norm_nonneg, -sub_zero (X x)], + apply Hx + end + +proposition approaches_zero_of_norm_approaches_zero + {F} (HX : ((λ n, norm (X n)) ⟶ 0) F) : + (X ⟶ 0) F := + begin + apply normed_vector_space.approaches_intro, + intro ε Hε, + apply set.filter.eventually_mono (approaches_dest HX Hε), + intro x Hx, + apply lt_of_abs_lt, + rewrite [sub_zero, -sub_zero ∥X x∥], + apply Hx + end + +proposition norm_approaches_zero_iff (X : ℕ → V) (F) : + (((λ n, norm (X n)) ⟶ 0) F) ↔ ((X ⟶ 0) F) := +iff.intro approaches_zero_of_norm_approaches_zero norm_approaches_zero_of_approaches_zero + +end + + +section +variables {U V : Type} +--variable [HU : normed_vector_space U] +variable [HV : normed_vector_space V] +variables {f g : U → V} +open set-- filter causes error?? +include HV + +theorem add_approaches {lf lg : V} {F : filter U} (Hf : (f ⟶ lf) F) (Hg : (g ⟶ lg) F) : + ((λ y, f y + g y) ⟶ lf + lg) F := + begin + apply normed_vector_space.approaches_intro, + intro ε Hε, + have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos Hε two_pos, + have Hfl : filter.eventually (λ x, dist (f x) lf < ε / 2) F, from approaches_dest Hf e2pos, + have Hgl : filter.eventually (λ x, dist (g x) lg < ε / 2) F, from approaches_dest Hg e2pos, + apply filter.eventually_mono, + apply filter.eventually_and Hfl Hgl, + intro x Hfg, + rewrite [add_sub_comm, -add_halves ε], + apply lt_of_le_of_lt, + apply norm_triangle, + cases Hfg with Hf' Hg', + apply add_lt_add, + exact Hf', exact Hg' + end + +theorem smul_approaches {lf : V} {F : filter U} (Hf : (f ⟶ lf) F) (s : ℝ) : + ((λ y, s • f y) ⟶ s • lf) F := + begin + apply normed_vector_space.approaches_intro, + intro ε Hε, + cases em (s = 0) with seq sneq, + {have H : (λ x, ∥(s • f x) - (s • lf)∥ < ε) = (λ x, true), + begin apply funext, intro x, rewrite [seq, 2 zero_smul, sub_zero, norm_zero, eq_true], exact Hε end, + rewrite H, + apply filter.eventually_true}, + {have e2pos : ε / abs s > 0, from div_pos_of_pos_of_pos Hε (abs_pos_of_ne_zero sneq), + have H : filter.eventually (λ x, ∥(f x) - lf∥ < ε / abs s) F, from approaches_dest Hf e2pos, + apply filter.eventually_mono H, + intro x Hx, + rewrite [-smul_sub_left_distrib, norm_smul, mul.comm], + apply mul_lt_of_lt_div, + apply abs_pos_of_ne_zero sneq, + apply Hx} + end + +end + +namespace normed_vector_space +variables {U V : Type} +variables [HU : normed_vector_space U] [HV : normed_vector_space V] +variables {f g : U → V} +include HU HV +open set + +theorem continuous_at_within_intro {x : U} {s : set U} + (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε) : + continuous_at_on f x s := + metric_space.continuous_at_within_intro H + +theorem continuous_at_on_dest {x : U} {s : set U} (Hfx : continuous_at_on f x s) : + ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε := + metric_space.continuous_at_on_dest Hfx + +theorem continuous_on_intro {s : set U} + (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε) : + continuous_on f s := + metric_space.continuous_on_intro H + +theorem continuous_on_dest {s : set U} (H : continuous_on f s) {x : U} (Hxs : x ∈ s) : + ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε := + metric_space.continuous_on_dest H Hxs + +theorem continuous_intro + (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε) : + continuous f := + metric_space.continuous_intro H + +theorem continuous_dest (H : continuous f) (x : U) : + ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε := + metric_space.continuous_dest H x + +theorem continuous_at_intro {x : U} (H : ∀ ε : ℝ, ε > 0 → (∃ δ : ℝ, δ > 0 ∧ ∀ x' : U, ∥x' - x∥ < δ → ∥f x' - f x∥ < ε)) : continuous_at f x := - continuous_at_intro H + metric_space.continuous_at_intro H -theorem normed_vector_space.continuous_at_elim {x : U} (H : continuous_at f x) : +theorem continuous_at_dest {x : U} (H : continuous_at f x) : ∀ ε : ℝ, ε > 0 → (∃ δ : ℝ, δ > 0 ∧ ∀ x' : U, ∥x' - x∥ < δ → ∥f x' - f x∥ < ε) := - continuous_at_elim H + metric_space.continuous_at_dest H + +end normed_vector_space + +section + +open topology +variables {U V : Type} +variables [HU : normed_vector_space U] [HV : normed_vector_space V] +variables {f g : U → V} +include HU HV + +theorem neg_continuous (Hf : continuous f) : continuous (λ x : U, - f x) := + begin + apply continuous_of_forall_continuous_at, + intro x, + apply continuous_at_of_tendsto_at, + apply neg_approaches, + apply tendsto_at_of_continuous_at, + apply forall_continuous_at_of_continuous, + apply Hf + end + +theorem add_continuous (Hf : continuous f) (Hg : continuous g) : continuous (λ x, f x + g x) := + begin + apply continuous_of_forall_continuous_at, + intro y, + apply continuous_at_of_tendsto_at, + apply add_approaches, + all_goals apply tendsto_at_of_continuous_at, + all_goals apply forall_continuous_at_of_continuous, + repeat assumption + end + +theorem sub_continuous (Hf : continuous f) (Hg : continuous g) : continuous (λ x, f x - g x) := + begin + apply continuous_of_forall_continuous_at, + intro y, + apply continuous_at_of_tendsto_at, + apply add_approaches, + all_goals apply tendsto_at_of_continuous_at, + all_goals apply forall_continuous_at_of_continuous, + assumption, + apply neg_continuous, + assumption + end + +theorem smul_continuous (s : ℝ) (Hf : continuous f) : continuous (λ x : U, s • f x) := + begin + apply continuous_of_forall_continuous_at, + intro y, + apply continuous_at_of_tendsto_at, + apply smul_approaches, + apply tendsto_at_of_continuous_at, + apply forall_continuous_at_of_continuous, + assumption + end + +end end analysis diff --git a/library/theories/analysis/real_deriv.lean b/library/theories/analysis/real_deriv.lean index 0f86d65fa..16e4c894a 100644 --- a/library/theories/analysis/real_deriv.lean +++ b/library/theories/analysis/real_deriv.lean @@ -6,7 +6,7 @@ Author: Robert Y. Lewis Derivatives on ℝ -/ import .bounded_linear_operator -open real nat classical topology analysis +open real nat classical topology analysis set noncomputable theory namespace real @@ -19,42 +19,42 @@ theorem add_sub_self (a b : ℝ) : a + b - a = b := definition derivative_at (f : ℝ → ℝ) (d x : ℝ) := is_frechet_deriv_at f (λ t, d • t) x -theorem derivative_at_intro (f : ℝ → ℝ) (d x : ℝ) (H : (λ h, (f (x + h) - f x) / h) ⟶ d at 0) : +theorem derivative_at_intro (f : ℝ → ℝ) (d x : ℝ) (H : (λ h, (f (x + h) - f x) / h) ⟶ d [at 0]) : derivative_at f d x := begin apply is_frechet_deriv_at_intro, intros ε Hε, - cases H Hε with δ Hδ, + cases approaches_at_dest H Hε with δ Hδ, existsi δ, split, exact and.left Hδ, intro y Hy, rewrite [-sub_zero y at Hy{2}], - note Hδ' := and.right Hδ y Hy, + note Hδ' := and.right Hδ y (and.right Hy) (and.left Hy), have Hδ'' : abs ((f (x + y) - f x - d * y) / y) < ε, by rewrite [-div_sub_div_same, mul_div_cancel _ (and.left Hy)]; apply Hδ', show abs (f (x + y) - f x - d * y) / abs y < ε, by rewrite -abs_div; apply Hδ'' end +theorem derivative_at_of_frechet_derivative_at {f g : ℝ → ℝ} [is_bdd_linear_map g] {d x : ℝ} + (H : is_frechet_deriv_at f g x) (Hg : g = λ x, d * x) : + derivative_at f d x := + by apply is_frechet_deriv_at_of_eq H Hg + theorem deriv_at_const (c x : ℝ) : derivative_at (λ t, c) 0 x := - begin - apply derivative_at_intro, - have (λ h, (c - c) / h) = (λ h, 0), from funext (λ h, by rewrite [sub_self, zero_div]), - rewrite this, - apply converges_to_at_constant - end + derivative_at_of_frechet_derivative_at + (@frechet_deriv_at_const ℝ ℝ _ _ _ c) + (funext (λ v, by rewrite zero_mul)) theorem deriv_at_id (x : ℝ) : derivative_at (λ t, t) 1 x := - begin - apply derivative_at_intro, - apply converges_to_at_real_intro, - intros ε Hε, - existsi 1, - split, - exact zero_lt_one, - intros x' Hx', - rewrite [add_sub_self, div_self (and.left Hx'), sub_self, abs_zero], - exact Hε - end + derivative_at_of_frechet_derivative_at + (@frechet_deriv_at_id ℝ ℝ _ _ _) + (funext (λ v, by rewrite one_mul)) + +theorem deriv_at_mul {f : ℝ → ℝ} {d x : ℝ} (H : derivative_at f d x) (c : ℝ) : + derivative_at (λ t, c * f t) (c * d) x := + derivative_at_of_frechet_derivative_at + (frechet_deriv_at_smul _ _ c H) + (funext (λ v, by rewrite mul.assoc)) end real diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index 03200a652..0fce9c2d2 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -150,17 +150,19 @@ namespace analysis theorem dist_eq_abs (x y : real) : dist x y = abs (x - y) := rfl -proposition converges_to_seq_real_intro {X : ℕ → ℝ} {y : ℝ} +namespace real +proposition approaches_at_infty_intro {X : ℕ → ℝ} {y : ℝ} (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε) : - (X ⟶ y [at ∞]) := approaches_at_infty_intro H + (X ⟶ y [at ∞]) := metric_space.approaches_at_infty_intro H -proposition converges_to_seq_real_elim {X : ℕ → ℝ} {y : ℝ} (H : X ⟶ y [at ∞]) : - ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε := approaches_at_infty_dest H +proposition approaches_at_infty_dest {X : ℕ → ℝ} {y : ℝ} (H : X ⟶ y [at ∞]) : + ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε := metric_space.approaches_at_infty_dest H -proposition converges_to_seq_real_intro' {X : ℕ → ℝ} {y : ℝ} +proposition approaches_at_infty_intro' {X : ℕ → ℝ} {y : ℝ} (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) ≤ ε) : (X ⟶ y [at ∞]) := approaches_at_infty_intro' H +end real open pnat subtype local postfix ⁻¹ := pnat.inv @@ -205,7 +207,7 @@ theorem converges_seq_of_cauchy {X : ℕ → ℝ} (H : cauchy X) : converges_seq 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 - (approaches_at_infty_intro + (real.approaches_at_infty_intro take ε : ℝ, suppose ε > 0, obtain (k' : ℕ) (Hn : 1 / succ k' < ε), from archimedean_small `ε > 0`, @@ -249,184 +251,271 @@ definition banach_space_real [trans_instance] : banach_space ℝ := complete := λ X H, analysis.complete ℝ H ⦄ +namespace real +open topology set +open normed_vector_space + +section +variable {f : ℝ → ℝ} + +theorem continuous_dest (H : continuous f) : + ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, + abs (x' - x) < δ → abs (f x' - f x) < ε := +normed_vector_space.continuous_dest H + +theorem continuous_intro + (H : ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, + abs (x' - x) < δ → abs (f x' - f x) < ε) : + continuous f := +normed_vector_space.continuous_intro H + +theorem continuous_at_dest {x : ℝ} (H : continuous_at f x) : + ∀ ε : ℝ, ε > 0 → (∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (x' - x) < δ → abs (f x' - f x) < ε) := +normed_vector_space.continuous_at_dest H + +theorem continuous_at_intro {x : ℝ} + (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, + abs (x' - x) < δ → abs (f x' - f x) < ε) : + continuous_at f x := +normed_vector_space.continuous_at_intro H + +theorem continuous_at_within_intro {x : ℝ} {s : set ℝ} + (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε) : + continuous_at_on f x s := +normed_vector_space.continuous_at_within_intro H + + +theorem continuous_at_on_dest {x : ℝ} {s : set ℝ} (Hfx : continuous_at_on f x s) : + ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε := +normed_vector_space.continuous_at_on_dest Hfx + +theorem continuous_on_intro {s : set ℝ} + (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε) : + continuous_on f s := +normed_vector_space.continuous_on_intro H + +theorem continuous_on_dest {s : set ℝ} (H : continuous_on f s) {x : ℝ} (Hxs : x ∈ s) : + ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε := +normed_vector_space.continuous_on_dest H Hxs + +end + +section approaches +open set.filter set topology + variables {X : Type} {F : filter X} {f : X → ℝ} {y : ℝ} + + proposition approaches_intro (H : ∀ ε, ε > 0 → eventually (λ x, abs ((f x) - y) < ε) F) : + (f ⟶ y) F := + normed_vector_space.approaches_intro H + + proposition approaches_dest (H : (f ⟶ y) F) {ε : ℝ} (εpos : ε > 0) : + eventually (λ x, abs ((f x) - y) < ε) F := + normed_vector_space.approaches_dest H εpos + + variables (F f y) + + proposition approaches_iff : ((f ⟶ y) F) ↔ (∀ ε, ε > 0 → eventually (λ x, abs ((f x) - y) < ε) F) := + iff.intro approaches_dest approaches_intro + +end approaches + +proposition approaches_at_infty_intro {f : ℕ → ℝ} {y : ℝ} + (H : ∀ ε, ε > 0 → ∃ N, ∀ n, n ≥ N → abs ((f n) - y) < ε) : + f ⟶ y [at ∞] := +normed_vector_space.approaches_at_infty_intro H + +proposition approaches_at_infty_dest {f : ℕ → ℝ} {y : ℝ} + (H : f ⟶ y [at ∞]) ⦃ε : ℝ⦄ (εpos : ε > 0) : + ∃ N, ∀ ⦃n⦄, n ≥ N → abs ((f n) - y) < ε := +normed_vector_space.approaches_at_infty_dest H εpos + +proposition approaches_at_infty_iff (f : ℕ → ℝ) (y : ℝ) : + f ⟶ y [at ∞] ↔ (∀ ε, ε > 0 → ∃ N, ∀ ⦃n⦄, n ≥ N → abs ((f n) - y) < ε) := +iff.intro approaches_at_infty_dest approaches_at_infty_intro + +section +variable {f : ℝ → ℝ} +proposition approaches_at_dest {y x : ℝ} + (H : f ⟶ y [at x]) ⦃ε : ℝ⦄ (εpos : ε > 0) : + ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε := +metric_space.approaches_at_dest H εpos + +proposition approaches_at_intro {y x : ℝ} + (H : ∀ ε, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε) : + f ⟶ y [at x] := +metric_space.approaches_at_intro H + +proposition approaches_at_iff (y x : ℝ) : f ⟶ y [at x] ↔ + (∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε) := +iff.intro approaches_at_dest approaches_at_intro + +end + +end real + /- limits under pointwise operations -/ section limit_operations -variables {X Y : ℕ → ℝ} +open set +variable {A : Type} +variables {X Y : A → ℝ} variables {x y : ℝ} +variable {F : filter A} -proposition mul_left_converges_to_seq (c : ℝ) (HX : X ⟶ x [at ∞]) : - (λ n, c * X n) ⟶ c * x [at ∞] := -smul_converges_to_seq c HX +proposition mul_left_approaches (c : ℝ) (HX : (X ⟶ x) F) : + ((λ n, c * X n) ⟶ c * x) F := +smul_approaches HX c -proposition mul_right_converges_to_seq (c : ℝ) (HX : X ⟶ x [at ∞]) : - (λ n, X n * c) ⟶ x * c [at ∞] := -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 +proposition mul_right_approaches (c : ℝ) (HX : (X ⟶ x) F) : + ((λ n, X n * c) ⟶ x * c) F := +have (λ n, X n * c) = (λ n, c * X n), from funext (λ n, !mul.comm), +by rewrite [this, mul.comm]; apply mul_left_approaches _ HX -theorem converges_to_seq_squeeze (HX : X ⟶ x [at ∞]) (HY : Y ⟶ x [at ∞]) {Z : ℕ → ℝ} (HZX : ∀ n, X n ≤ Z n) - (HZY : ∀ n, Z n ≤ Y n) : Z ⟶ x [at ∞] := +theorem approaches_squeeze (HX : (X ⟶ x) F) (HY : (Y ⟶ x) F) + {Z : A → ℝ} (HZX : filter.eventually (λ n, X n ≤ Z n) F) (HZY : filter.eventually (λ n, Z n ≤ Y n) F) : + (Z ⟶ x) F := begin - apply approaches_at_infty_intro, - intros ε Hε, - have Hε4 : ε / 4 > 0, from div_pos_of_pos_of_pos Hε four_pos, - cases approaches_at_infty_dest HX Hε4 with N1 HN1, - cases approaches_at_infty_dest HY Hε4 with N2 HN2, - existsi max N1 N2, - intro n Hn, - have HXY : abs (Y n - X n) < ε / 2, begin - apply lt_of_le_of_lt, - apply abs_sub_le _ x, - have Hε24 : ε / 2 = ε / 4 + ε / 4, from eq.symm !add_quarters, - rewrite Hε24, - apply add_lt_add, - apply HN2, - apply ge.trans Hn !le_max_right, - rewrite abs_sub, - apply HN1, - apply ge.trans Hn !le_max_left - end, - have HZX : abs (Z n - X n) < ε / 2, begin - have HZXnp : Z n - X n ≥ 0, from sub_nonneg_of_le !HZX, - have HXYnp : Y n - X n ≥ 0, from sub_nonneg_of_le (le.trans !HZX !HZY), - rewrite [abs_of_nonneg HZXnp, abs_of_nonneg HXYnp at HXY], - note Hgt := lt_add_of_sub_lt_right HXY, - have Hlt : Z n < ε / 2 + X n, from calc - Z n ≤ Y n : HZY - ... < ε / 2 + X n : Hgt, - apply sub_lt_right_of_lt_add Hlt - end, - have H : abs (Z n - x) < ε, begin - apply lt_of_le_of_lt, - apply abs_sub_le _ (X n), - apply lt.trans, - apply add_lt_add, - apply HZX, - apply HN1, - apply ge.trans Hn !le_max_left, - apply div_two_add_div_four_lt Hε - end, - exact H + apply real.approaches_intro, + intro ε Hε, + apply filter.eventually_mp, + rotate 1, + apply filter.eventually_and, + apply real.approaches_dest HX Hε, + apply real.approaches_dest HY Hε, + apply filter.eventually_mono, + apply filter.eventually_and HZX HZY, + intros x' Hlo Hdst, + change abs (Z x' - x) < ε, + cases em (x ≤ Z x') with HxleZ HxnleZ, -- annoying linear arith + {have Y x' - x = (Z x' - x) + (Y x' - Z x'), by rewrite -sub_eq_sub_add_sub, + have H : abs (Y x' - x) < ε, from and.right Hdst, + rewrite this at H, + have H'' : Y x' - Z x' ≥ 0, from sub_nonneg_of_le (and.right Hlo), + have H' : Z x' - x ≥ 0, from sub_nonneg_of_le HxleZ, + krewrite [abs_of_nonneg H', abs_of_nonneg (add_nonneg H' H'') at H], + apply lt_of_add_lt_of_nonneg_left H H''}, + {have X x' - x = (Z x' - x) + (X x' - Z x'), by rewrite -sub_eq_sub_add_sub, + have H : abs (X x' - x) < ε, from and.left Hdst, + rewrite this at H, + have H' : x - Z x' > 0, from sub_pos_of_lt (lt_of_not_ge HxnleZ), + have H'2 : Z x' - x < 0, + by rewrite [-neg_neg (Z x' - x)]; apply neg_neg_of_pos; rewrite [neg_sub]; apply H', + have H'' : X x' - Z x' ≤ 0, from sub_nonpos_of_le (and.left Hlo), + krewrite [abs_of_neg H'2, abs_of_neg (add_neg_of_neg_of_nonpos H'2 H'') at H, neg_add at H], + apply lt_of_add_lt_of_nonneg_left H, + apply neg_nonneg_of_nonpos H''} end -proposition converges_to_seq_of_abs_sub_converges_to_seq (Habs : (λ n, abs (X n - x)) ⟶ 0 [at ∞]) : - X ⟶ x [at ∞] := +proposition approaches_of_abs_sub_approaches {F} (Habs : ((λ n, abs (X n - x)) ⟶ 0) F) : + (X ⟶ x) F := begin - apply approaches_at_infty_intro, - intros ε Hε, - cases approaches_at_infty_dest Habs Hε with N HN, - existsi N, + apply real.approaches_intro, + intro ε Hε, + apply set.filter.eventually_mono, + apply real.approaches_dest Habs Hε, intro n Hn, - have Hn' : abs (abs (X n - x) - 0) < ε, from HN Hn, + have Hn' : abs (abs (X n - x) - 0) < ε, from Hn, rewrite [sub_zero at Hn', abs_abs at Hn'], exact Hn' end -proposition abs_sub_converges_to_seq_of_converges_to_seq (HX : X ⟶ x [at ∞]) : - (λ n, abs (X n - x)) ⟶ 0 [at ∞] := +proposition abs_sub_approaches_of_approaches {F} (HX : (X ⟶ x) F) : + ((λ n, abs (X n - x)) ⟶ 0) F := begin - apply approaches_at_infty_intro, + apply real.approaches_intro, intros ε Hε, - cases approaches_at_infty_dest HX Hε with N HN, - existsi N, + apply set.filter.eventually_mono, + apply real.approaches_dest HX Hε, intro n Hn, - have Hn' : abs (abs (X n - x) - 0) < ε, by rewrite [sub_zero, abs_abs]; apply HN Hn, + have Hn' : abs (abs (X n - x) - 0) < ε, by rewrite [sub_zero, abs_abs]; apply Hn, exact Hn' end -proposition mul_converges_to_seq (HX : X ⟶ x [at ∞]) (HY : Y ⟶ y [at ∞]) : - (λ n, X n * Y n) ⟶ x * y [at ∞] := - have Hbd : ∃ K : ℝ, ∀ n : ℕ, abs (X n) ≤ K, begin - cases bounded_of_converges_seq HX with K HK, - existsi K + abs x, - intro n, - note Habs := le.trans (abs_abs_sub_abs_le_abs_sub (X n) x) !HK, - apply le_add_of_sub_right_le, - apply le.trans, - apply le_abs_self, - assumption - end, - obtain K HK, from Hbd, - have Habsle : ∀ n, abs (X n * Y n - x * y) ≤ K * abs (Y n - y) + abs y * abs (X n - x), begin - intro, - have Heq : X n * Y n - x * y = (X n * Y n - X n * y) + (X n * y - x * y), by - rewrite [-sub_add_cancel (X n * Y n) (X n * y) at {1}, sub_eq_add_neg, *add.assoc], +proposition bounded_of_approaches_real {F} (HX : (X ⟶ x) F) : + ∃ K : ℝ, filter.eventually (λ n, abs (X n) ≤ K) F := + begin + cases bounded_of_converges HX with K HK, + existsi K + abs x, + apply filter.eventually_mono HK, + intro x' Hx', + note Hle := abs_sub_abs_le_abs_sub (X x') x, + apply le.trans, + apply le_add_of_sub_right_le, + apply Hle, + apply add_le_add_right, + apply Hx' + end + +proposition mul_approaches {F} (HX : (X ⟶ x) F) (HY : (Y ⟶ y) F) : + ((λ n, X n * Y n) ⟶ x * y) F := + obtain K HK, from bounded_of_approaches_real HX, + have Habsle : filter.eventually + (λ n, abs (X n * Y n - x * y) ≤ K * abs (Y n - y) + abs y * abs (X n - x)) F, begin + have Heq : ∀ n, X n * Y n - x * y = (X n * Y n - X n * y) + (X n * y - x * y), + by intro n; rewrite [-sub_add_cancel (X n * Y n) (X n * y) at {1}, sub_eq_add_neg, *add.assoc], + apply filter.eventually_mono HK, + intro x' Hx', apply le.trans, rewrite Heq, apply abs_add_le_abs_add_abs, apply add_le_add, rewrite [-mul_sub_left_distrib, abs_mul], apply mul_le_mul_of_nonneg_right, - apply HK, + apply Hx', apply abs_nonneg, rewrite [-mul_sub_right_distrib, abs_mul, mul.comm], apply le.refl end, - have Hdifflim : (λ n, abs (X n * Y n - x * y)) ⟶ 0 [at ∞], begin - apply converges_to_seq_squeeze, + have Hdifflim : ((λ n, abs (X n * Y n - x * y)) ⟶ 0) F, begin + apply approaches_squeeze, rotate 2, - intro, apply abs_nonneg, + intro, + apply filter.eventually_mono HK, + intro x' Hx', + apply abs_nonneg, apply Habsle, apply approaches_constant, rewrite -{0}zero_add, - apply add_converges_to_seq, + apply add_approaches, krewrite -(mul_zero K), - apply mul_left_converges_to_seq, - apply abs_sub_converges_to_seq_of_converges_to_seq, + apply mul_left_approaches, + apply abs_sub_approaches_of_approaches, exact HY, krewrite -(mul_zero (abs y)), - apply mul_left_converges_to_seq, - apply abs_sub_converges_to_seq_of_converges_to_seq, + apply mul_left_approaches, + apply abs_sub_approaches_of_approaches, exact HX end, - converges_to_seq_of_abs_sub_converges_to_seq Hdifflim + approaches_of_abs_sub_approaches Hdifflim - --- TODO: converges_to_seq_div, converges_to_seq_mul_left_iff, etc. - -proposition abs_converges_to_seq_zero (HX : X ⟶ 0 [at ∞]) : (λ n, abs (X n)) ⟶ 0 [at ∞] := -norm_converges_to_seq_zero HX - -proposition converges_to_seq_zero_of_abs_converges_to_seq_zero (HX : (λ n, abs (X n)) ⟶ 0 [at ∞]) : - X ⟶ 0 [at ∞] := -converges_to_seq_zero_of_norm_converges_to_seq_zero HX - -proposition abs_converges_to_seq_zero_iff (X : ℕ → ℝ) : - ((λ n, abs (X n)) ⟶ 0 [at ∞]) ↔ (X ⟶ 0 [at ∞]) := -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 - -/- properties of converges_to_at -/ - -section limit_operations_continuous -variables {f g h : ℝ → ℝ} -variables {a b x y : ℝ} - ---<<<<<<< HEAD -theorem mul_converges_to_at (Hf : f ⟶ a [at x]) (Hg : g ⟶ b [at x]) : (λ z, f z * g z) ⟶ a * b [at x] := -/-======= -theorem converges_to_at_real_intro (Hf : ∀ ⦃ε⦄, ε > 0 → - (∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ≠ x ∧ abs (x' - x) < δ → abs (f x' - y) < ε)) : - converges_to_at f y x := Hf - -theorem mul_converges_to_at (Hf : f ⟶ a at x) (Hg : g ⟶ b at x) : (λ z, f z * g z) ⟶ a * b at x := ->>>>>>> feat(library/analysis): basic properties about real derivatives-/ +proposition mul_approaches_zero_of_approaches_zero_of_approaches (HX : (X ⟶ 0) F) (HY : (Y ⟶ y) F) : + ((λ z, X z * Y z) ⟶ 0) F := begin - apply converges_to_at_of_all_conv_seqs, - intro X HX, - apply mul_converges_to_seq, - apply comp_approaches_at_infty Hf, - apply and.right (HX 0), - apply (set.filter.eventually_of_forall _ (λ n, and.left (HX n))), - apply comp_approaches_at_infty Hg, - apply and.right (HX 0), - apply (set.filter.eventually_of_forall _ (λ n, and.left (HX n))) + krewrite [-zero_mul y], + apply mul_approaches, + exact HX, exact HY end -end limit_operations_continuous +proposition mul_approaches_zero_of_approaches_of_approaches_zero (HX : (X ⟶ y) F) (HY : (Y ⟶ 0) F) : + ((λ z, X z * Y z) ⟶ 0) F := + begin + have H : (λ z, X z * Y z) = (λ z, Y z * X z), from funext (λ a, !mul.comm), + rewrite H, + exact mul_approaches_zero_of_approaches_zero_of_approaches HY HX + end + +proposition abs_approaches_zero_of_approaches_zero (HX : (X ⟶ 0) F) : ((λ n, abs (X n)) ⟶ 0) F := +norm_approaches_zero_of_approaches_zero HX + +proposition approaches_zero_of_abs_approaches_zero (HX : ((λ n, abs (X n)) ⟶ 0) F) : + (X ⟶ 0) F := +approaches_zero_of_norm_approaches_zero HX + +proposition abs_approaches_zero_iff : + ((λ n, abs (X n)) ⟶ 0) F ↔ (X ⟶ 0) F := +iff.intro approaches_zero_of_abs_approaches_zero abs_approaches_zero_of_approaches_zero +end limit_operations + /- monotone sequences -/ @@ -436,7 +525,7 @@ variable {X : ℕ → ℝ} proposition converges_to_seq_sup_of_nondecreasing (nondecX : nondecreasing X) {b : ℝ} (Hb : ∀ i, X i ≤ b) : X ⟶ sup (X ' univ) [at ∞] := -approaches_at_infty_intro +real.approaches_at_infty_intro (let sX := sup (X ' univ) in have Xle : ∀ i, X i ≤ sX, from take i, @@ -475,7 +564,7 @@ have H₃ : {x : ℝ | -x ∈ X ' univ} = {x : ℝ | x ∈ (λ n, -X n) ' univ}, ... = {x : ℝ | x ∈ (λ n, -X n) ' univ} : image_comp, have H₄ : ∀ i, - X i ≤ - b, from take i, neg_le_neg (Hb i), begin - apply iff.mp !neg_converges_to_seq_iff, + apply approaches_neg, -- need krewrite here krewrite [-sup_neg H₁ H₂, H₃, -nondecreasing_neg_iff at nonincX], apply converges_to_seq_sup_of_nondecreasing nonincX H₄ @@ -488,11 +577,11 @@ end monotone_sequences section xn open nat set -theorem pow_converges_to_seq_zero {x : ℝ} (H : abs x < 1) : +theorem pow_approaches_zero_at_infty {x : ℝ} (H : abs x < 1) : (λ n, x^n) ⟶ 0 [at ∞] := suffices H' : (λ n, (abs x)^n) ⟶ 0 [at ∞], from have (λ n, (abs x)^n) = (λ n, abs (x^n)), from funext (take n, eq.symm !abs_pow), - by rewrite this at H'; exact converges_to_seq_zero_of_abs_converges_to_seq_zero H', + by rewrite this at H'; exact approaches_zero_of_abs_approaches_zero H', let aX := (λ n, (abs x)^n), iaX := real.inf (aX ' univ), asX := (λ n, (abs x)^(succ n)) in @@ -506,7 +595,7 @@ have noninc_aX : nonincreasing aX, from have bdd_aX : ∀ i, 0 ≤ aX i, from take i, !pow_nonneg_of_nonneg !abs_nonneg, have aXconv : aX ⟶ iaX [at ∞], proof converges_to_seq_inf_of_nonincreasing noninc_aX bdd_aX qed, have asXconv : asX ⟶ iaX [at ∞], from tendsto_succ_at_infty aXconv, -have asXconv' : asX ⟶ (abs x) * iaX [at ∞], from mul_left_converges_to_seq (abs x) aXconv, +have asXconv' : asX ⟶ (abs x) * iaX [at ∞], from mul_left_approaches (abs x) aXconv, have iaX = (abs x) * iaX, from sorry, -- converges_to_seq_unique asXconv asXconv', have iaX = 0, from eq_zero_of_mul_eq_self_left (ne_of_lt H) (eq.symm this), show aX ⟶ 0 [at ∞], begin rewrite -this, exact aXconv end --from this ▸ aXconv @@ -515,36 +604,115 @@ end xn /- continuity on the reals -/ -section continuous -open topology +/-namespace real +open topology set +open normed_vector_space + +section variable {f : ℝ → ℝ} -theorem continuous_real_elim (H : continuous f) : +theorem continuous_dest (H : continuous f) : ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (x' - x) < δ → abs (f x' - f x) < ε := -take x, continuous_at_elim (forall_continuous_at_of_continuous H x) +normed_vector_space.continuous_dest H -theorem continuous_real_intro +theorem continuous_intro (H : ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (x' - x) < δ → abs (f x' - f x) < ε) : continuous f := -continuous_of_forall_continuous_at (take x, continuous_at_intro (H x)) +normed_vector_space.continuous_intro H -section -open set -variable {s : set ℝ} ---theorem continuous_on_real_elim (H : continuous_on f s) : --- ∀₀ x ∈ s, x = x := sorry +theorem continuous_at_dest {x : ℝ} (H : continuous_at f x) : + ∀ ε : ℝ, ε > 0 → (∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (x' - x) < δ → abs (f x' - f x) < ε) := +normed_vector_space.continuous_at_dest H + +theorem continuous_at_intro {x : ℝ} + (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, + abs (x' - x) < δ → abs (f x' - f x) < ε) : + continuous_at f x := +normed_vector_space.continuous_at_intro H + +theorem continuous_at_within_intro {x : ℝ} {s : set ℝ} + (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε) : + continuous_at_on f x s := +normed_vector_space.continuous_at_within_intro H + + +theorem continuous_at_on_dest {x : ℝ} {s : set ℝ} (Hfx : continuous_at_on f x s) : + ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε := +normed_vector_space.continuous_at_on_dest Hfx + +theorem continuous_on_intro {s : set ℝ} + (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε) : + continuous_on f s := +normed_vector_space.continuous_on_intro H + +theorem continuous_on_dest {s : set ℝ} (H : continuous_on f s) {x : ℝ} (Hxs : x ∈ s) : + ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε := +normed_vector_space.continuous_on_dest H Hxs end +section +variable {f : ℕ → ℝ} +proposition approaches_at_infty_intro {y : ℝ} + (H : ∀ ε, ε > 0 → ∃ N, ∀ n, n ≥ N → abs ((f n) - y) < ε) : + f ⟶ y [at ∞] := +normed_vector_space.approaches_at_infty_intro H + +proposition approaches_at_infty_dest {y : ℝ} + (H : f ⟶ y [at ∞]) ⦃ε : ℝ⦄ (εpos : ε > 0) : + ∃ N, ∀ ⦃n⦄, n ≥ N → abs ((f n) - y) < ε := +approaches_at_infty_dest H εpos + +proposition approaches_at_infty_iff (y : ℝ) : + f ⟶ y [at ∞] ↔ (∀ ε, ε > 0 → ∃ N, ∀ ⦃n⦄, n ≥ N → abs((f n) - y) < ε) := +iff.intro approaches_at_infty_dest approaches_at_infty_intro + +end + +section +variable {f : ℝ → ℝ} +proposition approaches_at_dest {y x : ℝ} + (H : f ⟶ y [at x]) ⦃ε : ℝ⦄ (εpos : ε > 0) : + ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε := +approaches_at_dest H εpos + +proposition approaches_at_intro {y x : ℝ} + (H : ∀ ε, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε) : + f ⟶ y [at x] := +approaches_at_intro H + +proposition approaches_at_iff (y x : ℝ) : f ⟶ y [at x] ↔ + (∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε) := +iff.intro approaches_at_dest approaches_at_intro + +/-proposition approaches_seq_real_intro {X : ℕ → ℝ} {y : ℝ} + (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε) : + (X ⟶ y [at ∞]) := metric_space.approaches_at_infty_intro H + +proposition approaches_seq_real_elim {X : ℕ → ℝ} {y : ℝ} (H : X ⟶ y [at ∞]) : + ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε := metric_space.approaches_at_infty_dest H + +proposition approaches_seq_real_intro' {X : ℕ → ℝ} {y : ℝ} + (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) ≤ ε) : + (X ⟶ y [at ∞]) := +approaches_at_infty_intro' H-/ + +end + +end real-/ + +section continuous +open topology +variable {f : ℝ → ℝ} 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, + let Hcont := real.continuous_dest Hf b Hb, cases Hcont with δ Hδ, existsi δ, split, @@ -559,7 +727,7 @@ theorem pos_on_nbhd_of_cts_of_pos {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), + let Hcont := real.continuous_dest Hf b (neg_pos_of_neg Hb), cases Hcont with δ Hδ, existsi δ, split, @@ -572,66 +740,17 @@ theorem neg_on_nbhd_of_cts_of_neg {b : ℝ} (Hb : f b < 0) : assumption end -theorem continuous_neg_of_continuous : continuous (λ x, - f x) := - begin - apply continuous_real_intro, - intros x ε Hε, - cases continuous_real_elim Hf x Hε with δ Hδ, - cases Hδ with Hδ₁ Hδ₂, - existsi δ, - split, - assumption, - intros x' Hx', - let HD := Hδ₂ x' Hx', - rewrite [-abs_neg, neg_neg_sub_neg], - exact HD - end - -theorem continuous_offset_of_continuous (a : ℝ) : - continuous (λ x, (f x) + a) := - begin - apply continuous_real_intro, - intros x ε Hε, - cases continuous_real_elim Hf x Hε with δ Hδ, - cases Hδ with Hδ₁ Hδ₂, - existsi δ, - split, - assumption, - intros x' Hx', - rewrite [add_sub_comm, sub_self, add_zero], - apply Hδ₂, - assumption - end - 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 continuous_at_of_tendsto_at, + apply mul_approaches, + all_goals apply tendsto_at_of_continuous_at, all_goals apply forall_continuous_at_of_continuous, apply Hf, apply Hcong end end continuous - --- this can be strengthened: Hle and Hge only need to hold around x -theorem converges_to_at_squeeze {M : Type} [Hm : metric_space M] {f g h : M → ℝ} {a : ℝ} {x : M} - (Hf : f ⟶ a at x) (Hh : h ⟶ a at x) (Hle : ∀ y : M, f y ≤ g y) - (Hge : ∀ y : M, g y ≤ h y) : g ⟶ a at x := - begin - apply converges_to_at_of_all_conv_seqs, - intro X HX, - apply converges_to_seq_squeeze, - apply all_conv_seqs_of_converges_to_at Hf, - apply HX, - apply all_conv_seqs_of_converges_to_at Hh, - apply HX, - intro, - apply Hle, - intro, - apply Hge - end diff --git a/library/theories/analysis/sqrt.lean b/library/theories/analysis/sqrt.lean index 94de569bf..3631344d9 100644 --- a/library/theories/analysis/sqrt.lean +++ b/library/theories/analysis/sqrt.lean @@ -34,7 +34,7 @@ private theorem lb_le_ub (x : ℝ) (H : x ≥ 0) : sqr_lb x ≤ sqr_ub x := apply zero_le_one end -private lemma sqr_cts : continuous (λ x : ℝ, x * x) := continuous_mul_of_continuous id_continuous id_continuous +private lemma sqr_cts : continuous (λ x : ℝ, x * x) := continuous_mul_of_continuous continuous_id continuous_id definition sqrt (x : ℝ) : ℝ := if H : x ≥ 0 then diff --git a/library/theories/move.lean b/library/theories/move.lean index 97861f16d..2e6fa1bf0 100644 --- a/library/theories/move.lean +++ b/library/theories/move.lean @@ -6,6 +6,7 @@ Temporary file; move in Lean3. -/ import data.set algebra.order_bigops import data.finset data.list.sort +import data.real -- move this to init.function @@ -20,6 +21,24 @@ theorem eq_of_inv_mul_eq_one {A : Type} {a b : A} [group A] (H : b⁻¹ * a = 1) have a⁻¹ * 1 = a⁻¹, by inst_simp, by inst_simp +theorem lt_neg_self_of_neg {A : Type} {a : A} [ordered_comm_group A] (Ha : a < 0) : a < -a := +calc + a < 0 : Ha + ... = -0 : by rewrite neg_zero + ... < -a : neg_lt_neg Ha + +theorem lt_of_add_lt_of_nonneg_left {A : Type} {a b c : A} [ordered_comm_group A] + (H : a + b < c) (Hb : b ≥ 0) : a < c := +calc + a < c - b : lt_sub_right_of_add_lt H + ... ≤ c : sub_le_self _ Hb + +theorem lt_of_add_lt_of_nonneg_right {A : Type} {a b c : A} [ordered_comm_group A] + (H : a + b < c) (Hb : a ≥ 0) : b < c := +calc + b < c - a : lt_sub_left_of_add_lt H + ... ≤ c : sub_le_self _ Hb + -- move to init.quotient namespace quot @@ -502,3 +521,18 @@ have succ (Max₀ s) ≤ Max₀ s, from le_Max₀ this, show false, from not_succ_le_self this end nat + + +-- move to real + +namespace real +theorem lt_of_abs_lt {a b : ℝ} (Ha : abs a < b) : a < b := +if Hnn : a ≥ 0 then + by rewrite [-abs_of_nonneg Hnn]; exact Ha +else + have Hlt : a < 0, from lt_of_not_ge Hnn, + have -a < b, by rewrite [-abs_of_neg Hlt]; exact Ha, + calc + a < -a : lt_neg_self_of_neg Hlt + ... < b : this +end real diff --git a/library/theories/topology/continuous.lean b/library/theories/topology/continuous.lean index a4029b89d..b49662137 100644 --- a/library/theories/topology/continuous.lean +++ b/library/theories/topology/continuous.lean @@ -5,7 +5,7 @@ Authors: Jacob Gross, Jeremy Avigad Continuous functions. -/ -import theories.topology.basic algebra.category ..move +import theories.topology.basic algebra.category ..move .limit open algebra eq.ops set topology function category sigma.ops namespace topology @@ -291,6 +291,41 @@ theorem forall_continuous_at_of_continuous {f : X → Y} (H : continuous f) : apply mem_univ end +section limit +open set +theorem tendsto_at_of_continuous_at {f : X → Y} {x : X} (H : continuous_at f x) : + (f ⟶ f x) (nhds x) := + begin + apply approaches_intro, + intro s HOs Hfxs, + cases H HOs Hfxs with u Hu, + apply eventually_nhds_intro, + exact and.left Hu, + exact and.left (and.right Hu), + intro x' Hx', + apply @mem_of_mem_preimage _ _ f, + apply and.right (and.right Hu), + exact Hx' + end + +theorem continuous_at_of_tendsto_at {f : X → Y} {x : X} (H : (f ⟶ f x) (nhds x)) : + continuous_at f x := + begin + intro s HOs Hfxs, + cases eventually_nhds_dest (approaches_elim H HOs Hfxs) with u Hu, + existsi u, + split, + exact and.left Hu, + split, + exact and.left (and.right Hu), + intro x Hx, + apply mem_preimage, + apply and.right (and.right Hu), + apply Hx + end + +end limit + /- The Category TOP -/ section TOP diff --git a/library/theories/topology/limit.lean b/library/theories/topology/limit.lean index 690d23f1e..72e05c5ec 100644 --- a/library/theories/topology/limit.lean +++ b/library/theories/topology/limit.lean @@ -703,6 +703,16 @@ section approaches have eventually (λ x, f x ∈ univ ∧ f x ≠ y) F₁, from eventually_congr (take x, by rewrite [mem_univ_iff, true_and]) Hf₂, tendsto_comp_of_approaches_of_tendsto_at_within Hf₁ this Hg + + proposition approaches_constant : ((λ x, y) ⟶ y) F := + begin + apply approaches_intro, + intro s Hs Hys, + have H : (λ x : X, y ∈ s) = (λ x : X, true), from funext (λ x, by rewrite classical.eq_true; exact Hys), + rewrite H, + apply eventually_true + end + end approaches /-