# HG changeset patch
# User paulson
# Date 1563455324 -3600
# Node ID 8a7053892d8e5ed3eef59e7ebab0800c5bfed856
# Parent  04f492d004fab6a6e83dd014d82d42b0f6bc02f8# Parent  ebd108578ab10be3f9b0be137c78810844ac0fe5
merged

diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Thu Jul 18 12:06:42 2019 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Jul 18 14:08:44 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"
           by (simp add: mea)
         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)"
diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Jul 18 12:06:42 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Jul 18 14:08:44 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
diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Jul 18 12:06:42 2019 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Jul 18 14:08:44 2019 +0100
@@ -393,6 +393,9 @@
     and measurable_lborel2[simp]: "measurable lborel M = measurable borel M"
   by (simp_all add: lborel_def)
 
+lemma space_lebesgue_on [simp]: "space (lebesgue_on S) = S"
+  by (simp add: space_restrict_space)
+
 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"
+    by (simp add: eq)
   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
diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Jul 18 12:06:42 2019 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Jul 18 14:08:44 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
 
diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jul 18 12:06:42 2019 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jul 18 14:08:44 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)
 
diff -r 04f492d004fa -r 8a7053892d8e src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Thu Jul 18 12:06:42 2019 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Jul 18 14:08:44 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"
diff -r 04f492d004fa -r 8a7053892d8e src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Thu Jul 18 12:06:42 2019 +0200
+++ b/src/HOL/NthRoot.thy	Thu Jul 18 14:08:44 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)