--- a/src/HOL/Analysis/Binary_Product_Measure.thy Wed Feb 01 23:02:59 2023 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy Thu Feb 02 12:55:07 2023 +0000
@@ -340,6 +340,16 @@
by (simp add: ac_simps)
qed
+lemma (in sigma_finite_measure) times_in_null_sets1 [intro]:
+ assumes "A \<in> null_sets N" "B \<in> sets M"
+ shows "A \<times> B \<in> null_sets (N \<Otimes>\<^sub>M M)"
+ using assms by (simp add: null_sets_def emeasure_pair_measure_Times)
+
+lemma (in sigma_finite_measure) times_in_null_sets2 [intro]:
+ assumes "A \<in> sets N" "B \<in> null_sets M"
+ shows "A \<times> B \<in> null_sets (N \<Otimes>\<^sub>M M)"
+ using assms by (simp add: null_sets_def emeasure_pair_measure_Times)
+
subsection \<open>Binary products of \<open>\<sigma>\<close>-finite emeasure spaces\<close>
locale\<^marker>\<open>tag unimportant\<close> pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2
--- a/src/HOL/Analysis/Complex_Transcendental.thy Wed Feb 01 23:02:59 2023 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Feb 02 12:55:07 2023 +0000
@@ -2596,6 +2596,9 @@
fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
by (simp add: exp_of_nat_mult powr_def)
+lemma powr_nat': "(z :: complex) \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> z powr of_nat n = z ^ n"
+ by (cases "z = 0") (auto simp: powr_nat)
+
lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
using Ln_Reals_eq norm_exp_eq_Re by (auto simp: Im_Ln_eq_0 powr_def norm_complex_def)
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Feb 01 23:02:59 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Thu Feb 02 12:55:07 2023 +0000
@@ -1825,6 +1825,31 @@
shows "compact S \<Longrightarrow> compact (frontier S)"
using compact_eq_bounded_closed compact_frontier_bounded by blast
+lemma no_limpt_imp_countable:
+ assumes "\<And>z. \<not>z islimpt (X :: 'a :: {real_normed_vector, heine_borel} set)"
+ shows "countable X"
+proof -
+ have "countable (\<Union>n. cball 0 (real n) \<inter> X)"
+ proof (intro countable_UN[OF _ countable_finite])
+ fix n :: nat
+ show "finite (cball 0 (real n) \<inter> X)"
+ using assms by (intro finite_not_islimpt_in_compact) auto
+ qed auto
+ also have "(\<Union>n. cball 0 (real n)) = (UNIV :: 'a set)"
+ proof safe
+ fix z :: 'a
+ have "norm z \<ge> 0"
+ by simp
+ hence "real (nat \<lceil>norm z\<rceil>) \<ge> norm z"
+ by linarith
+ thus "z \<in> (\<Union>n. cball 0 (real n))"
+ by auto
+ qed auto
+ hence "(\<Union>n. cball 0 (real n) \<inter> X) = X"
+ by blast
+ finally show "countable X" .
+qed
+
subsection \<open>Distance from a Set\<close>
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Feb 01 23:02:59 2023 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Feb 02 12:55:07 2023 +0000
@@ -4529,36 +4529,50 @@
using \<open>x \<in> S\<close> \<open>f c = y\<close> \<open>c \<in> S\<close> by auto
qed
-lemma has_derivative_zero_connected_constant:
+lemma has_derivative_zero_connected_constant_on:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
- assumes "connected S"
- and "open S"
- and "finite k"
- and "continuous_on S f"
- and "\<forall>x\<in>(S - k). (f has_derivative (\<lambda>h. 0)) (at x within S)"
- obtains c where "\<And>x. x \<in> S \<Longrightarrow> f(x) = c"
+ assumes "connected S" "open S" "finite K" "continuous_on S f"
+ and "\<forall>x\<in>S-K. (f has_derivative (\<lambda>h. 0)) (at x within S)"
+ shows "f constant_on S"
proof (cases "S = {}")
case True
then show ?thesis
- by (metis empty_iff that)
+ by (simp add: constant_on_def)
next
case False
then obtain c where "c \<in> S"
by (metis equals0I)
then show ?thesis
- by (metis has_derivative_zero_unique_strong_connected assms that)
-qed
+ unfolding constant_on_def
+ by (metis has_derivative_zero_unique_strong_connected assms )
+qed
+
+lemma DERIV_zero_connected_constant_on:
+ fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
+ assumes *: "connected S" "open S" "finite K" "continuous_on S f"
+ and 0: "\<forall>x\<in>S-K. DERIV f x :> 0"
+ shows "f constant_on S"
+ using has_derivative_zero_connected_constant_on [OF *] 0
+ by (metis has_derivative_at_withinI has_field_derivative_def lambda_zero)
lemma DERIV_zero_connected_constant:
fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
- assumes "connected S"
- and "open S"
- and "finite K"
- and "continuous_on S f"
- and "\<forall>x\<in>(S - K). DERIV f x :> 0"
+ assumes "connected S" and "open S" and "finite K" and "continuous_on S f"
+ and "\<forall>x\<in>S-K. DERIV f x :> 0"
obtains c where "\<And>x. x \<in> S \<Longrightarrow> f(x) = c"
- using has_derivative_zero_connected_constant [OF assms(1-4)] assms
- by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def)
+ by (metis DERIV_zero_connected_constant_on [OF assms] constant_on_def)
+
+lemma has_field_derivative_0_imp_constant_on:
+ fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
+ assumes "\<And>z. z \<in> S \<Longrightarrow> (f has_field_derivative 0) (at z)" and S: "connected S" "open S"
+ shows "f constant_on S"
+proof -
+ have *: "continuous_on S f"
+ using assms(1) by (intro DERIV_continuous_on[of _ _ "\<lambda>_. 0"])
+ (use assms in \<open>auto simp: at_within_open[of _ S]\<close>)
+ show ?thesis
+ using DERIV_zero_connected_constant_on[OF S finite.emptyI *] assms(1) by blast
+qed
subsection \<open>Integrating characteristic function of an interval\<close>
--- a/src/HOL/Analysis/Measure_Space.thy Wed Feb 01 23:02:59 2023 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Thu Feb 02 12:55:07 2023 +0000
@@ -1046,6 +1046,17 @@
using Int_absorb1[OF sets.sets_into_space, of N M]
by (subst AE_iff_null) (auto simp: Int_def[symmetric])
+lemma ae_filter_eq_bot_iff: "ae_filter M = bot \<longleftrightarrow> emeasure M (space M) = 0"
+proof -
+ have "ae_filter M = bot \<longleftrightarrow> (AE x in M. False)"
+ using trivial_limit_def by blast
+ also have "\<dots> \<longleftrightarrow> space M \<in> null_sets M"
+ by (simp add: AE_iff_null_sets eventually_ae_filter)
+ also have "\<dots> \<longleftrightarrow> emeasure M (space M) = 0"
+ by auto
+ finally show ?thesis .
+qed
+
lemma AE_not_in:
"N \<in> null_sets M \<Longrightarrow> AE x in M. x \<notin> N"
by (metis AE_iff_null_sets null_setsD2)
@@ -1060,12 +1071,9 @@
using assms unfolding eventually_ae_filter by auto
lemma AE_E2:
- assumes "AE x in M. P x" "{x\<in>space M. P x} \<in> sets M"
- shows "emeasure M {x\<in>space M. \<not> P x} = 0" (is "emeasure M ?P = 0")
-proof -
- have "{x\<in>space M. \<not> P x} = space M - {x\<in>space M. P x}" by auto
- with AE_iff_null[of M P] assms show ?thesis by auto
-qed
+ assumes "AE x in M. P x"
+ shows "emeasure M {x\<in>space M. \<not> P x} = 0"
+ by (metis (mono_tags, lifting) AE_iff_null assms emeasure_notin_sets null_setsD1)
lemma AE_E3:
assumes "AE x in M. P x"
@@ -1080,25 +1088,7 @@
lemma AE_mp[elim!]:
assumes AE_P: "AE x in M. P x" and AE_imp: "AE x in M. P x \<longrightarrow> Q x"
shows "AE x in M. Q x"
-proof -
- from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A"
- and A: "A \<in> sets M" "emeasure M A = 0"
- by (auto elim!: AE_E)
-
- from AE_imp obtain B where imp: "{x\<in>space M. P x \<and> \<not> Q x} \<subseteq> B"
- and B: "B \<in> sets M" "emeasure M B = 0"
- by (auto elim!: AE_E)
-
- show ?thesis
- proof (intro AE_I)
- have "emeasure M (A \<union> B) \<le> 0"
- using emeasure_subadditive[of A M B] A B by auto
- then show "A \<union> B \<in> sets M" "emeasure M (A \<union> B) = 0"
- using A B by auto
- show "{x\<in>space M. \<not> Q x} \<subseteq> A \<union> B"
- using P imp by auto
- qed
-qed
+ using assms by (fact eventually_rev_mp)
text \<open>The next lemma is convenient to combine with a lemma whose conclusion is of the
form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \<open>[symmetric]\<close> variant,
--- a/src/HOL/Rat.thy Wed Feb 01 23:02:59 2023 +0100
+++ b/src/HOL/Rat.thy Thu Feb 02 12:55:07 2023 +0000
@@ -883,6 +883,21 @@
lemma Rats_infinite: "\<not> finite \<rat>"
by (auto dest!: finite_imageD simp: inj_on_def infinite_UNIV_char_0 Rats_def)
+lemma Rats_add_iff: "a \<in> \<rat> \<or> b \<in> \<rat> \<Longrightarrow> a+b \<in> \<rat> \<longleftrightarrow> a \<in> \<rat> \<and> b \<in> \<rat>"
+ by (metis Rats_add Rats_diff add_diff_cancel add_diff_cancel_left')
+
+lemma Rats_diff_iff: "a \<in> \<rat> \<or> b \<in> \<rat> \<Longrightarrow> a-b \<in> \<rat> \<longleftrightarrow> a \<in> \<rat> \<and> b \<in> \<rat>"
+ by (metis Rats_add_iff diff_add_cancel)
+
+lemma Rats_mult_iff: "a \<in> \<rat>-{0} \<or> b \<in> \<rat>-{0} \<Longrightarrow> a*b \<in> \<rat> \<longleftrightarrow> a \<in> \<rat> \<and> b \<in> \<rat>"
+ by (metis Diff_iff Rats_divide Rats_mult insertI1 mult.commute nonzero_divide_eq_eq)
+
+lemma Rats_inverse_iff [simp]: "inverse a \<in> \<rat> \<longleftrightarrow> a \<in> \<rat>"
+ using Rats_inverse by force
+
+lemma Rats_divide_iff: "a \<in> \<rat>-{0} \<or> b \<in> \<rat>-{0} \<Longrightarrow> a/b \<in> \<rat> \<longleftrightarrow> a \<in> \<rat> \<and> b \<in> \<rat>"
+ by (metis Rats_divide Rats_mult_iff divide_eq_0_iff divide_inverse nonzero_mult_div_cancel_right)
+
subsection \<open>Implementation of rational numbers as pairs of integers\<close>