--- a/src/HOL/Analysis/Elementary_Topology.thy Tue Nov 05 19:15:00 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Tue Nov 05 19:55:42 2019 +0100
@@ -22,95 +22,6 @@
using openI by auto
-subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Archimedean properties and useful consequences\<close>
-
-text\<open>Bernoulli's inequality\<close>
-proposition Bernoulli_inequality:
- fixes x :: real
- assumes "-1 \<le> x"
- shows "1 + n * x \<le> (1 + x) ^ n"
-proof (induct n)
- case 0
- then show ?case by simp
-next
- case (Suc n)
- have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
- by (simp add: algebra_simps)
- also have "... = (1 + x) * (1 + n*x)"
- by (auto simp: power2_eq_square algebra_simps of_nat_Suc)
- also have "... \<le> (1 + x) ^ Suc n"
- using Suc.hyps assms mult_left_mono by fastforce
- finally show ?case .
-qed
-
-corollary Bernoulli_inequality_even:
- fixes x :: real
- assumes "even n"
- shows "1 + n * x \<le> (1 + x) ^ n"
-proof (cases "-1 \<le> x \<or> n=0")
- case True
- then show ?thesis
- by (auto simp: Bernoulli_inequality)
-next
- case False
- then have "real n \<ge> 1"
- by simp
- with False have "n * x \<le> -1"
- by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
- then have "1 + n * x \<le> 0"
- by auto
- also have "... \<le> (1 + x) ^ n"
- using assms
- using zero_le_even_power by blast
- finally show ?thesis .
-qed
-
-corollary real_arch_pow:
- fixes x :: real
- assumes x: "1 < x"
- shows "\<exists>n. y < x^n"
-proof -
- from x have x0: "x - 1 > 0"
- by arith
- from reals_Archimedean3[OF x0, rule_format, of y]
- obtain n :: nat where n: "y < real n * (x - 1)" by metis
- from x0 have x00: "x- 1 \<ge> -1" by arith
- from Bernoulli_inequality[OF x00, of n] n
- have "y < x^n" by auto
- then show ?thesis by metis
-qed
-
-corollary real_arch_pow_inv:
- fixes x y :: real
- assumes y: "y > 0"
- and x1: "x < 1"
- shows "\<exists>n. x^n < y"
-proof (cases "x > 0")
- case True
- with x1 have ix: "1 < 1/x" by (simp add: field_simps)
- from real_arch_pow[OF ix, of "1/y"]
- obtain n where n: "1/y < (1/x)^n" by blast
- then show ?thesis using y \<open>x > 0\<close>
- by (auto simp add: field_simps)
-next
- case False
- with y x1 show ?thesis
- by (metis less_le_trans not_less power_one_right)
-qed
-
-lemma forall_pos_mono:
- "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
- (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
- by (metis real_arch_inverse)
-
-lemma forall_pos_mono_1:
- "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
- (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
- apply (rule forall_pos_mono)
- apply auto
- apply (metis Suc_pred of_nat_Suc)
- done
-
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Affine transformations of intervals\<close>
lemma real_affinity_le: "0 < m \<Longrightarrow> m * x + c \<le> y \<longleftrightarrow> x \<le> inverse m * y + - (c / m)"
--- a/src/HOL/Analysis/Linear_Algebra.thy Tue Nov 05 19:15:00 2019 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Tue Nov 05 19:55:42 2019 +0100
@@ -490,96 +490,6 @@
by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
-subsection \<open>Archimedean properties and useful consequences\<close>
-
-text\<open>Bernoulli's inequality\<close>
-proposition Bernoulli_inequality:
- fixes x :: real
- assumes "-1 \<le> x"
- shows "1 + n * x \<le> (1 + x) ^ n"
-proof (induct n)
- case 0
- then show ?case by simp
-next
- case (Suc n)
- have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
- by (simp add: algebra_simps)
- also have "... = (1 + x) * (1 + n*x)"
- by (auto simp: power2_eq_square algebra_simps of_nat_Suc)
- also have "... \<le> (1 + x) ^ Suc n"
- using Suc.hyps assms mult_left_mono by fastforce
- finally show ?case .
-qed
-
-corollary Bernoulli_inequality_even:
- fixes x :: real
- assumes "even n"
- shows "1 + n * x \<le> (1 + x) ^ n"
-proof (cases "-1 \<le> x \<or> n=0")
- case True
- then show ?thesis
- by (auto simp: Bernoulli_inequality)
-next
- case False
- then have "real n \<ge> 1"
- by simp
- with False have "n * x \<le> -1"
- by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
- then have "1 + n * x \<le> 0"
- by auto
- also have "... \<le> (1 + x) ^ n"
- using assms
- using zero_le_even_power by blast
- finally show ?thesis .
-qed
-
-corollary real_arch_pow:
- fixes x :: real
- assumes x: "1 < x"
- shows "\<exists>n. y < x^n"
-proof -
- from x have x0: "x - 1 > 0"
- by arith
- from reals_Archimedean3[OF x0, rule_format, of y]
- obtain n :: nat where n: "y < real n * (x - 1)" by metis
- from x0 have x00: "x- 1 \<ge> -1" by arith
- from Bernoulli_inequality[OF x00, of n] n
- have "y < x^n" by auto
- then show ?thesis by metis
-qed
-
-corollary real_arch_pow_inv:
- fixes x y :: real
- assumes y: "y > 0"
- and x1: "x < 1"
- shows "\<exists>n. x^n < y"
-proof (cases "x > 0")
- case True
- with x1 have ix: "1 < 1/x" by (simp add: field_simps)
- from real_arch_pow[OF ix, of "1/y"]
- obtain n where n: "1/y < (1/x)^n" by blast
- then show ?thesis using y \<open>x > 0\<close>
- by (auto simp add: field_simps)
-next
- case False
- with y x1 show ?thesis
- by (metis less_le_trans not_less power_one_right)
-qed
-
-lemma forall_pos_mono:
- "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
- (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
- by (metis real_arch_inverse)
-
-lemma forall_pos_mono_1:
- "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
- (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
- apply (rule forall_pos_mono)
- apply auto
- apply (metis Suc_pred of_nat_Suc)
- done
-
-
subsection\<^marker>\<open>tag unimportant\<close> \<open>Euclidean Spaces as Typeclass\<close>
lemma independent_Basis: "independent Basis"
--- a/src/HOL/Real.thy Tue Nov 05 19:15:00 2019 +0100
+++ b/src/HOL/Real.thy Tue Nov 05 19:55:42 2019 +0100
@@ -1313,6 +1313,96 @@
by simp
+subsection \<open>Archimedean properties and useful consequences\<close>
+
+text\<open>Bernoulli's inequality\<close>
+proposition Bernoulli_inequality:
+ fixes x :: real
+ assumes "-1 \<le> x"
+ shows "1 + n * x \<le> (1 + x) ^ n"
+proof (induct n)
+ case 0
+ then show ?case by simp
+next
+ case (Suc n)
+ have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
+ by (simp add: algebra_simps)
+ also have "... = (1 + x) * (1 + n*x)"
+ by (auto simp: power2_eq_square algebra_simps)
+ also have "... \<le> (1 + x) ^ Suc n"
+ using Suc.hyps assms mult_left_mono by fastforce
+ finally show ?case .
+qed
+
+corollary Bernoulli_inequality_even:
+ fixes x :: real
+ assumes "even n"
+ shows "1 + n * x \<le> (1 + x) ^ n"
+proof (cases "-1 \<le> x \<or> n=0")
+ case True
+ then show ?thesis
+ by (auto simp: Bernoulli_inequality)
+next
+ case False
+ then have "real n \<ge> 1"
+ by simp
+ with False have "n * x \<le> -1"
+ by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
+ then have "1 + n * x \<le> 0"
+ by auto
+ also have "... \<le> (1 + x) ^ n"
+ using assms
+ using zero_le_even_power by blast
+ finally show ?thesis .
+qed
+
+corollary real_arch_pow:
+ fixes x :: real
+ assumes x: "1 < x"
+ shows "\<exists>n. y < x^n"
+proof -
+ from x have x0: "x - 1 > 0"
+ by arith
+ from reals_Archimedean3[OF x0, rule_format, of y]
+ obtain n :: nat where n: "y < real n * (x - 1)" by metis
+ from x0 have x00: "x- 1 \<ge> -1" by arith
+ from Bernoulli_inequality[OF x00, of n] n
+ have "y < x^n" by auto
+ then show ?thesis by metis
+qed
+
+corollary real_arch_pow_inv:
+ fixes x y :: real
+ assumes y: "y > 0"
+ and x1: "x < 1"
+ shows "\<exists>n. x^n < y"
+proof (cases "x > 0")
+ case True
+ with x1 have ix: "1 < 1/x" by (simp add: field_simps)
+ from real_arch_pow[OF ix, of "1/y"]
+ obtain n where n: "1/y < (1/x)^n" by blast
+ then show ?thesis using y \<open>x > 0\<close>
+ by (auto simp add: field_simps)
+next
+ case False
+ with y x1 show ?thesis
+ by (metis less_le_trans not_less power_one_right)
+qed
+
+lemma forall_pos_mono:
+ "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
+ (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
+ by (metis real_arch_inverse)
+
+lemma forall_pos_mono_1:
+ "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
+ (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
+ apply (rule forall_pos_mono)
+ apply auto
+ apply (metis Suc_pred of_nat_Suc)
+ done
+
+
subsection \<open>Floor and Ceiling Functions from the Reals to the Integers\<close>
(* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *)