--- 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)"
--- 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
--- 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
--- 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
--- 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)
--- 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"
--- 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)