imports Topology_Euclidean_Space Extended_Real

(* Title: HOL/Multivariate_Analysis/Extended_Real_Limits.thy Author: Johannes Hölzl, TU München Author: Robert Himmelmann, TU München Author: Armin Heller, TU München Author: Bogdan Grechuk, University of Edinburgh *) section ‹Limits on the Extended real number line› theory Extended_Real_Limits imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function" begin lemma compact_UNIV: "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)" using compact_complete_linorder by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def) lemma compact_eq_closed: fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" shows "compact S ⟷ closed S" using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed by auto lemma closed_contains_Sup_cl: fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" assumes "closed S" and "S ≠ {}" shows "Sup S ∈ S" proof - from compact_eq_closed[of S] compact_attains_sup[of S] assms obtain s where S: "s ∈ S" "∀t∈S. t ≤ s" by auto then have "Sup S = s" by (auto intro!: Sup_eqI) with S show ?thesis by simp qed lemma closed_contains_Inf_cl: fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" assumes "closed S" and "S ≠ {}" shows "Inf S ∈ S" proof - from compact_eq_closed[of S] compact_attains_inf[of S] assms obtain s where S: "s ∈ S" "∀t∈S. s ≤ t" by auto then have "Inf S = s" by (auto intro!: Inf_eqI) with S show ?thesis by simp qed instance ereal :: second_countable_topology proof (standard, intro exI conjI) let ?B = "(⋃r∈ℚ. {{..< r}, {r <..}} :: ereal set set)" show "countable ?B" by (auto intro: countable_rat) show "open = generate_topology ?B" proof (intro ext iffI) fix S :: "ereal set" assume "open S" then show "generate_topology ?B S" unfolding open_generated_order proof induct case (Basis b) then obtain e where "b = {..<e} ∨ b = {e<..}" by auto moreover have "{..<e} = ⋃{{..<x}|x. x ∈ ℚ ∧ x < e}" "{e<..} = ⋃{{x<..}|x. x ∈ ℚ ∧ e < x}" by (auto dest: ereal_dense3 simp del: ex_simps simp add: ex_simps[symmetric] conj_commute Rats_def image_iff) ultimately show ?case by (auto intro: generate_topology.intros) qed (auto intro: generate_topology.intros) next fix S assume "generate_topology ?B S" then show "open S" by induct auto qed qed lemma ereal_open_closed_aux: fixes S :: "ereal set" assumes "open S" and "closed S" and S: "(-∞) ∉ S" shows "S = {}" proof (rule ccontr) assume "¬ ?thesis" then have *: "Inf S ∈ S" by (metis assms(2) closed_contains_Inf_cl) { assume "Inf S = -∞" then have False using * assms(3) by auto } moreover { assume "Inf S = ∞" then have "S = {∞}" by (metis Inf_eq_PInfty ‹S ≠ {}›) then have False by (metis assms(1) not_open_singleton) } moreover { assume fin: "¦Inf S¦ ≠ ∞" from ereal_open_cont_interval[OF assms(1) * fin] obtain e where e: "e > 0" "{Inf S - e<..<Inf S + e} ⊆ S" . then obtain b where b: "Inf S - e < b" "b < Inf S" using fin ereal_between[of "Inf S" e] dense[of "Inf S - e"] by auto then have "b: {Inf S - e <..< Inf S + e}" using e fin ereal_between[of "Inf S" e] by auto then have "b ∈ S" using e by auto then have False using b by (metis complete_lattice_class.Inf_lower leD) } ultimately show False by auto qed lemma ereal_open_closed: fixes S :: "ereal set" shows "open S ∧ closed S ⟷ S = {} ∨ S = UNIV" proof - { assume lhs: "open S ∧ closed S" { assume "-∞ ∉ S" then have "S = {}" using lhs ereal_open_closed_aux by auto } moreover { assume "-∞ ∈ S" then have "- S = {}" using lhs ereal_open_closed_aux[of "-S"] by auto } ultimately have "S = {} ∨ S = UNIV" by auto } then show ?thesis by auto qed lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} ⟷ x = -∞" proof assume "x = -∞" then have "{x..} = UNIV" by auto then show "open {x..}" by auto next assume "open {x..}" then have "open {x..} ∧ closed {x..}" by auto then have "{x..} = UNIV" unfolding ereal_open_closed by auto then show "x = -∞" by (simp add: bot_ereal_def atLeast_eq_UNIV_iff) qed lemma mono_closed_real: fixes S :: "real set" assumes mono: "∀y z. y ∈ S ∧ y ≤ z ⟶ z ∈ S" and "closed S" shows "S = {} ∨ S = UNIV ∨ (∃a. S = {a..})" proof - { assume "S ≠ {}" { assume ex: "∃B. ∀x∈S. B ≤ x" then have *: "∀x∈S. Inf S ≤ x" using cInf_lower[of _ S] ex by (metis bdd_below_def) then have "Inf S ∈ S" apply (subst closed_contains_Inf) using ex ‹S ≠ {}› ‹closed S› apply auto done then have "∀x. Inf S ≤ x ⟷ x ∈ S" using mono[rule_format, of "Inf S"] * by auto then have "S = {Inf S ..}" by auto then have "∃a. S = {a ..}" by auto } moreover { assume "¬ (∃B. ∀x∈S. B ≤ x)" then have nex: "∀B. ∃x∈S. x < B" by (simp add: not_le) { fix y obtain x where "x∈S" and "x < y" using nex by auto then have "y ∈ S" using mono[rule_format, of x y] by auto } then have "S = UNIV" by auto } ultimately have "S = UNIV ∨ (∃a. S = {a ..})" by blast } then show ?thesis by blast qed lemma mono_closed_ereal: fixes S :: "real set" assumes mono: "∀y z. y ∈ S ∧ y ≤ z ⟶ z ∈ S" and "closed S" shows "∃a. S = {x. a ≤ ereal x}" proof - { assume "S = {}" then have ?thesis apply (rule_tac x=PInfty in exI) apply auto done } moreover { assume "S = UNIV" then have ?thesis apply (rule_tac x="-∞" in exI) apply auto done } moreover { assume "∃a. S = {a ..}" then obtain a where "S = {a ..}" by auto then have ?thesis apply (rule_tac x="ereal a" in exI) apply auto done } ultimately show ?thesis using mono_closed_real[of S] assms by auto qed lemma Liminf_within: fixes f :: "'a::metric_space ⇒ 'b::complete_lattice" shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S ∩ ball x e - {x}). f y)" unfolding Liminf_def eventually_at proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe) fix P d assume "0 < d" and "∀y. y ∈ S ⟶ y ≠ x ∧ dist y x < d ⟶ P y" then have "S ∩ ball x d - {x} ⊆ {x. P x}" by (auto simp: zero_less_dist_iff dist_commute) then show "∃r>0. INFIMUM (Collect P) f ≤ INFIMUM (S ∩ ball x r - {x}) f" by (intro exI[of _ d] INF_mono conjI ‹0 < d›) auto next fix d :: real assume "0 < d" then show "∃P. (∃d>0. ∀xa. xa ∈ S ⟶ xa ≠ x ∧ dist xa x < d ⟶ P xa) ∧ INFIMUM (S ∩ ball x d - {x}) f ≤ INFIMUM (Collect P) f" by (intro exI[of _ "λy. y ∈ S ∩ ball x d - {x}"]) (auto intro!: INF_mono exI[of _ d] simp: dist_commute) qed lemma Limsup_within: fixes f :: "'a::metric_space ⇒ 'b::complete_lattice" shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S ∩ ball x e - {x}). f y)" unfolding Limsup_def eventually_at proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe) fix P d assume "0 < d" and "∀y. y ∈ S ⟶ y ≠ x ∧ dist y x < d ⟶ P y" then have "S ∩ ball x d - {x} ⊆ {x. P x}" by (auto simp: zero_less_dist_iff dist_commute) then show "∃r>0. SUPREMUM (S ∩ ball x r - {x}) f ≤ SUPREMUM (Collect P) f" by (intro exI[of _ d] SUP_mono conjI ‹0 < d›) auto next fix d :: real assume "0 < d" then show "∃P. (∃d>0. ∀xa. xa ∈ S ⟶ xa ≠ x ∧ dist xa x < d ⟶ P xa) ∧ SUPREMUM (Collect P) f ≤ SUPREMUM (S ∩ ball x d - {x}) f" by (intro exI[of _ "λy. y ∈ S ∩ ball x d - {x}"]) (auto intro!: SUP_mono exI[of _ d] simp: dist_commute) qed lemma Liminf_at: fixes f :: "'a::metric_space ⇒ 'b::complete_lattice" shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)" using Liminf_within[of x UNIV f] by simp lemma Limsup_at: fixes f :: "'a::metric_space ⇒ 'b::complete_lattice" shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)" using Limsup_within[of x UNIV f] by simp lemma min_Liminf_at: fixes f :: "'a::metric_space ⇒ 'b::complete_linorder" shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)" unfolding inf_min[symmetric] Liminf_at apply (subst inf_commute) apply (subst SUP_inf) apply (intro SUP_cong[OF refl]) apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union) apply (drule sym) apply auto apply (metis INF_absorb centre_in_ball) done subsection ‹monoset› definition (in order) mono_set: "mono_set S ⟷ (∀x y. x ≤ y ⟶ x ∈ S ⟶ y ∈ S)" lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto lemma (in complete_linorder) mono_set_iff: fixes S :: "'a set" defines "a ≡ Inf S" shows "mono_set S ⟷ S = {a <..} ∨ S = {a..}" (is "_ = ?c") proof assume "mono_set S" then have mono: "⋀x y. x ≤ y ⟹ x ∈ S ⟹ y ∈ S" by (auto simp: mono_set) show ?c proof cases assume "a ∈ S" show ?c using mono[OF _ ‹a ∈ S›] by (auto intro: Inf_lower simp: a_def) next assume "a ∉ S" have "S = {a <..}" proof safe fix x assume "x ∈ S" then have "a ≤ x" unfolding a_def by (rule Inf_lower) then show "a < x" using ‹x ∈ S› ‹a ∉ S› by (cases "a = x") auto next fix x assume "a < x" then obtain y where "y < x" "y ∈ S" unfolding a_def Inf_less_iff .. with mono[of y x] show "x ∈ S" by auto qed then show ?c .. qed qed auto lemma ereal_open_mono_set: fixes S :: "ereal set" shows "open S ∧ mono_set S ⟷ S = UNIV ∨ S = {Inf S <..}" by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast ereal_open_closed mono_set_iff open_ereal_greaterThan) lemma ereal_closed_mono_set: fixes S :: "ereal set" shows "closed S ∧ mono_set S ⟷ S = {} ∨ S = {Inf S ..}" by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan) lemma ereal_Liminf_Sup_monoset: fixes f :: "'a ⇒ ereal" shows "Liminf net f = Sup {l. ∀S. open S ⟶ mono_set S ⟶ l ∈ S ⟶ eventually (λx. f x ∈ S) net}" (is "_ = Sup ?A") proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least) fix P assume P: "eventually P net" fix S assume S: "mono_set S" "INFIMUM (Collect P) f ∈ S" { fix x assume "P x" then have "INFIMUM (Collect P) f ≤ f x" by (intro complete_lattice_class.INF_lower) simp with S have "f x ∈ S" by (simp add: mono_set) } with P show "eventually (λx. f x ∈ S) net" by (auto elim: eventually_mono) next fix y l assume S: "∀S. open S ⟶ mono_set S ⟶ l ∈ S ⟶ eventually (λx. f x ∈ S) net" assume P: "∀P. eventually P net ⟶ INFIMUM (Collect P) f ≤ y" show "l ≤ y" proof (rule dense_le) fix B assume "B < l" then have "eventually (λx. f x ∈ {B <..}) net" by (intro S[rule_format]) auto then have "INFIMUM {x. B < f x} f ≤ y" using P by auto moreover have "B ≤ INFIMUM {x. B < f x} f" by (intro INF_greatest) auto ultimately show "B ≤ y" by simp qed qed lemma ereal_Limsup_Inf_monoset: fixes f :: "'a ⇒ ereal" shows "Limsup net f = Inf {l. ∀S. open S ⟶ mono_set (uminus ` S) ⟶ l ∈ S ⟶ eventually (λx. f x ∈ S) net}" (is "_ = Inf ?A") proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest) fix P assume P: "eventually P net" fix S assume S: "mono_set (uminus`S)" "SUPREMUM (Collect P) f ∈ S" { fix x assume "P x" then have "f x ≤ SUPREMUM (Collect P) f" by (intro complete_lattice_class.SUP_upper) simp with S(1)[unfolded mono_set, rule_format, of "- SUPREMUM (Collect P) f" "- f x"] S(2) have "f x ∈ S" by (simp add: inj_image_mem_iff) } with P show "eventually (λx. f x ∈ S) net" by (auto elim: eventually_mono) next fix y l assume S: "∀S. open S ⟶ mono_set (uminus ` S) ⟶ l ∈ S ⟶ eventually (λx. f x ∈ S) net" assume P: "∀P. eventually P net ⟶ y ≤ SUPREMUM (Collect P) f" show "y ≤ l" proof (rule dense_ge) fix B assume "l < B" then have "eventually (λx. f x ∈ {..< B}) net" by (intro S[rule_format]) auto then have "y ≤ SUPREMUM {x. f x < B} f" using P by auto moreover have "SUPREMUM {x. f x < B} f ≤ B" by (intro SUP_least) auto ultimately show "y ≤ B" by simp qed qed lemma liminf_bounded_open: fixes x :: "nat ⇒ ereal" shows "x0 ≤ liminf x ⟷ (∀S. open S ⟶ mono_set S ⟶ x0 ∈ S ⟶ (∃N. ∀n≥N. x n ∈ S))" (is "_ ⟷ ?P x0") proof assume "?P x0" then show "x0 ≤ liminf x" unfolding ereal_Liminf_Sup_monoset eventually_sequentially by (intro complete_lattice_class.Sup_upper) auto next assume "x0 ≤ liminf x" { fix S :: "ereal set" assume om: "open S" "mono_set S" "x0 ∈ S" { assume "S = UNIV" then have "∃N. ∀n≥N. x n ∈ S" by auto } moreover { assume "S ≠ UNIV" then obtain B where B: "S = {B<..}" using om ereal_open_mono_set by auto then have "B < x0" using om by auto then have "∃N. ∀n≥N. x n ∈ S" unfolding B using ‹x0 ≤ liminf x› liminf_bounded_iff by auto } ultimately have "∃N. ∀n≥N. x n ∈ S" by auto } then show "?P x0" by auto qed subsection "Relate extended reals and the indicator function" lemma ereal_indicator_le_0: "(indicator S x::ereal) ≤ 0 ⟷ x ∉ S" by (auto split: split_indicator simp: one_ereal_def) lemma ereal_indicator: "ereal (indicator A x) = indicator A x" by (auto simp: indicator_def one_ereal_def) lemma ereal_mult_indicator: "ereal (x * indicator A y) = ereal x * indicator A y" by (simp split: split_indicator) lemma ereal_indicator_mult: "ereal (indicator A y * x) = indicator A y * ereal x" by (simp split: split_indicator) lemma ereal_indicator_nonneg[simp, intro]: "0 ≤ (indicator A x ::ereal)" unfolding indicator_def by auto lemma indicator_inter_arith_ereal: "indicator A x * indicator B x = (indicator (A ∩ B) x :: ereal)" by (simp split: split_indicator) end