author paulson Thu, 18 Jul 2019 14:08:28 +0100 changeset 70563 ebd108578ab1 parent 70552 81b65ddac59f child 70564 8a7053892d8e
```--- a/src/HOL/Analysis/Change_Of_Vars.thy	Wed Jul 17 16:32:06 2019 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Jul 18 14:08:28 2019 +0100
@@ -423,77 +423,17 @@

subsection\<open>\<open>F_sigma\<close> and \<open>G_delta\<close> sets.\<close>(*FIX ME mv *)

-\<comment> \<open>\<^url>\<open>https://en.wikipedia.org/wiki/F-sigma_set\<close>\<close>
-inductive\<^marker>\<open>tag important\<close> fsigma :: "'a::topological_space set \<Rightarrow> bool" where
-  "(\<And>n::nat. closed (F n)) \<Longrightarrow> fsigma (\<Union>(F ` UNIV))"
-
-inductive\<^marker>\<open>tag important\<close> gdelta :: "'a::topological_space set \<Rightarrow> bool" where
-  "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (\<Inter>(F ` UNIV))"
-
-lemma fsigma_Union_compact:
-  fixes S :: "'a::{real_normed_vector,heine_borel} set"
-  shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = \<Union>(F ` UNIV))"
-proof safe
-  assume "fsigma S"
-  then obtain F :: "nat \<Rightarrow> 'a set" where F: "range F \<subseteq> Collect closed" "S = \<Union>(F ` UNIV)"
-    by (meson fsigma.cases image_subsetI mem_Collect_eq)
-  then have "\<exists>D::nat \<Rightarrow> 'a set. range D \<subseteq> Collect compact \<and> \<Union>(D ` UNIV) = F i" for i
-    using closed_Union_compact_subsets [of "F i"]
-    by (metis image_subsetI mem_Collect_eq range_subsetD)
-  then obtain D :: "nat \<Rightarrow> nat \<Rightarrow> 'a set"
-    where D: "\<And>i. range (D i) \<subseteq> Collect compact \<and> \<Union>((D i) ` UNIV) = F i"
-    by metis
-  let ?DD = "\<lambda>n. (\<lambda>(i,j). D i j) (prod_decode n)"
-  show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = \<Union>(F ` UNIV)"
-  proof (intro exI conjI)
-    show "range ?DD \<subseteq> Collect compact"
-      using D by clarsimp (metis mem_Collect_eq rangeI split_conv subsetCE surj_pair)
-    show "S = \<Union> (range ?DD)"
-    proof
-      show "S \<subseteq> \<Union> (range ?DD)"
-        using D F
-        by clarsimp (metis UN_iff old.prod.case prod_decode_inverse prod_encode_eq)
-      show "\<Union> (range ?DD) \<subseteq> S"
-        using D F  by fastforce
-    qed
-  qed
-next
-  fix F :: "nat \<Rightarrow> 'a set"
-  assume "range F \<subseteq> Collect compact" and "S = \<Union>(F ` UNIV)"
-  then show "fsigma (\<Union>(F ` UNIV))"
-    by (simp add: compact_imp_closed fsigma.intros image_subset_iff)
-qed
-
-lemma gdelta_imp_fsigma: "gdelta S \<Longrightarrow> fsigma (- S)"
-proof (induction rule: gdelta.induct)
-  case (1 F)
-  have "- \<Inter>(F ` UNIV) = (\<Union>i. -(F i))"
-    by auto
-  then show ?case
-    by (simp add: fsigma.intros closed_Compl 1)
-qed
-
-lemma fsigma_imp_gdelta: "fsigma S \<Longrightarrow> gdelta (- S)"
-proof (induction rule: fsigma.induct)
-  case (1 F)
-  have "- \<Union>(F ` UNIV) = (\<Inter>i. -(F i))"
-    by auto
-  then show ?case
-    by (simp add: 1 gdelta.intros open_closed)
-qed
-
-lemma gdelta_complement: "gdelta(- S) \<longleftrightarrow> fsigma S"
-  using fsigma_imp_gdelta gdelta_imp_fsigma by force
-
text\<open>A Lebesgue set is almost an \<open>F_sigma\<close> or \<open>G_delta\<close>.\<close>
lemma lebesgue_set_almost_fsigma:
assumes "S \<in> sets lebesgue"
obtains C T where "fsigma C" "negligible T" "C \<union> T = S" "disjnt C T"
proof -
{ fix n::nat
-    have "\<exists>T. closed T \<and> T \<subseteq> S \<and> S - T \<in> lmeasurable \<and> measure lebesgue (S-T) < 1 / Suc n"
+    obtain T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "emeasure lebesgue (S - T) < ennreal (1 / Suc n)"
using sets_lebesgue_inner_closed [OF assms]
-      by (metis divide_pos_pos less_numeral_extra(1) of_nat_0_less_iff zero_less_Suc)
+      by (metis of_nat_0_less_iff zero_less_Suc zero_less_divide_1_iff)
+    then have "\<exists>T. closed T \<and> T \<subseteq> S \<and> S - T \<in> lmeasurable \<and> measure lebesgue (S-T) < 1 / Suc n"
+      by (metis emeasure_eq_measure2 ennreal_leI not_le)
}
then obtain F where F: "\<And>n::nat. closed (F n) \<and> F n \<subseteq> S \<and> S - F n \<in> lmeasurable \<and> measure lebesgue (S - F n) < 1 / Suc n"
by metis
@@ -557,16 +497,16 @@
by (metis neg negligible_iff_null_sets)
have "frontier S \<in> lmeasurable" and mS0: "measure lebesgue (frontier S) = 0"
using neg negligible_imp_measurable negligible_iff_measure by blast+
-  with \<open>e > 0\<close> lmeasurable_outer_open
+  with \<open>e > 0\<close> sets_lebesgue_outer_open
obtain U where "open U"
-    and U: "frontier S \<subseteq> U" "U - frontier S \<in> lmeasurable" "measure lebesgue (U - frontier S) < e"
+    and U: "frontier S \<subseteq> U" "U - frontier S \<in> lmeasurable" "emeasure lebesgue (U - frontier S) < e"
by (metis fmeasurableD)
with null have "U \<in> lmeasurable"
by (metis borel_open measurable_Diff_null_set sets_completionI_sets sets_lborel)
have "measure lebesgue (U - frontier S) = measure lebesgue U"
using mS0 by (simp add: \<open>U \<in> lmeasurable\<close> fmeasurableD measure_Diff_null_set null)
with U have mU: "measure lebesgue U < e"
-    by simp
+    by (simp add: emeasure_eq_measure2 ennreal_less_iff)
show ?thesis
proof
have "U \<noteq> UNIV"
@@ -612,12 +552,12 @@
assumes "S \<in> sets lebesgue"
obtains K C where "negligible K" "\<And>n::nat. compact(C n)" "S = (\<Union>n. C n) \<union> K"
proof -
-  have "\<exists>T. closed T \<and> T \<subseteq> S \<and> (S - T) \<in> lmeasurable \<and> measure lebesgue (S - T) < (1/2)^n" for n
+  have "\<exists>T. closed T \<and> T \<subseteq> S \<and> (S - T) \<in> lmeasurable \<and> emeasure lebesgue (S - T) < ennreal ((1/2)^n)" for n
using sets_lebesgue_inner_closed assms
by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power)
then obtain C where clo: "\<And>n. closed (C n)" and subS: "\<And>n. C n \<subseteq> S"
and mea: "\<And>n. (S - C n) \<in> lmeasurable"
-    and less: "\<And>n. measure lebesgue (S - C n) < (1/2)^n"
+    and less: "\<And>n. emeasure lebesgue (S - C n) < ennreal ((1/2)^n)"
by metis
have "\<exists>F. (\<forall>n::nat. compact(F n)) \<and> (\<Union>n. F n) = C m" for m::nat
by (metis clo closed_Union_compact_subsets)
@@ -645,7 +585,8 @@
show "S - C n \<in> lmeasurable"
show "measure lebesgue (S - C n) \<le> e"
-          using less [of n] n by simp
+          using less [of n] n
+          by (simp add: emeasure_eq_measure2 less_le mea)
qed
qed
show "compact (?C n)" for n
@@ -758,9 +699,11 @@
have eps_d: "f ` S \<in> lmeasurable"  "?\<mu> (f ` S) \<le> (B+e) * (?\<mu> S + d)" (is "?MD")
if "d > 0" for d
proof -
-        obtain T where "open T" "S \<subseteq> T" and TS: "(T-S) \<in> lmeasurable" and "?\<mu> (T-S) < d"
-          using S \<open>d > 0\<close> lmeasurable_outer_open by blast
-        with S have "T \<in> lmeasurable" and Tless: "?\<mu> T < ?\<mu> S + d"
+        obtain T where T: "open T" "S \<subseteq> T" and TS: "(T-S) \<in> lmeasurable" and "emeasure lebesgue (T-S) < ennreal d"
+          using S \<open>d > 0\<close> sets_lebesgue_outer_open by blast
+        then have "?\<mu> (T-S) < d"
+          by (metis emeasure_eq_measure2 ennreal_leI not_less)
+        with S T TS have "T \<in> lmeasurable" and Tless: "?\<mu> T < ?\<mu> S + d"
by (auto simp: measurable_measure_Diff dest!: fmeasurable_Diff_D)
have "\<exists>r. 0 < r \<and> r < d \<and> ball x r \<subseteq> T \<and> f ` (S \<inter> ball x r) \<in> lmeasurable \<and>
?\<mu> (f ` (S \<inter> ball x r)) \<le> (B + e) * ?\<mu> (ball x r)"```
```--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Jul 17 16:32:06 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Jul 18 14:08:28 2019 +0100
@@ -1168,6 +1168,10 @@
qed auto
qed

+corollary eventually_ae_filter_negligible:
+  "eventually P (ae_filter lebesgue) \<longleftrightarrow> (\<exists>N. negligible N \<and> {x. \<not> P x} \<subseteq> N)"
+  by (auto simp: completion.AE_iff_null_sets negligible_iff_null_sets null_sets_completion_subset)
+
lemma starlike_negligible:
assumes "closed S"
and eq1: "\<And>c x. (a + c *\<^sub>R x) \<in> S \<Longrightarrow> 0 \<le> c \<Longrightarrow> a + x \<in> S \<Longrightarrow> c = 1"
@@ -1561,7 +1565,8 @@
using \<open>0 < e\<close> \<open>0 < B\<close> by (simp add: divide_simps)
obtain T where "open T" "S \<subseteq> T" "(T - S) \<in> lmeasurable"
"measure lebesgue (T - S) < e/2 / (2 * B * DIM('M)) ^ DIM('N)"
-    by (rule lmeasurable_outer_open [OF \<open>S \<in> sets lebesgue\<close> e22])
+    using sets_lebesgue_outer_open [OF \<open>S \<in> sets lebesgue\<close> e22]
+    by (metis emeasure_eq_measure2 ennreal_leI linorder_not_le)
then have T: "measure lebesgue T \<le> e/2 / (2 * B * DIM('M)) ^ DIM('N)"
using \<open>negligible S\<close> by (simp add: measure_Diff_null_set negligible_iff_null_sets)
have "\<exists>r. 0 < r \<and> r \<le> 1/2 \<and>
@@ -3563,7 +3568,7 @@
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
assumes f: "\<And>k. (f k) integrable_on S" and h: "h integrable_on S"
and le: "\<And>k x. x \<in> S \<Longrightarrow> norm (f k x) \<le> h x"
-    and conv: "\<forall>x \<in> S. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+    and conv: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
shows "g integrable_on S" "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> integral S g"
proof -
have 3: "h absolutely_integrable_on S"
@@ -3709,8 +3714,7 @@
using fU absolutely_integrable_on_def by blast
show "(\<lambda>x. if x \<in> \<Union>(s ` UNIV) then norm(f x) else 0) integrable_on UNIV"
by (metis (no_types) absolutely_integrable_on_def f integrable_restrict_UNIV)
-    show "\<forall>x\<in>UNIV.
-         (\<lambda>n. if x \<in> (\<Union>m\<le>n. s m) then f x else 0)
+    show "\<And>x. (\<lambda>n. if x \<in> (\<Union>m\<le>n. s m) then f x else 0)
\<longlonglongrightarrow> (if x \<in> \<Union>(s ` UNIV) then f x else 0)"
by (force intro: tendsto_eventually eventually_sequentiallyI)
qed auto```
```--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Jul 17 16:32:06 2019 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Jul 18 14:08:28 2019 +0100
@@ -393,6 +393,9 @@
and measurable_lborel2[simp]: "measurable lborel M = measurable borel M"

+lemma space_lebesgue_on [simp]: "space (lebesgue_on S) = S"
+
lemma sets_lebesgue_on_refl [iff]: "S \<in> sets (lebesgue_on S)"
by (metis inf_top.right_neutral sets.top space_borel space_completion space_lborel space_restrict_space)

@@ -1290,9 +1293,10 @@
qed (use A N in auto)
qed

-lemma lmeasurable_outer_open:
+lemma sets_lebesgue_outer_open:
+  fixes e::real
assumes S: "S \<in> sets lebesgue" and "e > 0"
-  obtains T where "open T" "S \<subseteq> T" "(T - S) \<in> lmeasurable" "measure lebesgue (T - S) < e"
+  obtains T where "open T" "S \<subseteq> T" "(T - S) \<in> lmeasurable" "emeasure lebesgue (T - S) < ennreal e"
proof -
obtain S' where S': "S \<subseteq> S'" "S' \<in> sets borel"
and null: "S' - S \<in> null_sets lebesgue"
@@ -1315,27 +1319,28 @@
by (simp add: S U(1) sets.Diff)
then show "(U - S) \<in> lmeasurable"
unfolding fmeasurable_def using U(3) eq less_le_trans by fastforce
-  with eq U show "measure lebesgue (U - S) < e"
-    by (metis \<open>U - S \<in> lmeasurable\<close> emeasure_eq_measure2 ennreal_leI not_le)
+  with eq U show "emeasure lebesgue (U - S) < e"
qed
qed

lemma sets_lebesgue_inner_closed:
+  fixes e::real
assumes "S \<in> sets lebesgue" "e > 0"
-  obtains T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "measure lebesgue (S - T) < e"
+  obtains T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "emeasure lebesgue (S - T) < ennreal e"
proof -
have "-S \<in> sets lebesgue"
using assms by (simp add: Compl_in_sets_lebesgue)
then obtain T where "open T" "-S \<subseteq> T"
-          and T: "(T - -S) \<in> lmeasurable" "measure lebesgue (T - -S) < e"
-    using lmeasurable_outer_open assms  by blast
+          and T: "(T - -S) \<in> lmeasurable" "emeasure lebesgue (T - -S) < e"
+    using sets_lebesgue_outer_open assms  by blast
show thesis
proof
show "closed (-T)"
using \<open>open T\<close> by blast
show "-T \<subseteq> S"
using \<open>- S \<subseteq> T\<close> by auto
-    show "S - ( -T) \<in> lmeasurable" "measure lebesgue (S - (- T)) < e"
+    show "S - ( -T) \<in> lmeasurable" "emeasure lebesgue (S - (- T)) < e"
using T by (auto simp: Int_commute)
qed
qed
@@ -1348,4 +1353,69 @@
"\<lbrakk>closedin (top_of_set S) T; S \<in> sets lebesgue\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
by (metis borel_closed closedin_closed sets.Int sets_completionI_sets sets_lborel)

+
+subsection\<open>\<open>F_sigma\<close> and \<open>G_delta\<close> sets.\<close>
+
+\<comment> \<open>\<^url>\<open>https://en.wikipedia.org/wiki/F-sigma_set\<close>\<close>
+inductive\<^marker>\<open>tag important\<close> fsigma :: "'a::topological_space set \<Rightarrow> bool" where
+  "(\<And>n::nat. closed (F n)) \<Longrightarrow> fsigma (\<Union>(F ` UNIV))"
+
+inductive\<^marker>\<open>tag important\<close> gdelta :: "'a::topological_space set \<Rightarrow> bool" where
+  "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (\<Inter>(F ` UNIV))"
+
+lemma fsigma_Union_compact:
+  fixes S :: "'a::{real_normed_vector,heine_borel} set"
+  shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = \<Union>(F ` UNIV))"
+proof safe
+  assume "fsigma S"
+  then obtain F :: "nat \<Rightarrow> 'a set" where F: "range F \<subseteq> Collect closed" "S = \<Union>(F ` UNIV)"
+    by (meson fsigma.cases image_subsetI mem_Collect_eq)
+  then have "\<exists>D::nat \<Rightarrow> 'a set. range D \<subseteq> Collect compact \<and> \<Union>(D ` UNIV) = F i" for i
+    using closed_Union_compact_subsets [of "F i"]
+    by (metis image_subsetI mem_Collect_eq range_subsetD)
+  then obtain D :: "nat \<Rightarrow> nat \<Rightarrow> 'a set"
+    where D: "\<And>i. range (D i) \<subseteq> Collect compact \<and> \<Union>((D i) ` UNIV) = F i"
+    by metis
+  let ?DD = "\<lambda>n. (\<lambda>(i,j). D i j) (prod_decode n)"
+  show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = \<Union>(F ` UNIV)"
+  proof (intro exI conjI)
+    show "range ?DD \<subseteq> Collect compact"
+      using D by clarsimp (metis mem_Collect_eq rangeI split_conv subsetCE surj_pair)
+    show "S = \<Union> (range ?DD)"
+    proof
+      show "S \<subseteq> \<Union> (range ?DD)"
+        using D F
+        by clarsimp (metis UN_iff old.prod.case prod_decode_inverse prod_encode_eq)
+      show "\<Union> (range ?DD) \<subseteq> S"
+        using D F  by fastforce
+    qed
+  qed
+next
+  fix F :: "nat \<Rightarrow> 'a set"
+  assume "range F \<subseteq> Collect compact" and "S = \<Union>(F ` UNIV)"
+  then show "fsigma (\<Union>(F ` UNIV))"
+    by (simp add: compact_imp_closed fsigma.intros image_subset_iff)
+qed
+
+lemma gdelta_imp_fsigma: "gdelta S \<Longrightarrow> fsigma (- S)"
+proof (induction rule: gdelta.induct)
+  case (1 F)
+  have "- \<Inter>(F ` UNIV) = (\<Union>i. -(F i))"
+    by auto
+  then show ?case
+    by (simp add: fsigma.intros closed_Compl 1)
+qed
+
+lemma fsigma_imp_gdelta: "fsigma S \<Longrightarrow> gdelta (- S)"
+proof (induction rule: fsigma.induct)
+  case (1 F)
+  have "- \<Union>(F ` UNIV) = (\<Inter>i. -(F i))"
+    by auto
+  then show ?case
+    by (simp add: 1 gdelta.intros open_closed)
+qed
+
+lemma gdelta_complement: "gdelta(- S) \<longleftrightarrow> fsigma S"
+  using fsigma_imp_gdelta gdelta_imp_fsigma by force
+
end```
```--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Wed Jul 17 16:32:06 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Jul 18 14:08:28 2019 +0100
@@ -145,6 +145,28 @@
with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast
qed

