src/HOL/Analysis/Linear_Algebra.thy
 changeset 66486 ffaaa83543b2 parent 66453 cc19f7ca2ed6 child 66503 7685861f337d
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Aug 22 14:34:26 2017 +0200
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue Aug 22 21:36:48 2017 +0200
1.3 @@ -1397,43 +1397,6 @@
1.4  lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> x \<bullet> x = 1"
1.6
1.7 -text\<open>Squaring equations and inequalities involving norms.\<close>
1.8 -
1.9 -lemma dot_square_norm: "x \<bullet> x = (norm x)\<^sup>2"
1.10 -  by (simp only: power2_norm_eq_inner) (* TODO: move? *)
1.11 -
1.12 -lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x = a\<^sup>2"
1.13 -  by (auto simp add: norm_eq_sqrt_inner)
1.14 -
1.15 -lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x \<le> a\<^sup>2"
1.16 -  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
1.17 -  using norm_ge_zero[of x]
1.18 -  apply arith
1.19 -  done
1.20 -
1.21 -lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> x \<bullet> x \<ge> a\<^sup>2"
1.22 -  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
1.23 -  using norm_ge_zero[of x]
1.24 -  apply arith
1.25 -  done
1.26 -
1.27 -lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
1.28 -  by (metis not_le norm_ge_square)
1.29 -
1.30 -lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
1.31 -  by (metis norm_le_square not_less)
1.32 -
1.33 -text\<open>Dot product in terms of the norm rather than conversely.\<close>
1.34 -