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.4    by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
     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>