+lemma tendsto_sup[tendsto_intros]:
+  fixes X :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+  assumes "(X \<longlongrightarrow> x) net" "(Y \<longlongrightarrow> y) net"
+  shows "((\<lambda>i. sup (X i) (Y i)) \<longlongrightarrow> sup x y) net"
+   unfolding sup_max eucl_sup by (intro assms tendsto_intros)
+
+lemma tendsto_inf[tendsto_intros]:
+  fixes X :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+  assumes "(X \<longlongrightarrow> x) net" "(Y \<longlongrightarrow> y) net"
+  shows "((\<lambda>i. inf (X i) (Y i)) \<longlongrightarrow> inf x y) net"
+   unfolding inf_min eucl_inf by (intro assms tendsto_intros)
+
+lemma tendsto_componentwise_max:
+  assumes f: "(f \<longlongrightarrow> l) F" and g: "(g \<longlongrightarrow> m) F"
+  shows "((\<lambda>x. (\<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)) \<longlongrightarrow> (\<Sum>i\<in>Basis. max (l \<bullet> i) (m \<bullet> i) *\<^sub>R i)) F"
+  by (intro tendsto_intros assms)
+
+lemma tendsto_componentwise_min:
+  assumes f: "(f \<longlongrightarrow> l) F" and g: "(g \<longlongrightarrow> m) F"
+  shows "((\<lambda>x. (\<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)) \<longlongrightarrow> (\<Sum>i\<in>Basis. min (l \<bullet> i) (m \<bullet> i) *\<^sub>R i)) F"
+  by (intro tendsto_intros assms)
+
lemma (in order) atLeastatMost_empty'[simp]:
"(\<not> a \<le> b) \<Longrightarrow> {a..b} = {}"
by (auto)
@@ -336,6 +358,6 @@
fixes a :: "'a::ordered_euclidean_space"
shows "ENR{a..b}"
by (auto simp: interval_cbox)
-
+
end
```
```--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Jul 17 16:32:06 2019 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jul 18 14:08:28 2019 +0100
@@ -920,6 +920,9 @@
"0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a + b) = ennreal a + ennreal b"
by (transfer fixing: a b) (auto simp: max_absorb2)

