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