# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1675342507 0
# Node ID 6d2ca97a8f466e835aab327381101c31f3a8cd32
# Parent  4aff4a84b8af9e65f8dc0ac1a1c3cafc02f9b4ec
More of Manuel's material, and some changes

diff -r 4aff4a84b8af -r 6d2ca97a8f46 src/HOL/Analysis/Binary_Product_Measure.thy
--- 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
diff -r 4aff4a84b8af -r 6d2ca97a8f46 src/HOL/Analysis/Complex_Transcendental.thy
--- 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)
 
diff -r 4aff4a84b8af -r 6d2ca97a8f46 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- 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>
 
diff -r 4aff4a84b8af -r 6d2ca97a8f46 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- 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>
diff -r 4aff4a84b8af -r 6d2ca97a8f46 src/HOL/Analysis/Measure_Space.thy
--- 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,
diff -r 4aff4a84b8af -r 6d2ca97a8f46 src/HOL/Rat.thy
--- 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>