+lemma add_mono_ennreal: "x < ennreal y \<Longrightarrow> x' < ennreal y' \<Longrightarrow> x + x' < ennreal (y + y')"
+  by (metis (full_types) add_strict_mono ennreal_less_zero_iff ennreal_plus less_le not_less zero_le)
+
lemma sum_ennreal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. ennreal (f i)) = ennreal (sum f I)"
by (induction I rule: infinite_finite_induct) (auto simp: sum_nonneg)
```
```--- a/src/HOL/Library/Liminf_Limsup.thy	Wed Jul 17 16:32:06 2019 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Jul 18 14:08:28 2019 +0100
@@ -106,6 +106,12 @@
unfolding Limsup_def eventually_sequentially
by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)

+lemma mem_limsup_iff: "x \<in> limsup A \<longleftrightarrow> (\<exists>\<^sub>F n in sequentially. x \<in> A n)"
+  by (simp add: Limsup_def) (metis (mono_tags) eventually_mono not_frequently)
+
+lemma mem_liminf_iff: "x \<in> liminf A \<longleftrightarrow> (\<forall>\<^sub>F n in sequentially. x \<in> A n)"
+  by (simp add: Liminf_def) (metis (mono_tags) eventually_mono)
+
lemma Limsup_const:
assumes ntriv: "\<not> trivial_limit F"
shows "Limsup F (\<lambda>x. c) = c"```
```--- a/src/HOL/NthRoot.thy	Wed Jul 17 16:32:06 2019 +0100
+++ b/src/HOL/NthRoot.thy	Thu Jul 18 14:08:28 2019 +0100
@@ -379,6 +379,18 @@
DERIV_odd_real_root[THEN DERIV_cong]
DERIV_even_real_root[THEN DERIV_cong])

