src/HOL/Analysis/Linear_Algebra.thy
 changeset 69516 09bb8f470959 parent 69513 42e08052dae8 child 69517 dc20f278e8f3
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 22:54:29 2018 +0100
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 23:38:55 2018 +0100
1.3 @@ -310,51 +310,6 @@
1.5
1.6
1.7 -subsection%unimportant \<open>Interlude: Some properties of real sets\<close>
1.8 -
1.9 -lemma seq_mono_lemma:
1.10 -  assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
1.11 -    and "\<forall>n \<ge> m. e n \<le> e m"
1.12 -  shows "\<forall>n \<ge> m. d n < e m"
1.13 -  using assms by force
1.14 -
1.15 -lemma infinite_enumerate:
1.16 -  assumes fS: "infinite S"
1.17 -  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. r n \<in> S)"
1.18 -  unfolding strict_mono_def
1.19 -  using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
1.20 -
1.21 -lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
1.22 -  apply auto
1.23 -  apply (rule_tac x="d/2" in exI)
1.24 -  apply auto
1.25 -  done
1.26 -
1.27 -lemma approachable_lt_le2:  \<comment> \<open>like the above, but pushes aside an extra formula\<close>
1.28 -    "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
1.29 -  apply auto
1.30 -  apply (rule_tac x="d/2" in exI, auto)
1.31 -  done
1.32 -
1.33 -lemma triangle_lemma:
1.34 -  fixes x y z :: real
1.35 -  assumes x: "0 \<le> x"
1.36 -    and y: "0 \<le> y"
1.37 -    and z: "0 \<le> z"
1.38 -    and xy: "x\<^sup>2 \<le> y\<^sup>2 + z\<^sup>2"
1.39 -  shows "x \<le> y + z"
1.40 -proof -
1.41 -  have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2"
1.42 -    using z y by simp
1.43 -  with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2"
1.44 -    by (simp add: power2_eq_square field_simps)
1.45 -  from y z have yz: "y + z \<ge> 0"
1.46 -    by arith
1.47 -  from power2_le_imp_le[OF th yz] show ?thesis .
1.48 -qed
1.49 -
1.50 -
1.51 -
1.52  subsection \<open>Archimedean properties and useful consequences\<close>
1.53
1.54  text\<open>Bernoulli's inequality\<close>
```