author paulson Thu, 19 Sep 2019 12:36:15 +0100 changeset 70724 65371451fde8 parent 70723 4e39d87c9737 child 70725 e19c18b4a0dd
A few more simple results
 src/HOL/Analysis/Change_Of_Vars.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Complex_Transcendental.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Elementary_Metric_Spaces.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Elementary_Normed_Spaces.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Elementary_Topology.thy file | annotate | diff | comparison | revisions src/HOL/Library/Extended_Real.thy file | annotate | diff | comparison | revisions src/HOL/Power.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Analysis/Change_Of_Vars.thy	Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Sep 19 12:36:15 2019 +0100
@@ -9,41 +9,6 @@

begin

-subsection \<open>Orthogonal Transformation of Balls\<close>
-
-lemma image_orthogonal_transformation_ball:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
-  assumes "orthogonal_transformation f"
-  shows "f ` ball x r = ball (f x) r"
-proof (intro equalityI subsetI)
-  fix y assume "y \<in> f ` ball x r"
-  with assms show "y \<in> ball (f x) r"
-    by (auto simp: orthogonal_transformation_isometry)
-next
-  fix y assume y: "y \<in> ball (f x) r"
-  then obtain z where z: "y = f z"
-    using assms orthogonal_transformation_surj by blast
-  with y assms show "y \<in> f ` ball x r"
-    by (auto simp: orthogonal_transformation_isometry)
-qed
-
-lemma  image_orthogonal_transformation_cball:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
-  assumes "orthogonal_transformation f"
-  shows "f ` cball x r = cball (f x) r"
-proof (intro equalityI subsetI)
-  fix y assume "y \<in> f ` cball x r"
-  with assms show "y \<in> cball (f x) r"
-    by (auto simp: orthogonal_transformation_isometry)
-next
-  fix y assume y: "y \<in> cball (f x) r"
-  then obtain z where z: "y = f z"
-    using assms orthogonal_transformation_surj by blast
-  with y assms show "y \<in> f ` cball x r"
-    by (auto simp: orthogonal_transformation_isometry)
-qed
-
-
subsection \<open>Measurable Shear and Stretch\<close>

proposition```
```--- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Sep 19 12:36:15 2019 +0100
@@ -2568,12 +2568,23 @@
apply (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide)
done

-lemma lim_ln_over_n: "((\<lambda>n. ln(real_of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
+lemma lim_ln_over_n [tendsto_intros]: "((\<lambda>n. ln(real_of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]]
apply (subst filterlim_sequentially_Suc [symmetric])
done

+lemma lim_log_over_n [tendsto_intros]:
+  "(\<lambda>n. log k n/n) \<longlonglongrightarrow> 0"
+proof -
+  have *: "log k n/n = (1/ln k) * (ln n / n)" for n
+    unfolding log_def by auto
+  have "(\<lambda>n. (1/ln k) * (ln n / n)) \<longlonglongrightarrow> (1/ln k) * 0"
+    by (intro tendsto_intros)
+  then show ?thesis
+    unfolding * by auto
+qed
+
lemma lim_1_over_complex_power:
assumes "0 < Re s"
shows "(\<lambda>n. 1 / of_nat n powr s) \<longlonglongrightarrow> 0"```
```--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu Sep 19 12:36:15 2019 +0100
@@ -2000,6 +2000,11 @@
lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
by (auto intro!: antisym infdist_nonneg infdist_le2)

+lemma infdist_Un_min:
+  assumes "A \<noteq> {}" "B \<noteq> {}"
+  shows "infdist x (A \<union> B) = min (infdist x A) (infdist x B)"
+using assms by (simp add: infdist_def cINF_union inf_real_def)
+
lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
proof (cases "A = {}")
case True
@@ -2041,6 +2046,9 @@
finally show ?thesis by simp
qed

+lemma infdist_triangle_abs: "\<bar>infdist x A - infdist y A\<bar> \<le> dist x y"
+  by (metis (full_types) abs_diff_le_iff diff_le_eq dist_commute infdist_triangle)
+
lemma in_closure_iff_infdist_zero:
assumes "A \<noteq> {}"
shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
@@ -3236,6 +3244,15 @@
by (auto simp: setdist_def infdist_def)
qed

+lemma infdist_mono:
+  assumes "A \<subseteq> B" "A \<noteq> {}"
+  shows "infdist x B \<le> infdist x A"
+  by (simp add: assms infdist_eq_setdist setdist_subset_right)
+
+lemma infdist_singleton [simp]:
+  "infdist x {y} = dist x y"
+
proposition setdist_attains_inf:
assumes "compact B" "B \<noteq> {}"
obtains y where "y \<in> B" "setdist A B = infdist y A"```
```--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Thu Sep 19 12:36:15 2019 +0100
@@ -9,17 +9,13 @@
theory Elementary_Normed_Spaces
imports
"HOL-Library.FuncSet"
-  Elementary_Metric_Spaces Linear_Algebra
+  Elementary_Metric_Spaces Cartesian_Space
Connected
begin
+subsection \<open>Orthogonal Transformation of Balls\<close>

subsection\<^marker>\<open>tag unimportant\<close> \<open>Various Lemmas Combining Imports\<close>

-lemma countable_PiE:
-  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)"
-  by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
-
-
lemma open_sums:
fixes T :: "('b::real_normed_vector) set"
assumes "open S \<or> open T"
@@ -53,6 +49,38 @@
qed
qed