+lemma power_tendsto_0_iff [simp]:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes "n > 0"
+  shows "((\<lambda>x. f x ^ n) \<longlongrightarrow> 0) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F"
+proof -
+  have "((\<lambda>x. \<bar>root n (f x ^ n)\<bar>) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> 0) F"
+    by (auto simp: assms root_abs_power tendsto_rabs_zero_iff)
+  then have "((\<lambda>x. f x ^ n) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> 0) F"
+    by (metis tendsto_real_root abs_0 real_root_zero tendsto_rabs)
+  with assms show ?thesis
+    by (auto simp: tendsto_null_power)
+qed

subsection \<open>Square Root\<close>

@@ -392,20 +404,13 @@
unfolding sqrt_def by (rule real_root_pos_unique [OF pos2])

lemma real_sqrt_abs [simp]: "sqrt (x\<^sup>2) = \<bar>x\<bar>"
-  apply (rule real_sqrt_unique)
-   apply (rule power2_abs)
-  apply (rule abs_ge_zero)
-  done
+  by (metis power2_abs abs_ge_zero real_sqrt_unique)

lemma real_sqrt_pow2 [simp]: "0 \<le> x \<Longrightarrow> (sqrt x)\<^sup>2 = x"
unfolding sqrt_def by (rule real_root_pow_pos2 [OF pos2])

lemma real_sqrt_pow2_iff [simp]: "(sqrt x)\<^sup>2 = x \<longleftrightarrow> 0 \<le> x"
-  apply (rule iffI)
-   apply (erule subst)
-   apply (rule zero_le_power2)
-  apply (erule real_sqrt_pow2)
-  done
+  by (metis real_sqrt_pow2 zero_le_power2)

lemma real_sqrt_zero [simp]: "sqrt 0 = 0"
unfolding sqrt_def by (rule real_root_zero)```