feat(library/analysis): basic properties about real derivatives
This commit is contained in:
parent
92531fba16
commit
670ee10b27
4 changed files with 132 additions and 29 deletions
|
@ -17,7 +17,7 @@ structure is_bdd_linear_map [class] {V W : Type} [normed_vector_space V] [normed
|
|||
extends is_module_hom ℝ f :=
|
||||
(op_norm : ℝ) (op_norm_pos : op_norm > 0) (op_norm_bound : ∀ v : V, ∥f v∥ ≤ op_norm * ∥v∥)
|
||||
|
||||
theorem is_bdd_linear_map_id (V : Type) [normed_vector_space V] : is_bdd_linear_map (λ x : V, x) :=
|
||||
theorem is_bdd_linear_map_id [instance] (V : Type) [normed_vector_space V] : is_bdd_linear_map (λ x : V, x) :=
|
||||
begin
|
||||
fapply is_bdd_linear_map.mk,
|
||||
repeat (intros; reflexivity),
|
||||
|
@ -218,7 +218,7 @@ 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 :=
|
||||
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 :=
|
||||
theorem frechet_deriv_at_const (w : W) : is_frechet_deriv_at (λ v : V, w) (λ v : V, 0) x :=
|
||||
begin
|
||||
intros ε Hε,
|
||||
existsi 1,
|
||||
|
|
|
@ -347,6 +347,7 @@ 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 ∞],
|
||||
|
@ -362,6 +363,66 @@ 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 converges_to_seq_offset_iff (X : ℕ → M) (y : M) (k : ℕ) :
|
||||
((λ n, X (n + k)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
|
||||
iff.intro converges_to_seq_of_converges_to_seq_offset !converges_to_seq_offset
|
||||
|
||||
proposition converges_to_seq_offset_left_iff (X : ℕ → M) (y : M) (k : ℕ) :
|
||||
((λ n, X (k + n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
|
||||
iff.intro converges_to_seq_of_converges_to_seq_offset_left !converges_to_seq_offset_left
|
||||
|
||||
proposition converges_to_seq_offset_succ_iff (X : ℕ → M) (y : M) :
|
||||
((λ n, X (succ n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
|
||||
iff.intro converges_to_seq_of_converges_to_seq_offset_succ !converges_to_seq_offset_succ
|
||||
|
||||
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 -/
|
||||
|
||||
|
@ -552,32 +613,6 @@ 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
|
||||
theorem continuous_at_intro {f : M → N} {x : M}
|
||||
(H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε) :
|
||||
|
@ -726,7 +761,7 @@ approaches_at_intro
|
|||
--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) :
|
||||
(Hf : continuous f) :
|
||||
converges_seq (λ n, f (X n)) :=
|
||||
begin
|
||||
cases HX with xlim Hxlim,
|
||||
|
|
60
library/theories/analysis/real_deriv.lean
Normal file
60
library/theories/analysis/real_deriv.lean
Normal file
|
@ -0,0 +1,60 @@
|
|||
/-
|
||||
Copyright (c) 2016 Robert Y. Lewis. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Robert Y. Lewis
|
||||
|
||||
Derivatives on ℝ
|
||||
-/
|
||||
import .bounded_linear_operator
|
||||
open real nat classical topology analysis
|
||||
noncomputable theory
|
||||
|
||||
namespace real
|
||||
|
||||
-- move this to group
|
||||
theorem add_sub_self (a b : ℝ) : a + b - a = b :=
|
||||
by rewrite [add_sub_assoc, add.comm, sub_add_cancel]
|
||||
|
||||
-- make instance of const mul bdd lin op?
|
||||
|
||||
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) :
|
||||
derivative_at f d x :=
|
||||
begin
|
||||
apply is_frechet_deriv_at_intro,
|
||||
intros ε Hε,
|
||||
cases 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,
|
||||
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 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
|
||||
|
||||
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
|
||||
|
||||
end real
|
|
@ -405,7 +405,15 @@ 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-/
|
||||
begin
|
||||
apply converges_to_at_of_all_conv_seqs,
|
||||
intro X HX,
|
||||
|
|
Loading…
Reference in a new issue