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

fix(theories/analysis): rename derivative theorems

Browse source
This commit is contained in:
Rob Lewis 2016-05-25 17:57:33 -04:00 committed by Leonardo de Moura
parent 6b71b75d6f
commit 371638a628
4 changed files with 56 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -127,7 +127,7 @@ theorem op_norm_pos : op_norm f > 0 := is_bdd_linear_map.op_norm_pos _ _ f
theorem op_norm_bound (v : V) : ∥f v∥ ≤ (op_norm f) * ∥v∥ := is_bdd_linear_map.op_norm_bound _ _ f v
theorem bounded_linear_operator_continuous : continuous f :=
theorem bdd_linear_map_continuous : continuous f :=
begin
apply continuous_of_forall_continuous_at,
intro x,
@ -156,10 +156,10 @@ variables {V W : Type}
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) :=
definition has_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]
lemma diff_quot_cts {f A : V → W} [HA : is_bdd_linear_map A] {y : V} (Hf : is_frechet_deriv_at f A y) :
lemma diff_quot_cts {f A : V → W} [HA : is_bdd_linear_map A] {y : V} (Hf : has_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,
@ -189,19 +189,19 @@ theorem is_bdd_linear_map_of_eq {A B : V → W} [HA : is_bdd_linear_map A] (HAB
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 :=
(Hfd : has_frechet_deriv_at f A x) {B : V → W} (HAB : A = B) :
@has_frechet_deriv_at _ _ _ _ f B (is_bdd_linear_map_of_eq HAB) x :=
begin
unfold is_frechet_deriv_at,
unfold has_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}
theorem has_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 :=
has_frechet_deriv_at f A x :=
begin
apply normed_vector_space.approaches_at_intro,
intros ε Hε,
@ -223,7 +223,7 @@ theorem is_frechet_deriv_at_intro {f A : V → W} [is_bdd_linear_map A] {x : V}
end
end
theorem is_frechet_deriv_at_elim {f A : V → W} [is_bdd_linear_map A] {x : V} (H : is_frechet_deriv_at f A x) :
theorem has_frechet_deriv_at_elim {f A : V → W} [is_bdd_linear_map A] {x : V} (H : has_frechet_deriv_at f A x) :
∀ ⦃ε : ℝ⦄, ε > 0 →
(∃ δ : ℝ, δ > 0 ∧ ∀ ⦃x' : V⦄, x' ≠ 0 ∧ ∥x'∥ < δ → ∥f (x + x') - f x - A x'∥ / ∥x'∥ < ε) :=
begin
@ -242,7 +242,7 @@ theorem is_frechet_deriv_at_elim {f A : V → W} [is_bdd_linear_map A] {x : V} (
end
structure frechet_diffable_at [class] (f : V → W) (x : V) :=
(A : V → W) [HA : is_bdd_linear_map A] (is_fr_der : is_frechet_deriv_at f A x)
(A : V → W) [HA : is_bdd_linear_map A] (is_fr_der : has_frechet_deriv_at f A x)
variables f g : V → W
variable x : V
@ -258,7 +258,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 has_frechet_deriv_at_const (w : W) : has_frechet_deriv_at (λ v : V, w) (λ v : V, 0) x :=
begin
apply normed_vector_space.approaches_at_intro,
intros ε Hε,
@ -271,7 +271,7 @@ theorem frechet_deriv_at_const (w : W) : is_frechet_deriv_at (λ v : V, w) (λ v
assumption
end
theorem frechet_deriv_at_id : is_frechet_deriv_at (λ v : V, v) (λ v : V, v) x :=
theorem has_frechet_deriv_at_id : has_frechet_deriv_at (λ v : V, v) (λ v : V, v) x :=
begin
apply normed_vector_space.approaches_at_intro,
intros ε Hε,
@ -284,8 +284,8 @@ theorem frechet_deriv_at_id : is_frechet_deriv_at (λ v : V, v) (λ v : V, v) x
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 :=
theorem has_frechet_deriv_at_smul (c : ℝ) {A : V → W} [is_bdd_linear_map A]
(Hf : has_frechet_deriv_at f A x) : has_frechet_deriv_at (λ y, c • f y) (λ y, c • A y) x :=
begin
eapply @decidable.cases_on (abs c = 0),
exact _,
@ -329,12 +329,12 @@ theorem frechet_deriv_at_smul (c : ℝ) {A : V → W} [is_bdd_linear_map A]
end
end
theorem frechet_deriv_at_neg {A : V → W} [is_bdd_linear_map A]
(Hf : is_frechet_deriv_at f A x) : is_frechet_deriv_at (λ y, - f y) (λ y, - A y) x :=
theorem has_frechet_deriv_at_neg {A : V → W} [is_bdd_linear_map A]
(Hf : has_frechet_deriv_at f A x) : has_frechet_deriv_at (λ y, - f y) (λ y, - A y) x :=
begin
apply is_frechet_deriv_at_intro,
apply has_frechet_deriv_at_intro,
intros ε Hε,
cases is_frechet_deriv_at_elim Hf Hε with δ Hδ,
cases has_frechet_deriv_at_elim Hf Hε with δ Hδ,
existsi δ,
split,
exact and.left Hδ,
@ -345,9 +345,9 @@ theorem frechet_deriv_at_neg {A : V → W} [is_bdd_linear_map A]
assumption
end
theorem frechet_deriv_at_add (A B : V → W) [is_bdd_linear_map A] [is_bdd_linear_map B]
(Hf : is_frechet_deriv_at f A x) (Hg : is_frechet_deriv_at g B x) :
is_frechet_deriv_at (λ y, f y + g y) (λ y, A y + B y) x :=
theorem has_frechet_deriv_at_add (A B : V → W) [is_bdd_linear_map A] [is_bdd_linear_map B]
(Hf : has_frechet_deriv_at f A x) (Hg : has_frechet_deriv_at g B x) :
has_frechet_deriv_at (λ y, f y + g y) (λ y, A y + B y) x :=
begin
have Hle : ∀ h, ∥f (x + h) + g (x + h) - (f x + g x) - (A h + B h)∥ / ∥h∥ ≤
∥f (x + h) - f x - A h∥ / ∥h∥ + ∥g (x + h) - g x - B h∥ / ∥h∥, begin
@ -435,8 +435,8 @@ 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 :=
theorem continuous_at_of_has_frechet_deriv_at {A : V → W} [is_bdd_linear_map A]
(H : has_frechet_deriv_at f A x) : continuous_at f x :=
begin
apply @continuous_at_of_diffable_at,
existsi A,
@ -454,7 +454,7 @@ lemma div_add_eq_add_mul_div {A : Type} [field A] (a b c : A) (Hb : b ≠ 0) : (
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}
private 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,
@ -471,12 +471,12 @@ 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 :=
theorem has_frechet_deriv_at_comp (Hg : has_frechet_deriv_at g B x) (Hf : has_frechet_deriv_at f A (g x)) :
@has_frechet_deriv_at _ _ _ _ (λ y, f (g y)) (λ y, A (B y)) !is_bdd_linear_map_comp x :=
begin
unfold is_frechet_deriv_at,
note Hf' := is_frechet_deriv_at_elim Hf,
note Hg' := is_frechet_deriv_at_elim Hg,
unfold has_frechet_deriv_at,
note Hf' := has_frechet_deriv_at_elim Hf,
note Hg' := has_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
@ -522,6 +522,7 @@ theorem frechet_derivative_at_comp (Hg : is_frechet_deriv_at g B x) (Hf : is_fre
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],
clear [Hf, Hg, Hf', Hg', Hneq],
simp} --(.5 seconds)
end,
apply approaches_squeeze, -- again, by squeezing
@ -553,7 +554,7 @@ theorem frechet_derivative_at_comp (Hg : is_frechet_deriv_at g B x) (Hf : is_fre
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δ,
cases normed_vector_space.continuous_at_dest (continuous_at_of_has_frechet_deriv_at g x Hg) _ Hε with δ Hδ,
existsi δ,
split,
exact and.left Hδ,

38
library/theories/analysis/real_deriv.lean
View file

@ -11,18 +11,14 @@ 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
definition has_deriv_at (f : ℝ → ℝ) (d x : ℝ) := has_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 :=
theorem has_deriv_at_intro (f : ℝ → ℝ) (d x : ℝ) (H : (λ h, (f (x + h) - f x) / h) ⟶ d [at 0]) :
has_deriv_at f d x :=
begin
apply is_frechet_deriv_at_intro,
apply has_frechet_deriv_at_intro,
intros ε Hε,
cases approaches_at_dest H Hε with δ Hδ,
existsi δ,
@ -36,25 +32,25 @@ theorem derivative_at_intro (f : ℝ → ℝ) (d x : ℝ) (H : (λ h, (f (x + 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 :=
theorem has_deriv_at_of_has_frechet_deriv_at {f g : ℝ → ℝ} [is_bdd_linear_map g] {d x : ℝ}
(H : has_frechet_deriv_at f g x) (Hg : g = λ x, d * x) :
has_deriv_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 :=
derivative_at_of_frechet_derivative_at
(@frechet_deriv_at_const ℝ ℝ _ _ _ c)
theorem has_deriv_at_const (c x : ℝ) : has_deriv_at (λ t, c) 0 x :=
has_deriv_at_of_has_frechet_deriv_at
(@has_frechet_deriv_at_const ℝ ℝ _ _ _ c)
(funext (λ v, by rewrite zero_mul))
theorem deriv_at_id (x : ℝ) : derivative_at (λ t, t) 1 x :=
derivative_at_of_frechet_derivative_at
(@frechet_deriv_at_id ℝ ℝ _ _ _)
theorem has_deriv_at_id (x : ℝ) : has_deriv_at (λ t, t) 1 x :=
has_deriv_at_of_has_frechet_deriv_at
(@has_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)
theorem has_deriv_at_mul {f : ℝ → ℝ} {d x : ℝ} (H : has_deriv_at f d x) (c : ℝ) :
has_deriv_at (λ t, c * f t) (c * d) x :=
has_deriv_at_of_has_frechet_deriv_at
(has_frechet_deriv_at_smul _ _ c H)
(funext (λ v, by rewrite mul.assoc))
end real

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

@ -146,10 +146,6 @@ end real
/- the reals form a complete metric space -/
namespace analysis
theorem dist_eq_abs (x y : real) : dist x y = abs (x - y) := rfl
namespace real
proposition approaches_at_infty_intro {X : ℕ → ℝ} {y : ℝ}
(H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε) :
@ -164,6 +160,10 @@ proposition approaches_at_infty_intro' {X : ℕ → ℝ} {y : ℝ}
approaches_at_infty_intro' H
end real
namespace analysis
theorem dist_eq_abs (x y : real) : dist x y = abs (x - y) := rfl
open pnat subtype
local postfix ⁻¹ := pnat.inv
@ -319,20 +319,6 @@ open set.filter set topology
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 : ℝ}

4
library/theories/move.lean
View file

@ -45,6 +45,10 @@ calc
a = a / c * c : !div_mul_cancel (ne.symm (ne_of_lt Hc))
... < b * c : mul_lt_mul_of_pos_right H Hc
theorem add_sub_self {A : Type} [add_comm_group A] (a b : A) : a + b - a = b :=
by rewrite [add_sub_assoc, add.comm, sub_add_cancel]
-- move to init.quotient
namespace quot