From eae80118bfa715f9c81ce22287640a6cd5d05657 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 16 May 2016 09:40:20 -0400 Subject: [PATCH] feat(library/theories/topology/limit.lean): add topological filters --- library/theories/topology/limit.lean | 206 ++++++++++++++++++++++++++- 1 file changed, 203 insertions(+), 3 deletions(-) diff --git a/library/theories/topology/limit.lean b/library/theories/topology/limit.lean index 1f268ec62..e8cca37bf 100644 --- a/library/theories/topology/limit.lean +++ b/library/theories/topology/limit.lean @@ -62,7 +62,7 @@ and iff rules. Again, see also specific versions for metric spaces, normed space Note that the filters at_infty and at_ninfty don't rely on topological notions at all, only the existence of a suitable order. -/ -import data.set data.nat algebra.interval +import data.set data.nat algebra.interval .basic import theories.move -- TODO: remove after move to Lean 3 open set function set.filter interval @@ -263,6 +263,7 @@ section linorderX (assume H, obtain x Hx, from H, eventually_at_infty Hx) end linorderX + /- at_ninfty -/ section linorderX @@ -315,7 +316,8 @@ section linorderX (assume H, obtain x Hx, from H, eventually_at_ninfty Hx) end linorderX -/- approaches infty -/ + +/- approaches_infty -/ section approaches_infty variable [linear_strong_order_pair Y] @@ -355,7 +357,8 @@ section approaches_infty eventually_mpr H (eventually_mpr this (eventually_of_forall _ (take x, le.trans)))) end approaches_infty -/- approaches ninfty -/ + +/- approaches_ninfty -/ section approaches_ninfty variable [linear_strong_order_pair Y] @@ -395,4 +398,201 @@ section approaches_ninfty (take x H₁ H₂, le.trans H₂ H₁)))) end approaches_ninfty + +/- the nhds filter -/ + +open topology + +section nhds_filter + variables [topology X] {P : X → Prop} + + definition nhds (x : X) : filter X := Inf (principal ' {s | Open s ∧ x ∈ s}) + + proposition eventually_nhds {x : X} {s : set X} (Os : Open s) (xs : x ∈ s) (H : ∀₀ x ∈ s, P x) : + eventually P (nhds x) := + eventually_Inf (mem_image_of_mem _ (and.intro Os xs)) (eventually_principal H) + + proposition eventually_mem_nhds {x : X} {s : set X} (Os : Open s) (xs : x ∈ s) : + eventually (λ x, x ∈ s) (nhds x) := + eventually_nhds Os xs (λ x Hx, Hx) + + proposition exists_of_eventually_nhds {x : X} (H : eventually P (nhds x)) : + ∃ s, Open s ∧ x ∈ s ∧ ∀₀ x ∈ s, P x := + let princS := principal ' {s | Open s ∧ x ∈ s} in + have principal univ ∈ princS, + from mem_image_of_mem principal (and.intro Open_univ !mem_univ), + have ∃₀ F ∈ princS, eventually P F, from + exists_eventually_of_eventually_Inf this H + (λ F₁ (F₁mem : F₁ ∈ princS) F₂ (F₂mem : F₂ ∈ princS), + obtain s₁ [[Os₁ xs₁] (F₁eq : principal s₁ = F₁)], from F₁mem, + obtain s₂ [[Os₂ xs₂] (F₂eq : principal s₂ = F₂)], from F₂mem, + have F₁ ⊓ F₂ ∈ princS, + begin + rewrite [-F₁eq, -F₂eq, principal_inf_principal], + exact mem_image_of_mem _ (and.intro (Open_inter Os₁ Os₂) (mem_inter xs₁ xs₂)) + end, + show ∃₀ F ∈ princS, F ≤ F₁ ⊓ F₂, from exists.intro _ (and.intro this !le.refl)), + obtain F [Fmem ePF], from this, + obtain s [[Os xs] (Feq : principal s = F)], from Fmem, + exists.intro s (and.intro Os (and.intro xs + (subset_of_eventually_principal (by rewrite Feq; exact ePF)))) + + proposition eventually_nhds_iff (x : X) : + eventually P (nhds x) ↔ ∃ s, Open s ∧ x ∈ s ∧ ∀₀ x ∈ s, P x := + iff.intro exists_of_eventually_nhds + (assume H, obtain s [Os [xs Hs]], from H, eventually_nhds Os xs Hs) +end nhds_filter + + +/- the at_within filter -/ + +section at_within + variables [topology X] {P : X → Prop} + + definition at_within (x : X) (s : set X) : filter X := inf (nhds x) (principal (s \ '{x})) + + notation [at x ` within ` s] := at_within x s + + proposition eventually_at_within {x : X} {s t : set X} (Os : Open s) (xs : x ∈ s) + (Hs : ∀₀ y ∈ s, y ≠ x → y ∈ t → P y) : + eventually P [at x within t] := + have H₁ : eventually (λ y, y ≠ x → y ∈ t → P y) (nhds x), + from eventually_nhds Os xs Hs, + eventually_inf H₁ _ (mem_principal _) + (take y, assume Hy, + have H : y ∈ t \ '{x}, from and.right Hy, + have H' : y ≠ x, from suppose y = x, + have y ∈ '{x}, from mem_singleton_of_eq this, + show false, from and.right H this, + show P y, from and.left Hy `y ≠ x` (and.left H)) + + proposition exists_of_eventually_at_within {x : X} {t : set X} + (H : eventually P [at x within t]) : + ∃ s, Open s ∧ x ∈ s ∧ ∀₀ y ∈ s, y ≠ x → y ∈ t → P y := + obtain P₁ [eP₁nhds [P₂ [eP₂princ (H' : P ⊇ P₁ ∩ P₂)]]], from exists_of_eventually_inf H, + obtain s [Os [xs Hs]], from exists_of_eventually_nhds eP₁nhds, + have Ht : ∀₀ y ∈ t \ '{x}, P₂ y, from subset_of_eventually_principal eP₂princ, + exists.intro s (and.intro Os (and.intro xs + (take y, assume ys ynex yt, + have y ∉ '{x}, from assume ymem, ynex (eq_of_mem_singleton ymem), + show P y, from H' (and.intro (Hs y ys) (Ht (mem_diff yt this)))))) + + theorem eventually_at_within_iff (x : X) {s : set X} : + eventually P [at x within s] ↔ ∃ t, Open t ∧ x ∈ t ∧ ∀₀ y ∈ t, y ≠ x → y ∈ s → P y := + iff.intro exists_of_eventually_at_within + (assume H, obtain t [Ot [xt Ht]], from H, eventually_at_within Ot xt Ht) + + abbreviation at_elt (x : X) : filter X := at_within x univ + + notation [at x] := at_elt x + + proposition eventually_at {x : X} {s : set X} (Os : Open s) (xs : x ∈ s) + (Hs : ∀₀ y ∈ s, y ≠ x → P y) : + eventually P [at x] := + eventually_at_within Os xs (take y, assume ys ynex yuniv, Hs ys ynex) + + proposition exists_of_eventually_at {x : X} (H : eventually P [at x]) : + ∃ s, Open s ∧ x ∈ s ∧ ∀₀ y ∈ s, y ≠ x → P y := + obtain s [Os [xs Hs]], from exists_of_eventually_at_within H, + exists.intro s (and.intro Os (and.intro xs (λ y ys ynex, Hs y ys ynex trivial))) + + proposition eventually_at_iff (x : X) : + eventually P [at x] ↔ ∃ s, Open s ∧ x ∈ s ∧ ∀₀ y ∈ s, y ≠ x → P y := + iff.intro exists_of_eventually_at + (assume H, obtain s [Os [xs Hs]], from H, eventually_at Os xs Hs) + + proposition at_within_eq_of_Open {x : X} {s : set X} (Os : Open s) (xs : x ∈ s) : + [at x within s] = [at x] := + filter.eq (ext (take P, iff.intro + (assume H, + obtain t [Ot [xt Ht]], from exists_of_eventually_at_within H, + eventually_at (Open_inter Os Ot) (mem_inter xs xt) + (λ y Hy yne, Ht _ (and.right Hy) yne (and.left Hy))) + (assume H, + obtain t [Ot [xt Ht]], from exists_of_eventually_at H, + eventually_at_within (Open_inter Os Ot) (mem_inter xs xt) + (λ y Hy yne ys, Ht _ (and.right Hy) yne)))) +end at_within + + +/- at_left and at_right -/ + +section at_left_at_right + variables [topology X] [linear_strong_order_pair X] {P : X → Prop} + + abbreviation at_left (x : X) : filter X := [at x within '(-∞, x)] + abbreviation at_right (x : X) : filter X := [at x within '(x, ∞)] + + notation [at x`-]` := at_left x + notation [at x`+]` := at_right x + + proposition eventually_at_left {x : X} {s : set X} (Os : Open s) (xs : x ∈ s) + (H : ∀₀ y ∈ s, y < x → P y) : + eventually P [at x-] := + eventually_at_within Os xs (take y, assume ys ynex yltx, H ys yltx) + + proposition exists_of_eventually_at_left {x : X} (H : eventually P [at x-]) : + ∃ s, Open s ∧ x ∈ s ∧ ∀₀ y ∈ s, y < x → P y := + obtain s [Os [xs Hs]], from exists_of_eventually_at_within H, + exists.intro s (and.intro Os (and.intro xs + (take y, assume ys yltx, + show P y, from Hs y ys (ne_of_lt yltx) yltx))) + + variable (P) + proposition eventually_at_left_iff (x : X) : + eventually P [at x-] ↔ ∃ s, Open s ∧ x ∈ s ∧ ∀₀ y ∈ s, y < x → P y := + iff.intro exists_of_eventually_at_left + (take H, obtain s [Os [xs Hs]], from H, eventually_at_left Os xs Hs) + + variable {P} + proposition eventually_at_right {x : X} {s : set X} (Os : Open s) (xs : x ∈ s) + (H : ∀₀ y ∈ s, y > x → P y) : + eventually P [at x+] := + eventually_at_within Os xs (take y, assume ys ynex yltx, H ys yltx) + + proposition exists_of_eventually_at_right {x : X} (H : eventually P [at x+]) : + ∃ s, Open s ∧ x ∈ s ∧ ∀₀ y ∈ s, y > x → P y := + obtain s [Os [xs Hs]], from exists_of_eventually_at_within H, + exists.intro s (and.intro Os (and.intro xs + (take y, assume ys yltx, + show P y, from Hs y ys (ne_of_gt yltx) yltx))) + + variable (P) + proposition eventually_at_right_iff (x : X) : + eventually P [at x+] ↔ ∃ s, Open s ∧ x ∈ s ∧ ∀₀ y ∈ s, y > x → P y := + iff.intro exists_of_eventually_at_right + (take H, obtain s [Os [xs Hs]], from H, eventually_at_right Os xs Hs) +end at_left_at_right + + +/- approaches -/ + +section approaches + variables [topology Y] + variables {F : filter X} {f : X → Y} {y : Y} + + abbreviation approaches (f : X → Y) (y : Y) : filter X → Prop := tendsto f (nhds y) + + notation f ⟶ y := approaches f y + + proposition approaches_intro (H : ∀ s, Open s → y ∈ s → eventually (λ x, f x ∈ s) F) : + (f ⟶ y) F := + tendsto_of_forall_eventually + (take P, assume eventuallyP, + obtain s [Os [(ys : y ∈ s) (H' : ∀₀ y' ∈ s, P y')]], + from exists_of_eventually_nhds eventuallyP, + have eventually (λ x, P (f x)) F, from eventually_mono (H s Os ys) (λ x Hx, H' Hx), + show eventually P (mapfilter f F), from eventually_mapfilter this) + + proposition approaches_elim (H : (f ⟶ y) F) {s : set Y} (Os : Open s) (ys : y ∈ s) : + eventually (λ x, f x ∈ s) F := + have eventually (λ y', y' ∈ s) (mapfilter f F), + from eventually_mapfilter_of_tendsto H (eventually_mem_nhds Os ys), + eventually_of_eventually_mapfilter this + + variables (F f y) + proposition approaches_iff : (f ⟶ y) F ↔ (∀ s, Open s → y ∈ s → eventually (λ x, f x ∈ s) F) := + iff.intro approaches_elim approaches_intro +end approaches + end topology