From ea3915f279dc0e0368b5b7d746a80428fdad7ce2 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Tue, 15 Sep 2015 18:57:08 -0400 Subject: [PATCH] feat(library/theories/analysis): prove intermediate value theorem --- library/theories/analysis/metric_space.lean | 42 ++++ library/theories/analysis/real_limit.lean | 263 +++++++++++++++++++- 2 files changed, 303 insertions(+), 2 deletions(-) diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index 727e9bbf9..cd65985b5 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -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 diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index 0fe675d88..48be1669f 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -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₂ :=