src/HOL/Analysis/Inner_Product.thy
changeset 66486 ffaaa83543b2
parent 65513 587433a18053
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Analysis/Inner_Product.thy	Tue Aug 22 14:34:26 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Tue Aug 22 21:36:48 2017 +0200
     1.3 @@ -305,6 +305,56 @@
     1.4    unfolding inner_complex_def by simp
     1.5  
     1.6  
     1.7 +lemma dot_square_norm: "inner x x = (norm x)\<^sup>2"
     1.8 +  by (simp only: power2_norm_eq_inner) (* TODO: move? *)
     1.9 +
    1.10 +lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> inner x x = a\<^sup>2"
    1.11 +  by (auto simp add: norm_eq_sqrt_inner)
    1.12 +
    1.13 +lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> inner x x \<le> a\<^sup>2"
    1.14 +  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
    1.15 +  using norm_ge_zero[of x]
    1.16 +  apply arith
    1.17 +  done
    1.18 +
    1.19 +lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> inner x x \<ge> a\<^sup>2"
    1.20 +  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
    1.21 +  using norm_ge_zero[of x]
    1.22 +  apply arith
    1.23 +  done
    1.24 +
    1.25 +lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> inner x x < a\<^sup>2"
    1.26 +  by (metis not_le norm_ge_square)
    1.27 +
    1.28 +lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> inner x x > a\<^sup>2"
    1.29 +  by (metis norm_le_square not_less)
    1.30 +
    1.31 +text\<open>Dot product in terms of the norm rather than conversely.\<close>
    1.32 +
    1.33 +lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
    1.34 +  inner_scaleR_left inner_scaleR_right
    1.35 +
    1.36 +lemma dot_norm: "inner x y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
    1.37 +  by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
    1.38 +
    1.39 +lemma dot_norm_neg: "inner x y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
    1.40 +  by (simp only: power2_norm_eq_inner inner_simps inner_commute)
    1.41 +    (auto simp add: algebra_simps)
    1.42 +
    1.43 +lemma of_real_inner_1 [simp]: 
    1.44 +  "inner (of_real x) (1 :: 'a :: {real_inner, real_normed_algebra_1}) = x"
    1.45 +  by (simp add: of_real_def dot_square_norm)
    1.46 +  
    1.47 +lemma summable_of_real_iff: 
    1.48 +  "summable (\<lambda>x. of_real (f x) :: 'a :: {real_normed_algebra_1,real_inner}) \<longleftrightarrow> summable f"
    1.49 +proof
    1.50 +  assume *: "summable (\<lambda>x. of_real (f x) :: 'a)"
    1.51 +  interpret bounded_linear "\<lambda>x::'a. inner x 1"
    1.52 +    by (rule bounded_linear_inner_left)
    1.53 +  from summable [OF *] show "summable f" by simp
    1.54 +qed (auto intro: summable_of_real)
    1.55 +
    1.56 +
    1.57  subsection \<open>Gradient derivative\<close>
    1.58  
    1.59  definition