+lemma image_orthogonal_transformation_ball:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+  assumes "orthogonal_transformation f"
+  shows "f ` ball x r = ball (f x) r"
+proof (intro equalityI subsetI)
+  fix y assume "y \<in> f ` ball x r"
+  with assms show "y \<in> ball (f x) r"
+    by (auto simp: orthogonal_transformation_isometry)
+next
+  fix y assume y: "y \<in> ball (f x) r"
+  then obtain z where z: "y = f z"
+    using assms orthogonal_transformation_surj by blast
+  with y assms show "y \<in> f ` ball x r"
+    by (auto simp: orthogonal_transformation_isometry)
+qed
+
+lemma image_orthogonal_transformation_cball:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+  assumes "orthogonal_transformation f"
+  shows "f ` cball x r = cball (f x) r"
+proof (intro equalityI subsetI)
+  fix y assume "y \<in> f ` cball x r"
+  with assms show "y \<in> cball (f x) r"
+    by (auto simp: orthogonal_transformation_isometry)
+next
+  fix y assume y: "y \<in> cball (f x) r"
+  then obtain z where z: "y = f z"
+    using assms orthogonal_transformation_surj by blast
+  with y assms show "y \<in> f ` cball x r"
+    by (auto simp: orthogonal_transformation_isometry)
+qed
+

subsection \<open>Support\<close>
```
```--- a/src/HOL/Analysis/Elementary_Topology.thy	Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Thu Sep 19 12:36:15 2019 +0100
@@ -2479,6 +2479,14 @@
unfolding homeomorphism_def
by (intro conjI ballI continuous_on_compose) (auto simp: image_iff)

+lemma homeomorphism_cong:
+  "homeomorphism X' Y' f' g'"
+    if "homeomorphism X Y f g" "X' = X" "Y' = Y" "\<And>x. x \<in> X \<Longrightarrow> f' x = f x" "\<And>y. y \<in> Y \<Longrightarrow> g' y = g y"
+  using that by (auto simp add: homeomorphism_def)
+
+lemma homeomorphism_empty [simp]:
+  "homeomorphism {} {} f g"
+  unfolding homeomorphism_def by auto

lemma homeomorphism_symD: "homeomorphism S t f g \<Longrightarrow> homeomorphism t S g f"
```--- a/src/HOL/Library/Extended_Real.thy	Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Sep 19 12:36:15 2019 +0100
@@ -1725,13 +1725,44 @@
by (cases a b c rule: ereal3_cases)
(auto simp: field_simps zero_less_mult_iff)

-lemma ereal_inverse_real: "\<bar>z\<bar> \<noteq> \<infinity> \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> ereal (inverse (real_of_ereal z)) = inverse z"
-  by (cases z) simp_all
+lemma ereal_inverse_real [simp]: "\<bar>z\<bar> \<noteq> \<infinity> \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> ereal (inverse (real_of_ereal z)) = inverse z"
+  by auto

lemma ereal_inverse_mult:
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse (a * (b::ereal)) = inverse a * inverse b"
by (cases a; cases b) auto

+lemma inverse_eq_infinity_iff_eq_zero [simp]:
+  "1/(x::ereal) = \<infinity> \<longleftrightarrow> x = 0"
+
+lemma ereal_distrib_left:
+  fixes a b c :: ereal
+  assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>"
+    and "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>"
+    and "\<bar>c\<bar> \<noteq> \<infinity>"
+  shows "c * (a + b) = c * a + c * b"
+using assms
+by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+
+lemma ereal_distrib_minus_left:
+  fixes a b c :: ereal
+  assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>"
+    and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
+    and "\<bar>c\<bar> \<noteq> \<infinity>"
+  shows "c * (a - b) = c * a - c * b"
+using assms
+by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+
+lemma ereal_distrib_minus_right:
+  fixes a b c :: ereal
+  assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>"
+    and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
+    and "\<bar>c\<bar> \<noteq> \<infinity>"
+  shows "(a - b) * c = a * c - b * c"
+using assms
+by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+

subsection "Complete lattice"

@@ -4116,6 +4147,11 @@
by (force simp: continuous_on_def mult_ac)
qed (insert assms, auto simp: mono_def ereal_mult_right_mono)

+lemma Liminf_ereal_mult_left:
+  assumes "F \<noteq> bot" "(c::real) \<ge> 0"
+    shows "Liminf F (\<lambda>n. ereal c * f n) = ereal c * Liminf F f"
+using Liminf_ereal_mult_right[OF assms] by (subst (1 2) mult.commute)
+
lemma Limsup_ereal_mult_left:
assumes "F \<noteq> bot" "(c::real) \<ge> 0"
shows   "Limsup F (\<lambda>n. ereal c * f n) = ereal c * Limsup F f"```
```--- a/src/HOL/Power.thy	Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Power.thy	Thu Sep 19 12:36:15 2019 +0100
@@ -54,12 +54,6 @@
lemma power_mult: "a ^ (m * n) = (a ^ m) ^ n"

-lemma power2_eq_square: "a\<^sup>2 = a * a"
-
-lemma power3_eq_cube: "a ^ 3 = a * a * a"
-  by (simp add: numeral_3_eq_3 mult.assoc)
-
lemma power_even_eq: "a ^ (2 * n) = (a ^ n)\<^sup>2"
by (subst mult.commute) (simp add: power_mult)

@@ -73,6 +67,15 @@