feat(library/theories/analysis): prove intermediate value theorem
This commit is contained in:
Rob Lewis
Leonardo de Moura
parent
f5dcb1e0a9
commit
ea3915f279
2 changed files with 303 additions and 2 deletions
|
|
@ -136,6 +136,48 @@ 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
|
||||
|
||||
definition continuous_at (f : M → N) (x : M) := converges_to_at f (f x) x
|
||||
|
||||
definition continuous (f : M → N) := ∀ x, continuous_at f x
|
||||
|
||||
theorem continuous_at_spec {f : M → N} {x : M} (Hf : continuous_at f x) :
|
||||
∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ x', dist x x' < δ → dist (f x') (f x) < ε :=
|
||||
take ε, suppose ε > 0,
|
||||
obtain δ Hδ, from Hf this,
|
||||
exists.intro δ (and.intro
|
||||
(and.left Hδ)
|
||||
(take x', suppose dist x x' < δ,
|
||||
if Heq : x = x' then
|
||||
by rewrite [Heq, dist_self]; assumption
|
||||
else
|
||||
(suffices dist x x' < δ, from and.right Hδ _ (and.intro Heq this),
|
||||
this)))
|
||||
|
||||
definition image_seq (X : ℕ → M) (f : M → N) : ℕ → N := λ n, f (X n)
|
||||
|
||||
theorem image_seq_converges_of_converges [instance] (X : ℕ → M) [HX : converges_seq X] {f : M → N} (Hf : continuous f) :
|
||||
converges_seq (image_seq X f) :=
|
||||
begin
|
||||
cases HX with xlim Hxlim,
|
||||
existsi f xlim,
|
||||
rewrite ↑converges_to_seq at *,
|
||||
intros ε Hε,
|
||||
let Hcont := Hf xlim Hε,
|
||||
cases Hcont with δ Hδ,
|
||||
cases Hxlim (and.left Hδ) with B HB,
|
||||
existsi B,
|
||||
intro n Hn,
|
||||
cases em (xlim = X n),
|
||||
rewrite [↑image_seq, a, dist_self],
|
||||
assumption,
|
||||
rewrite ↑image_seq,
|
||||
apply and.right Hδ,
|
||||
split,
|
||||
exact a,
|
||||
rewrite dist_comm,
|
||||
apply HB Hn
|
||||
end
|
||||
|
||||
end metric_space_M_N
|
||||
|
||||
end metric_space
|
||||
|
|
|
|||
|
|
@ -129,8 +129,6 @@ exists.intro l
|
|||
have abs (X n - l) ≤ real.of_rat k⁻¹, from conv k n' Hn,
|
||||
show abs (X n - l) < ε, from lt_of_le_of_lt this Hk))
|
||||
|
||||
/- sup and inf -/
|
||||
|
||||
open set
|
||||
|
||||
private definition exists_is_sup {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b)) :
|
||||
|
|
@ -189,6 +187,267 @@ by+ rewrite [↑inf, dif_pos H]; exact and.right (inf_aux_spec H) b Hb
|
|||
|
||||
end
|
||||
|
||||
section inter_val
|
||||
open set
|
||||
|
||||
-- this definition should be inherited from metric_space once a migrate is done.
|
||||
definition continuous (f : ℝ → ℝ) :=
|
||||
∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (x - x') < δ → abs (f x - f x') < ε
|
||||
|
||||
private definition inter_sup (a b : ℝ) (f : ℝ → ℝ) := sup {x | x < b ∧ f x < 0}
|
||||
|
||||
private theorem add_midpoint {a b : ℝ} (H : a < b) : a + (b - a) / 2 < b :=
|
||||
begin
|
||||
rewrite [-div_sub_div_same, sub_eq_add_neg, {b / 2 + _}add.comm, -add.assoc, -sub_eq_add_neg],
|
||||
apply add_lt_of_lt_sub_right,
|
||||
krewrite *sub_self_div_two,
|
||||
apply div_lt_div_of_lt_of_pos H two_pos
|
||||
end
|
||||
|
||||
section
|
||||
parameters {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) (Ha : f a < 0) (Hb : f b > 0)
|
||||
include Hf Ha Hb Hab
|
||||
|
||||
private theorem Hinh : ∃ x, x ∈ {x | x < b ∧ f x < 0} := exists.intro a (and.intro Hab Ha)
|
||||
|
||||
private theorem Hmem : ∀ x, x ∈ {x | x < b ∧ f x < 0} → x ≤ b := λ x Hx, le_of_lt (and.left Hx)
|
||||
|
||||
private theorem Hsupleb : inter_sup a b f ≤ b := sup_le (Hinh) Hmem
|
||||
|
||||
private theorem sup_fn_interval_aux1 : ∀ ε : ℝ, ε > 0 → f (inter_sup a b f) ≥ 0 - ε :=
|
||||
(take ε, suppose ε > 0,
|
||||
have ¬ f (inter_sup a b f) < 0 - ε, from
|
||||
(suppose f (inter_sup a b f) < 0 - ε,
|
||||
have ∃ δ, δ > (0 : ℝ) ∧ inter_sup a b f + δ < b ∧ f (inter_sup a b f + δ) < 0, begin
|
||||
let Hcont := Hf (inter_sup a b f)
|
||||
(show -f (inter_sup a b f) > 0, begin
|
||||
rewrite zero_sub at this,
|
||||
apply lt.trans,
|
||||
exact `ε > 0`,
|
||||
apply lt_neg_of_lt_neg,
|
||||
exact this
|
||||
end),
|
||||
cases Hcont with δ Hδ,
|
||||
cases em (inter_sup a b f + δ / 2 < b),
|
||||
existsi δ / 2,
|
||||
split,
|
||||
apply div_pos_of_pos_of_pos (and.left Hδ) two_pos,
|
||||
split,
|
||||
assumption,
|
||||
have Habs : abs (inter_sup a b f - (inter_sup a b f + δ / 2)) < δ, begin
|
||||
krewrite [sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg,
|
||||
abs_of_pos (div_pos_of_pos_of_pos (and.left Hδ) two_pos)],
|
||||
apply div_two_lt_of_pos (and.left Hδ)
|
||||
end,
|
||||
let Hlt := and.right Hδ _ Habs,
|
||||
let Hlt' := sub_lt_of_abs_sub_lt_left Hlt,
|
||||
let Hlt'' := lt_add_of_sub_lt_right _ _ _ Hlt',
|
||||
rewrite [-sub_eq_add_neg at Hlt'', sub_self at Hlt''],
|
||||
assumption,
|
||||
let Hble := le_of_not_gt a_1,
|
||||
have Habs : abs (inter_sup a b f - b) < δ, begin
|
||||
apply abs_lt_of_lt_of_neg_lt,
|
||||
apply sub_lt_left_of_lt_add,
|
||||
apply lt_of_le_of_lt,
|
||||
apply Hsupleb,
|
||||
apply lt_add_of_pos_right (and.left Hδ),
|
||||
rewrite neg_sub,
|
||||
apply sub_lt_left_of_lt_add,
|
||||
apply lt_of_le_of_lt,
|
||||
apply Hble,
|
||||
apply add_lt_add_left,
|
||||
apply div_two_lt_of_pos (and.left Hδ)
|
||||
end,
|
||||
let Hlt := and.right Hδ _ Habs,
|
||||
let Hlt' := sub_lt_of_abs_sub_lt_left Hlt,
|
||||
let Hlt'' := lt_add_of_sub_lt_right _ _ _ Hlt',
|
||||
rewrite [-sub_eq_add_neg at Hlt'', sub_self at Hlt''],
|
||||
apply absurd Hb (not_lt_of_ge (le_of_lt Hlt''))
|
||||
end,
|
||||
obtain δ Hδ, from this,
|
||||
have inter_sup a b f + δ ∈ {x | x < b ∧ f x < 0},
|
||||
from and.intro (and.left (and.right Hδ)) (and.right (and.right Hδ)),
|
||||
have Hle : ¬ inter_sup a b f < inter_sup a b f + δ,
|
||||
from not_lt_of_ge (le_sup this Hmem),
|
||||
show false, from Hle (lt_add_of_pos_right (and.left Hδ))),
|
||||
le_of_not_gt this)
|
||||
|
||||
private theorem sup_fn_interval_aux2 : ∀ ε : ℝ, ε > 0 → f (inter_sup a b f) < ε :=
|
||||
(take ε, suppose ε > 0,
|
||||
have ¬ f (inter_sup a b f) ≥ ε, from
|
||||
(suppose f (inter_sup a b f) ≥ ε,
|
||||
have ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (inter_sup a b f - x') < δ → f x' > 0, begin
|
||||
let Hcont := Hf (inter_sup a b f) (show f (inter_sup a b f) > 0, from gt_of_ge_of_gt this `ε > 0`),
|
||||
cases Hcont with δ Hδ,
|
||||
existsi δ,
|
||||
split,
|
||||
exact and.left Hδ,
|
||||
intro x Hx,
|
||||
let Hlt := and.right Hδ _ Hx,
|
||||
let Hlt' := sub_lt_of_abs_sub_lt_right Hlt,
|
||||
rewrite sub_self at Hlt',
|
||||
exact Hlt'
|
||||
end,
|
||||
obtain δ Hδ, from this,
|
||||
have ∀ x, x ∈ {x | x < b ∧ f x < 0} → x ≤ inter_sup a b f - δ / 2, from
|
||||
(take x, suppose x ∈ {x | x < b ∧ f x < 0},
|
||||
have x ≤ inter_sup a b f, from le_sup this Hmem,
|
||||
have ¬ x > inter_sup a b f - δ / 2, from
|
||||
(assume Hngt,
|
||||
have abs (inter_sup a b f - x) < δ, begin
|
||||
apply abs_lt_of_lt_of_neg_lt,
|
||||
apply sub_lt_of_sub_lt,
|
||||
apply gt.trans,
|
||||
exact Hngt,
|
||||
apply sub_lt_sub_left,
|
||||
exact div_two_lt_of_pos (and.left Hδ),
|
||||
rewrite neg_sub,
|
||||
apply lt_of_le_of_lt,
|
||||
rotate 1,
|
||||
apply and.left Hδ,
|
||||
apply sub_nonpos_of_le,
|
||||
apply le_sup,
|
||||
exact this,
|
||||
exact Hmem
|
||||
end,
|
||||
have f x > 0, from and.right Hδ _ this,
|
||||
show false, from (not_lt_of_gt this) (and.right `x ∈ {x | x < b ∧ f x < 0}`)),
|
||||
le_of_not_gt this),
|
||||
have Hle : inter_sup a b f ≤ inter_sup a b f - δ / 2, from sup_le Hinh this,
|
||||
show false, from not_le_of_gt (sub_lt_of_pos _ (div_pos_of_pos_of_pos (and.left Hδ) (two_pos))) Hle),
|
||||
lt_of_not_ge this)
|
||||
|
||||
private theorem sup_fn_interval : f (inter_sup a b f) = 0 :=
|
||||
have Hnlt : f (inter_sup a b f) ≥ 0, from ge_of_forall_ge_sub sup_fn_interval_aux1,
|
||||
eq_zero_of_nonneg_of_forall_lt Hnlt sup_fn_interval_aux2
|
||||
|
||||
private theorem intermediate_value_incr_aux1 : ∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (b - y) < δ → f y > 0 :=
|
||||
begin
|
||||
let Hcont := Hf b Hb,
|
||||
cases Hcont with δ Hδ,
|
||||
existsi δ,
|
||||
split,
|
||||
exact and.left Hδ,
|
||||
intro y Hy,
|
||||
let Hy' := and.right Hδ _ Hy,
|
||||
let Hlt := sub_lt_of_abs_sub_lt_right Hy',
|
||||
rewrite sub_self at Hlt,
|
||||
assumption
|
||||
end
|
||||
|
||||
private theorem intermediate_value_incr_aux2 : ∃ δ : ℝ, δ > 0 ∧ a + δ < b ∧ f (a + δ) < 0 :=
|
||||
begin
|
||||
have Hnfa : - (f a) > 0, from neg_pos_of_neg Ha,
|
||||
let Hcont := Hf a Hnfa,
|
||||
cases Hcont with δ Hδ,
|
||||
cases em (a + δ < b) with Haδ Haδ,
|
||||
existsi δ / 2,
|
||||
split,
|
||||
exact div_pos_of_pos_of_pos (and.left Hδ) two_pos,
|
||||
split,
|
||||
apply lt.trans,
|
||||
apply add_lt_add_left,
|
||||
exact div_two_lt_of_pos (and.left Hδ),
|
||||
assumption,
|
||||
have Habs : abs (a - (a + δ / 2)) < δ, begin
|
||||
krewrite [sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg,
|
||||
abs_of_pos (div_pos_of_pos_of_pos (and.left Hδ) two_pos)],
|
||||
exact div_two_lt_of_pos (and.left Hδ)
|
||||
end,
|
||||
let Hlt := and.right Hδ _ Habs,
|
||||
let Hlt' := sub_lt_of_abs_sub_lt_left Hlt,
|
||||
let Hlt'' := lt_add_of_sub_lt_right _ _ _ Hlt',
|
||||
rewrite [-sub_eq_add_neg at Hlt'', sub_self at Hlt''],
|
||||
assumption,
|
||||
existsi (b - a) / 2,
|
||||
split,
|
||||
apply div_pos_of_pos_of_pos,
|
||||
exact sub_pos_of_lt _ _ Hab,
|
||||
exact two_pos,
|
||||
split,
|
||||
apply add_midpoint Hab,
|
||||
have Habs : abs (a - (a + (b - a) / 2)) < δ, begin
|
||||
krewrite [sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg,
|
||||
abs_of_pos (div_pos_of_pos_of_pos (sub_pos_of_lt _ _ Hab) two_pos)],
|
||||
apply lt_of_lt_of_le,
|
||||
apply div_two_lt_of_pos (sub_pos_of_lt _ _ Hab),
|
||||
apply sub_left_le_of_le_add,
|
||||
apply le_of_not_gt Haδ
|
||||
end,
|
||||
let Hlt := and.right Hδ _ Habs,
|
||||
let Hlt' := sub_lt_of_abs_sub_lt_left Hlt,
|
||||
let Hlt'' := lt_add_of_sub_lt_right _ _ _ Hlt',
|
||||
rewrite [-sub_eq_add_neg at Hlt'', sub_self at Hlt''],
|
||||
assumption
|
||||
end
|
||||
|
||||
theorem intermediate_value_incr : ∃ c, a < c ∧ c < b ∧ f c = 0 :=
|
||||
begin
|
||||
existsi inter_sup a b f,
|
||||
split,
|
||||
cases intermediate_value_incr_aux2 with δ Hδ,
|
||||
apply lt_of_lt_of_le,
|
||||
apply lt_add_of_pos_right,
|
||||
exact and.left Hδ,
|
||||
apply le_sup,
|
||||
exact and.right Hδ,
|
||||
intro x Hx,
|
||||
apply le_of_lt,
|
||||
exact and.left Hx,
|
||||
split,
|
||||
cases intermediate_value_incr_aux1 with δ Hδ,
|
||||
apply lt_of_le_of_lt,
|
||||
rotate 1,
|
||||
apply sub_lt_of_pos,
|
||||
exact and.left Hδ,
|
||||
exact sup_fn_interval,
|
||||
apply sup_le,
|
||||
exact exists.intro a (and.intro Hab Ha),
|
||||
intro x Hx,
|
||||
apply le_of_not_gt,
|
||||
intro Hxgt,
|
||||
have Hxgt' : b - x < δ, from sub_lt_of_sub_lt _ _ _ Hxgt,
|
||||
rewrite -(abs_of_pos (sub_pos_of_lt _ _ (and.left Hx))) at Hxgt',
|
||||
let Hxgt'' := and.right Hδ _ Hxgt',
|
||||
exact not_lt_of_ge (le_of_lt Hxgt'') (and.right Hx)
|
||||
end
|
||||
|
||||
end
|
||||
|
||||
private definition neg_f (f : ℝ → ℝ) := λ x, - f x
|
||||
|
||||
private theorem neg_continuous_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) : continuous (neg_f f) :=
|
||||
begin
|
||||
intros x ε Hε,
|
||||
cases Hcon x Hε with δ Hδ,
|
||||
cases Hδ with Hδ₁ Hδ₂,
|
||||
existsi δ,
|
||||
split,
|
||||
assumption,
|
||||
intros x' Hx',
|
||||
let HD := Hδ₂ x' Hx',
|
||||
rewrite [-abs_neg, ↑neg_f, neg_neg_sub_neg],
|
||||
assumption
|
||||
end
|
||||
|
||||
theorem intermediate_value_decr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b)
|
||||
(Ha : f a > 0) (Hb : f b < 0) : ∃ c, a < c ∧ c < b ∧ f c = 0 :=
|
||||
begin
|
||||
have Ha' : (neg_f f) a < 0, from neg_neg_of_pos Ha,
|
||||
have Hb' : (neg_f f) b > 0, from neg_pos_of_neg Hb,
|
||||
have Hcon : continuous (neg_f f), from neg_continuous_of_continuous Hf,
|
||||
let Hiv := intermediate_value_incr Hcon Hab Ha' Hb',
|
||||
cases Hiv with c Hc,
|
||||
existsi c,
|
||||
split,
|
||||
exact and.left Hc,
|
||||
split,
|
||||
exact and.left (and.right Hc),
|
||||
apply eq_zero_of_neg_eq_zero,
|
||||
apply and.right (and.right Hc)
|
||||
end
|
||||
|
||||
end inter_val
|
||||
/-
|
||||
proposition converges_to_at_unique {f : M → N} {y₁ y₂ : N} {x : M}
|
||||
(H₁ : f ⟶ y₁ '[at x]) (H₂ : f ⟶ y₂ '[at x]) : y₁ = y₂ :=
|
||||
|
|
|
|||
Loading…
Reference in a new issue