author  huffman 
Sat, 21 Feb 2009 15:39:59 0800  
changeset 30045  b8ddd7667eed 
parent 30041  9becd197a40e 
child 30066  9223483cc927 
permissions  rwrr 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1 
(* Title: Library/Euclidean_Space 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

2 
ID: $Id: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

3 
Author: Amine Chaieb, University of Cambridge 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

4 
*) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

5 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

6 
header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

7 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

8 
theory Euclidean_Space 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

9 
imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

10 
Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type 
30045  11 
Inner_Product 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

12 
uses ("normarith.ML") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

13 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

14 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

15 
text{* Some common special cases.*} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

16 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

17 
lemma forall_1: "(\<forall>(i::'a::{order,one}). 1 <= i \<and> i <= 1 > P i) \<longleftrightarrow> P 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

18 
by (metis order_eq_iff) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

19 
lemma forall_dimindex_1: "(\<forall>i \<in> {1..dimindex(UNIV:: 1 set)}. P i) \<longleftrightarrow> P 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

20 
by (simp add: dimindex_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

21 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

22 
lemma forall_2: "(\<forall>(i::nat). 1 <= i \<and> i <= 2 > P i) \<longleftrightarrow> P 1 \<and> P 2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

23 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

24 
have "\<And>i::nat. 1 <= i \<and> i <= 2 \<longleftrightarrow> i = 1 \<or> i = 2" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

25 
thus ?thesis by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

26 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

27 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

28 
lemma forall_3: "(\<forall>(i::nat). 1 <= i \<and> i <= 3 > P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

29 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

30 
have "\<And>i::nat. 1 <= i \<and> i <= 3 \<longleftrightarrow> i = 1 \<or> i = 2 \<or> i = 3" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

31 
thus ?thesis by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

32 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

33 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

34 
lemma setsum_singleton[simp]: "setsum f {x} = f x" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

35 
lemma setsum_1: "setsum f {(1::'a::{order,one})..1} = f 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

36 
by (simp add: atLeastAtMost_singleton) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

37 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

38 
lemma setsum_2: "setsum f {1::nat..2} = f 1 + f 2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

39 
by (simp add: nat_number atLeastAtMostSuc_conv add_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

40 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

41 
lemma setsum_3: "setsum f {1::nat..3} = f 1 + f 2 + f 3" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

42 
by (simp add: nat_number atLeastAtMostSuc_conv add_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

43 

29906  44 
subsection{* Basic componentwise operations on vectors. *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

45 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

46 
instantiation "^" :: (plus,type) plus 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

47 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

48 
definition vector_add_def : "op + \<equiv> (\<lambda> x y. (\<chi> i. (x$i) + (y$i)))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

49 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

50 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

51 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

52 
instantiation "^" :: (times,type) times 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

53 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

54 
definition vector_mult_def : "op * \<equiv> (\<lambda> x y. (\<chi> i. (x$i) * (y$i)))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

55 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

56 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

57 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

58 
instantiation "^" :: (minus,type) minus begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

59 
definition vector_minus_def : "op  \<equiv> (\<lambda> x y. (\<chi> i. (x$i)  (y$i)))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

60 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

61 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

62 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

63 
instantiation "^" :: (uminus,type) uminus begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

64 
definition vector_uminus_def : "uminus \<equiv> (\<lambda> x. (\<chi> i.  (x$i)))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

65 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

66 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

67 
instantiation "^" :: (zero,type) zero begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

68 
definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

69 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

70 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

71 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

72 
instantiation "^" :: (one,type) one begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

73 
definition vector_one_def : "1 \<equiv> (\<chi> i. 1)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

74 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

75 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

76 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

77 
instantiation "^" :: (ord,type) ord 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

78 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

79 
definition vector_less_eq_def: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

80 
"less_eq (x :: 'a ^'b) y = (ALL i : {1 .. dimindex (UNIV :: 'b set)}. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

81 
x$i <= y$i)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

82 
definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i : {1 .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

83 
dimindex (UNIV :: 'b set)}. x$i < y$i)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

84 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

85 
instance by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

86 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

87 

30039  88 
instantiation "^" :: (scaleR, type) scaleR 
89 
begin 

90 
definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))" 

91 
instance .. 

92 
end 

93 

94 
text{* Also the scalarvector multiplication. *} 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

95 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

96 
definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

97 
where "c *s x = (\<chi> i. c * (x$i))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

98 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

99 
text{* Constant Vectors *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

100 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

101 
definition "vec x = (\<chi> i. x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

102 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

103 
text{* Dot products. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

104 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

105 
definition dot :: "'a::{comm_monoid_add, times} ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

106 
"x \<bullet> y = setsum (\<lambda>i. x$i * y$i) {1 .. dimindex (UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

107 
lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \<bullet> y = (x$1) * (y$1)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

108 
by (simp add: dot_def dimindex_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

109 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

110 
lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

111 
by (simp add: dot_def dimindex_def nat_number) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

112 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

113 
lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2) + (x$3) * (y$3)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

114 
by (simp add: dot_def dimindex_def nat_number) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

115 

29906  116 
subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

117 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

118 
lemmas Cart_lambda_beta' = Cart_lambda_beta[rule_format] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

119 
method_setup vector = {* 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

120 
let 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

121 
val ss1 = HOL_basic_ss addsimps [@{thm dot_def}, @{thm setsum_addf} RS sym, 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

122 
@{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

123 
@{thm setsum_left_distrib}, @{thm setsum_negf} RS sym] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

124 
val ss2 = @{simpset} addsimps 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

125 
[@{thm vector_add_def}, @{thm vector_mult_def}, 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

126 
@{thm vector_minus_def}, @{thm vector_uminus_def}, 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

127 
@{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def}, 
30039  128 
@{thm vector_scaleR_def}, 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

129 
@{thm Cart_lambda_beta'}, @{thm vector_scalar_mult_def}] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

130 
fun vector_arith_tac ths = 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

131 
simp_tac ss1 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

132 
THEN' (fn i => rtac @{thm setsum_cong2} i 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

133 
ORELSE rtac @{thm setsum_0'} i 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

134 
ORELSE simp_tac (HOL_basic_ss addsimps [@{thm "Cart_eq"}]) i) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

135 
(* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

136 
THEN' asm_full_simp_tac (ss2 addsimps ths) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

137 
in 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

138 
Method.thms_args (Method.SIMPLE_METHOD' o vector_arith_tac) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

139 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

140 
*} "Lifts trivial vector statements to real arith statements" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

141 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

142 
lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

143 
lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

144 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

145 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

146 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

147 
text{* Obvious "componentpushing". *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

148 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

149 
lemma vec_component: " i \<in> {1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (vec x :: 'a ^ 'n)$i = x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

150 
by (vector vec_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

151 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

152 
lemma vector_add_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

153 
fixes x y :: "'a::{plus} ^ 'n" assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

154 
shows "(x + y)$i = x$i + y$i" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

155 
using i by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

156 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

157 
lemma vector_minus_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

158 
fixes x y :: "'a::{minus} ^ 'n" assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

159 
shows "(x  y)$i = x$i  y$i" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

160 
using i by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

161 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

162 
lemma vector_mult_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

163 
fixes x y :: "'a::{times} ^ 'n" assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

164 
shows "(x * y)$i = x$i * y$i" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

165 
using i by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

166 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

167 
lemma vector_smult_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

168 
fixes y :: "'a::{times} ^ 'n" assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

169 
shows "(c *s y)$i = c * (y$i)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

170 
using i by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

171 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

172 
lemma vector_uminus_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

173 
fixes x :: "'a::{uminus} ^ 'n" assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

174 
shows "( x)$i =  (x$i)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

175 
using i by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

176 

30039  177 
lemma vector_scaleR_component: 
178 
fixes x :: "'a::scaleR ^ 'n" 

179 
assumes i: "i \<in> {1 .. dimindex(UNIV :: 'n set)}" 

180 
shows "(scaleR r x)$i = scaleR r (x$i)" 

181 
using i by vector 

182 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

183 
lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

184 

30039  185 
lemmas vector_component = 
186 
vec_component vector_add_component vector_mult_component 

187 
vector_smult_component vector_minus_component vector_uminus_component 

188 
vector_scaleR_component cond_component 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

189 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

190 
subsection {* Some frequently useful arithmetic lemmas over vectors. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

191 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

192 
instance "^" :: (semigroup_add,type) semigroup_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

193 
apply (intro_classes) by (vector add_assoc) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

194 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

195 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

196 
instance "^" :: (monoid_add,type) monoid_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

197 
apply (intro_classes) by vector+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

198 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

199 
instance "^" :: (group_add,type) group_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

200 
apply (intro_classes) by (vector algebra_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

201 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

202 
instance "^" :: (ab_semigroup_add,type) ab_semigroup_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

203 
apply (intro_classes) by (vector add_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

204 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

205 
instance "^" :: (comm_monoid_add,type) comm_monoid_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

206 
apply (intro_classes) by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

207 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

208 
instance "^" :: (ab_group_add,type) ab_group_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

209 
apply (intro_classes) by vector+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

210 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

211 
instance "^" :: (cancel_semigroup_add,type) cancel_semigroup_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

212 
apply (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

213 
by (vector Cart_eq)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

214 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

215 
instance "^" :: (cancel_ab_semigroup_add,type) cancel_ab_semigroup_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

216 
apply (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

217 
by (vector Cart_eq) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

218 

30039  219 
instance "^" :: (real_vector, type) real_vector 
220 
by default (vector scaleR_left_distrib scaleR_right_distrib)+ 

221 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

222 
instance "^" :: (semigroup_mult,type) semigroup_mult 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

223 
apply (intro_classes) by (vector mult_assoc) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

224 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

225 
instance "^" :: (monoid_mult,type) monoid_mult 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

226 
apply (intro_classes) by vector+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

227 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

228 
instance "^" :: (ab_semigroup_mult,type) ab_semigroup_mult 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

229 
apply (intro_classes) by (vector mult_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

230 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

231 
instance "^" :: (ab_semigroup_idem_mult,type) ab_semigroup_idem_mult 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

232 
apply (intro_classes) by (vector mult_idem) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

233 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

234 
instance "^" :: (comm_monoid_mult,type) comm_monoid_mult 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

235 
apply (intro_classes) by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

236 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

237 
fun vector_power :: "('a::{one,times} ^'n) \<Rightarrow> nat \<Rightarrow> 'a^'n" where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

238 
"vector_power x 0 = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

239 
 "vector_power x (Suc n) = x * vector_power x n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

240 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

241 
instantiation "^" :: (recpower,type) recpower 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

242 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

243 
definition vec_power_def: "op ^ \<equiv> vector_power" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

244 
instance 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

245 
apply (intro_classes) by (simp_all add: vec_power_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

246 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

247 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

248 
instance "^" :: (semiring,type) semiring 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

249 
apply (intro_classes) by (vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

250 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

251 
instance "^" :: (semiring_0,type) semiring_0 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

252 
apply (intro_classes) by (vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

253 
instance "^" :: (semiring_1,type) semiring_1 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

254 
apply (intro_classes) apply vector using dimindex_ge_1 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

255 
instance "^" :: (comm_semiring,type) comm_semiring 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

256 
apply (intro_classes) by (vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

257 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

258 
instance "^" :: (comm_semiring_0,type) comm_semiring_0 by (intro_classes) 
29905  259 
instance "^" :: (cancel_comm_monoid_add, type) cancel_comm_monoid_add .. 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

260 
instance "^" :: (semiring_0_cancel,type) semiring_0_cancel by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

261 
instance "^" :: (comm_semiring_0_cancel,type) comm_semiring_0_cancel by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

262 
instance "^" :: (ring,type) ring by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

263 
instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

264 
instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes) 
30039  265 

266 
instance "^" :: (ring_1,type) ring_1 .. 

267 

268 
instance "^" :: (real_algebra,type) real_algebra 

269 
apply intro_classes 

270 
apply (simp_all add: vector_scaleR_def ring_simps) 

271 
apply vector 

272 
apply vector 

273 
done 

274 

275 
instance "^" :: (real_algebra_1,type) real_algebra_1 .. 

276 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

277 
lemma of_nat_index: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

278 
"i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

279 
apply (induct n) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

280 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

281 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

282 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

283 
lemma zero_index[simp]: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

284 
"i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (0 :: 'a::zero ^'n)$i = 0" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

285 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

286 
lemma one_index[simp]: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

287 
"i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (1 :: 'a::one ^'n)$i = 1" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

288 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

289 
lemma one_plus_of_nat_neq_0: "(1::'a::semiring_char_0) + of_nat n \<noteq> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

290 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

291 
have "(1::'a) + of_nat n = 0 \<longleftrightarrow> of_nat 1 + of_nat n = (of_nat 0 :: 'a)" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

292 
also have "\<dots> \<longleftrightarrow> 1 + n = 0" by (simp only: of_nat_add[symmetric] of_nat_eq_iff) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

293 
finally show ?thesis by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

294 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

295 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

296 
instance "^" :: (semiring_char_0,type) semiring_char_0 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

297 
proof (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

298 
fix m n ::nat 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

299 
show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

300 
proof(induct m arbitrary: n) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

301 
case 0 thus ?case apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

302 
apply (induct n,auto simp add: ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

303 
using dimindex_ge_1 apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

304 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

305 
by (auto simp add: of_nat_index one_plus_of_nat_neq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

306 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

307 
case (Suc n m) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

308 
thus ?case apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

309 
apply (induct m, auto simp add: ring_simps of_nat_index zero_index) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

310 
using dimindex_ge_1 apply simp apply blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

311 
apply (simp add: one_plus_of_nat_neq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

312 
using dimindex_ge_1 apply simp apply blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

313 
apply (simp add: vector_component one_index of_nat_index) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

314 
apply (simp only: of_nat.simps(2)[where ?'a = 'a, symmetric] of_nat_eq_iff) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

315 
using dimindex_ge_1 apply simp apply blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

316 
apply (simp add: vector_component one_index of_nat_index) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

317 
apply (simp only: of_nat.simps(2)[where ?'a = 'a, symmetric] of_nat_eq_iff) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

318 
using dimindex_ge_1 apply simp apply blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

319 
apply (simp add: vector_component one_index of_nat_index) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

320 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

321 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

322 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

323 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

324 
instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes 
30039  325 
instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

326 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

327 
lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

328 
by (vector mult_assoc) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

329 
lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

330 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

331 
lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

332 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

333 
lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

334 
lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

335 
lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x  y) = c *s x  c *s y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

336 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

337 
lemma vector_smult_rneg: "(c::'a::ring) *s x = (c *s x)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

338 
lemma vector_smult_lneg: " (c::'a::ring) *s x = (c *s x)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

339 
lemma vector_sneg_minus1: "x = ( (1::'a::ring_1)) *s x" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

340 
lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

341 
lemma vector_sub_rdistrib: "((a::'a::ring)  b) *s x = a *s x  b *s x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

342 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

343 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

344 
lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

345 
apply (auto simp add: vec_def Cart_eq vec_component Cart_lambda_beta ) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

346 
using dimindex_ge_1 apply auto done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

347 

30040  348 
subsection {* Square root of sum of squares *} 
349 

350 
definition 

351 
"setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)" 

352 

353 
lemma setL2_cong: 

354 
"\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B" 

355 
unfolding setL2_def by simp 

356 

357 
lemma strong_setL2_cong: 

358 
"\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B" 

359 
unfolding setL2_def simp_implies_def by simp 

360 

361 
lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0" 

362 
unfolding setL2_def by simp 

363 

364 
lemma setL2_empty [simp]: "setL2 f {} = 0" 

365 
unfolding setL2_def by simp 

366 

367 
lemma setL2_insert [simp]: 

368 
"\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow> 

369 
setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)" 

370 
unfolding setL2_def by (simp add: setsum_nonneg) 

371 

372 
lemma setL2_nonneg [simp]: "0 \<le> setL2 f A" 

373 
unfolding setL2_def by (simp add: setsum_nonneg) 

374 

375 
lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0" 

376 
unfolding setL2_def by simp 

377 

378 
lemma setL2_mono: 

379 
assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i" 

380 
assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i" 

381 
shows "setL2 f K \<le> setL2 g K" 

382 
unfolding setL2_def 

383 
by (simp add: setsum_nonneg setsum_mono power_mono prems) 

384 

385 
lemma setL2_right_distrib: 

386 
"0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A" 

387 
unfolding setL2_def 

388 
apply (simp add: power_mult_distrib) 

389 
apply (simp add: setsum_right_distrib [symmetric]) 

390 
apply (simp add: real_sqrt_mult setsum_nonneg) 

391 
done 

392 

393 
lemma setL2_left_distrib: 

394 
"0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A" 

395 
unfolding setL2_def 

396 
apply (simp add: power_mult_distrib) 

397 
apply (simp add: setsum_left_distrib [symmetric]) 

398 
apply (simp add: real_sqrt_mult setsum_nonneg) 

399 
done 

400 

401 
lemma setsum_nonneg_eq_0_iff: 

402 
fixes f :: "'a \<Rightarrow> 'b::pordered_ab_group_add" 

403 
shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" 

404 
apply (induct set: finite, simp) 

405 
apply (simp add: add_nonneg_eq_0_iff setsum_nonneg) 

406 
done 

407 

408 
lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" 

409 
unfolding setL2_def 

410 
by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff) 

411 

412 
lemma setL2_triangle_ineq: 

413 
shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A" 

414 
proof (cases "finite A") 

415 
case False 

416 
thus ?thesis by simp 

417 
next 

418 
case True 

419 
thus ?thesis 

420 
proof (induct set: finite) 

421 
case empty 

422 
show ?case by simp 

423 
next 

424 
case (insert x F) 

425 
hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le> 

426 
sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)" 

427 
by (intro real_sqrt_le_mono add_left_mono power_mono insert 

428 
setL2_nonneg add_increasing zero_le_power2) 

429 
also have 

430 
"\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)" 

431 
by (rule real_sqrt_sum_squares_triangle_ineq) 

432 
finally show ?case 

433 
using insert by simp 

434 
qed 

435 
qed 

436 

437 
lemma sqrt_sum_squares_le_sum: 

438 
"\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y" 

439 
apply (rule power2_le_imp_le) 

440 
apply (simp add: power2_sum) 

441 
apply (simp add: mult_nonneg_nonneg) 

442 
apply (simp add: add_nonneg_nonneg) 

443 
done 

444 

445 
lemma setL2_le_setsum [rule_format]: 

446 
"(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A" 

447 
apply (cases "finite A") 

448 
apply (induct set: finite) 

449 
apply simp 

450 
apply clarsimp 

451 
apply (erule order_trans [OF sqrt_sum_squares_le_sum]) 

452 
apply simp 

453 
apply simp 

454 
apply simp 

455 
done 

456 

457 
lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>" 

458 
apply (rule power2_le_imp_le) 

459 
apply (simp add: power2_sum) 

460 
apply (simp add: mult_nonneg_nonneg) 

461 
apply (simp add: add_nonneg_nonneg) 

462 
done 

463 

464 
lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)" 

465 
apply (cases "finite A") 

466 
apply (induct set: finite) 

467 
apply simp 

468 
apply simp 

469 
apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs]) 

470 
apply simp 

471 
apply simp 

472 
done 

473 

474 
lemma setL2_mult_ineq_lemma: 

475 
fixes a b c d :: real 

476 
shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>" 

477 
proof  

478 
have "0 \<le> (a * d  b * c)\<twosuperior>" by simp 

479 
also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>  2 * (a * d) * (b * c)" 

480 
by (simp only: power2_diff power_mult_distrib) 

481 
also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>  2 * (a * c) * (b * d)" 

482 
by simp 

483 
finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>" 

484 
by simp 

485 
qed 

486 

487 
lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A" 

488 
apply (cases "finite A") 

489 
apply (induct set: finite) 

490 
apply simp 

491 
apply (rule power2_le_imp_le, simp) 

492 
apply (rule order_trans) 

493 
apply (rule power_mono) 

494 
apply (erule add_left_mono) 

495 
apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg) 

496 
apply (simp add: power2_sum) 

497 
apply (simp add: power_mult_distrib) 

498 
apply (simp add: right_distrib left_distrib) 

499 
apply (rule ord_le_eq_trans) 

500 
apply (rule setL2_mult_ineq_lemma) 

501 
apply simp 

502 
apply (intro mult_nonneg_nonneg setL2_nonneg) 

503 
apply simp 

504 
done 

505 

506 
lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A" 

507 
apply (rule_tac s="insert i (A  {i})" and t="A" in subst) 

508 
apply fast 

509 
apply (subst setL2_insert) 

510 
apply simp 

511 
apply simp 

512 
apply simp 

513 
done 

514 

515 
subsection {* Norms *} 

516 

517 
instantiation "^" :: (real_normed_vector, type) real_normed_vector 

518 
begin 

519 

520 
definition vector_norm_def: 

521 
"norm (x::'a^'b) = setL2 (\<lambda>i. norm (x$i)) {1 .. dimindex (UNIV:: 'b set)}" 

522 

523 
definition vector_sgn_def: 

524 
"sgn (x::'a^'b) = scaleR (inverse (norm x)) x" 

525 

526 
instance proof 

527 
fix a :: real and x y :: "'a ^ 'b" 

528 
show "0 \<le> norm x" 

529 
unfolding vector_norm_def 

530 
by (rule setL2_nonneg) 

531 
show "norm x = 0 \<longleftrightarrow> x = 0" 

532 
unfolding vector_norm_def 

533 
by (simp add: setL2_eq_0_iff Cart_eq) 

534 
show "norm (x + y) \<le> norm x + norm y" 

535 
unfolding vector_norm_def 

536 
apply (rule order_trans [OF _ setL2_triangle_ineq]) 

537 
apply (rule setL2_mono) 

538 
apply (simp add: vector_component norm_triangle_ineq) 

539 
apply simp 

540 
done 

541 
show "norm (scaleR a x) = \<bar>a\<bar> * norm x" 

542 
unfolding vector_norm_def 

543 
by (simp add: vector_component norm_scaleR setL2_right_distrib 

544 
cong: strong_setL2_cong) 

545 
show "sgn x = scaleR (inverse (norm x)) x" 

546 
by (rule vector_sgn_def) 

547 
qed 

548 

549 
end 

550 

30045  551 
subsection {* Inner products *} 
552 

553 
instantiation "^" :: (real_inner, type) real_inner 

554 
begin 

555 

556 
definition vector_inner_def: 

557 
"inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) {1 .. dimindex(UNIV::'b set)}" 

558 

559 
instance proof 

560 
fix r :: real and x y z :: "'a ^ 'b" 

561 
show "inner x y = inner y x" 

562 
unfolding vector_inner_def 

563 
by (simp add: inner_commute) 

564 
show "inner (x + y) z = inner x z + inner y z" 

565 
unfolding vector_inner_def 

566 
by (vector inner_left_distrib) 

567 
show "inner (scaleR r x) y = r * inner x y" 

568 
unfolding vector_inner_def 

569 
by (vector inner_scaleR_left) 

570 
show "0 \<le> inner x x" 

571 
unfolding vector_inner_def 

572 
by (simp add: setsum_nonneg) 

573 
show "inner x x = 0 \<longleftrightarrow> x = 0" 

574 
unfolding vector_inner_def 

575 
by (simp add: Cart_eq setsum_nonneg_eq_0_iff) 

576 
show "norm x = sqrt (inner x x)" 

577 
unfolding vector_inner_def vector_norm_def setL2_def 

578 
by (simp add: power2_norm_eq_inner) 

579 
qed 

580 

581 
end 

582 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

583 
subsection{* Properties of the dot product. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

584 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

585 
lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

586 
by (vector mult_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

587 
lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \<bullet> z = (x \<bullet> z) + (y \<bullet> z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

588 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

589 
lemma dot_radd: "x \<bullet> (y + (z::'a::ring ^ 'n)) = (x \<bullet> y) + (x \<bullet> z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

590 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

591 
lemma dot_lsub: "((x::'a::ring ^ 'n)  y) \<bullet> z = (x \<bullet> z)  (y \<bullet> z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

592 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

593 
lemma dot_rsub: "(x::'a::ring ^ 'n) \<bullet> (y  z) = (x \<bullet> y)  (x \<bullet> z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

594 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

595 
lemma dot_lmult: "(c *s x) \<bullet> y = (c::'a::ring) * (x \<bullet> y)" by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

596 
lemma dot_rmult: "x \<bullet> (c *s y) = (c::'a::comm_ring) * (x \<bullet> y)" by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

597 
lemma dot_lneg: "(x) \<bullet> (y::'a::ring ^ 'n) = (x \<bullet> y)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

598 
lemma dot_rneg: "(x::'a::ring ^ 'n) \<bullet> (y) = (x \<bullet> y)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

599 
lemma dot_lzero[simp]: "0 \<bullet> x = (0::'a::{comm_monoid_add, mult_zero})" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

600 
lemma dot_rzero[simp]: "x \<bullet> 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

601 
lemma dot_pos_le[simp]: "(0::'a\<Colon>ordered_ring_strict) <= x \<bullet> x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

602 
by (simp add: dot_def setsum_nonneg) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

603 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

604 
lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::pordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

605 
using fS fp setsum_nonneg[OF fp] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

606 
proof (induct set: finite) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

607 
case empty thus ?case by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

608 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

609 
case (insert x F) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

610 
from insert.prems have Fx: "f x \<ge> 0" and Fp: "\<forall> a \<in> F. f a \<ge> 0" by simp_all 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

611 
from insert.hyps Fp setsum_nonneg[OF Fp] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

612 
have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

613 
from sum_nonneg_eq_zero_iff[OF Fx setsum_nonneg[OF Fp]] insert.hyps(1,2) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

614 
show ?case by (simp add: h) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

615 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

616 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

617 
lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

618 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

619 
{assume f: "finite (UNIV :: 'n set)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

620 
let ?S = "{Suc 0 .. card (UNIV :: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

621 
have fS: "finite ?S" using f by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

622 
have fp: "\<forall> i\<in> ?S. x$i * x$i>= 0" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

623 
have ?thesis by (vector dimindex_def f setsum_squares_eq_0_iff[OF fS fp])} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

624 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

625 
{assume "\<not> finite (UNIV :: 'n set)" then have ?thesis by (vector dimindex_def)} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

626 
ultimately show ?thesis by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

627 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

628 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

629 
lemma dot_pos_lt: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

630 
by (auto simp add: le_less) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

631 

30040  632 
subsection{* The collapse of the general concepts to dimension one. *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

633 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

634 
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

635 
by (vector dimindex_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

636 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

637 
lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

638 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

639 
apply (erule_tac x= "x$1" in allE) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

640 
apply (simp only: vector_one[symmetric]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

641 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

642 

30040  643 
lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)" 
644 
by (simp add: vector_norm_def dimindex_def) 

645 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

646 
lemma norm_real: "norm(x::real ^ 1) = abs(x$1)" 
30040  647 
by (simp add: norm_vector_1) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

648 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

649 
text{* Metric *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

650 

30040  651 
text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

652 
definition dist:: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real" where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

653 
"dist x y = norm (x  y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

654 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

655 
lemma dist_real: "dist(x::real ^ 1) y = abs((x$1)  (y$1))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

656 
using dimindex_ge_1[of "UNIV :: 1 set"] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

657 
by (auto simp add: norm_real dist_def vector_component Cart_lambda_beta[where ?'a = "1"] ) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

658 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

659 
subsection {* A connectedness or intermediate value lemma with several applications. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

660 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

661 
lemma connected_real_lemma: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

662 
fixes f :: "real \<Rightarrow> real ^ 'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

663 
assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

664 
and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y  x) < d \<longrightarrow> dist(f y) (f x) < e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

665 
and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

666 
and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

667 
and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

668 
shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

669 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

670 
let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

671 
have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

672 
have Sub: "\<exists>y. isUb UNIV ?S y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

673 
apply (rule exI[where x= b]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

674 
using ab fb e12 by (auto simp add: isUb_def setle_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

675 
from reals_complete[OF Se Sub] obtain l where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

676 
l: "isLub UNIV ?S l"by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

677 
have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

678 
apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

679 
by (metis linorder_linear) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

680 
have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

681 
apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

682 
by (metis linorder_linear not_le) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

683 
have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z  x) < d" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

684 
have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

685 
have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by dlo 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

686 
{assume le2: "f l \<in> e2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

687 
from le2 fa fb e12 alb have la: "l \<noteq> a" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

688 
hence lap: "l  a > 0" using alb by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

689 
from e2[rule_format, OF le2] obtain e where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

690 
e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

691 
from dst[OF alb e(1)] obtain d where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

692 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

693 
have "\<exists>d'. d' < d \<and> d' >0 \<and> l  d' > a" using lap d(1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

694 
apply ferrack by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

695 
then obtain d' where d': "d' > 0" "d' < d" "l  d' > a" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

696 
from d e have th0: "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> f y \<in> e2" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

697 
from th0[rule_format, of "l  d'"] d' have "f (l  d') \<in> e2" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

698 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

699 
have "f (l  d') \<in> e1" using ale1[rule_format, of "l d'"] d' by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

700 
ultimately have False using e12 alb d' by auto} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

701 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

702 
{assume le1: "f l \<in> e1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

703 
from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

704 
hence blp: "b  l > 0" using alb by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

705 
from e1[rule_format, OF le1] obtain e where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

706 
e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

707 
from dst[OF alb e(1)] obtain d where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

708 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

709 
have "\<exists>d'. d' < d \<and> d' >0" using d(1) by dlo 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

710 
then obtain d' where d': "d' > 0" "d' < d" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

711 
from d e have th0: "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> f y \<in> e1" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

712 
hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

713 
with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

714 
with l d' have False 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

715 
by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) } 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

716 
ultimately show ?thesis using alb by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

717 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

718 

29881  719 
text{* One immediately useful corollary is the existence of square roots!  Should help to get rid of all the development of squareroot for reals as a special case @{typ "real^1"} *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

720 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

721 
lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

722 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

723 
have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

724 
thus ?thesis by (simp add: ring_simps power2_eq_square) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

725 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

726 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

727 
lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y  x) < d \<longrightarrow> abs(y * y  x * x) < e)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

728 
using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_def, rule_format, of e x] apply (auto simp add: power2_eq_square) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

729 
apply (rule_tac x="s" in exI) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

730 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

731 
apply (erule_tac x=y in allE) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

732 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

733 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

734 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

735 
lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y^2 ==> sqrt x <= y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

736 
using real_sqrt_le_iff[of x "y^2"] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

737 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

738 
lemma real_le_rsqrt: "x^2 \<le> y \<Longrightarrow> x \<le> sqrt y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

739 
using real_sqrt_le_mono[of "x^2" y] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

740 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

741 
lemma real_less_rsqrt: "x^2 < y \<Longrightarrow> x < sqrt y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

742 
using real_sqrt_less_mono[of "x^2" y] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

743 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

744 
lemma sqrt_even_pow2: assumes n: "even n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

745 
shows "sqrt(2 ^ n) = 2 ^ (n div 2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

746 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

747 
from n obtain m where m: "n = 2*m" unfolding even_nat_equiv_def2 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

748 
by (auto simp add: nat_number) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

749 
from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

750 
by (simp only: power_mult[symmetric] mult_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

751 
then show ?thesis using m by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

752 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

753 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

754 
lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

755 
apply (cases "x = 0", simp_all) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

756 
using sqrt_divide_self_eq[of x] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

757 
apply (simp add: inverse_eq_divide real_sqrt_ge_0_iff field_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

758 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

759 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

760 
text{* Hence derive more interesting properties of the norm. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

761 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

762 
lemma norm_0: "norm (0::real ^ 'n) = 0" 
30040  763 
by (rule norm_zero) 
764 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

765 
lemma norm_mul: "norm(a *s x) = abs(a) * norm x" 
30040  766 
by (simp add: vector_norm_def vector_component setL2_right_distrib 
767 
abs_mult cong: strong_setL2_cong) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

768 
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))" 
30040  769 
by (simp add: vector_norm_def dot_def setL2_def power2_eq_square) 
770 
lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)" 

771 
by (simp add: vector_norm_def setL2_def dot_def power2_eq_square) 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

772 
lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x" 
30040  773 
by (simp add: real_vector_norm_def) 
30041  774 
lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

775 
lemma vector_mul_eq_0: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

776 
by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

777 
lemma vector_mul_lcancel: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

778 
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

779 
lemma vector_mul_rcancel: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

780 
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

781 
lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==> a *s x = a *s y ==> (x = y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

782 
by (metis vector_mul_lcancel) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

783 
lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

784 
by (metis vector_mul_rcancel) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

785 
lemma norm_cauchy_schwarz: "x \<bullet> y <= norm x * norm y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

786 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

787 
{assume "norm x = 0" 
30041  788 
hence ?thesis by (simp add: dot_lzero dot_rzero)} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

789 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

790 
{assume "norm y = 0" 
30041  791 
hence ?thesis by (simp add: dot_lzero dot_rzero)} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

792 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

793 
{assume h: "norm x \<noteq> 0" "norm y \<noteq> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

794 
let ?z = "norm y *s x  norm x *s y" 
30041  795 
from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

796 
from dot_pos_le[of ?z] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

797 
have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

798 
apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

799 
by (simp add: norm_pow_2[symmetric] power2_eq_square dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

800 
hence "x\<bullet>y \<le> (norm x ^2 * norm y ^2) / (norm x * norm y)" using p 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

801 
by (simp add: field_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

802 
hence ?thesis using h by (simp add: power2_eq_square)} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

803 
ultimately show ?thesis by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

804 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

805 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

806 
lemma norm_cauchy_schwarz_abs: "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

807 
using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "y"] 
30041  808 
by (simp add: real_abs_def dot_rneg) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

809 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

810 
lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x  y)" 
30041  811 
using norm_triangle_ineq[of "y" "x  y"] by (simp add: ring_simps) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

812 
lemma norm_triangle_le: "norm(x::real ^'n) + norm y <= e ==> norm(x + y) <= e" 
30041  813 
by (metis order_trans norm_triangle_ineq) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

814 
lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e" 
30041  815 
by (metis basic_trans_rules(21) norm_triangle_ineq) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

816 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

817 
lemma setsum_delta: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

818 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

819 
shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

820 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

821 
let ?f = "(\<lambda>k. if k=a then b k else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

822 
{assume a: "a \<notin> S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

823 
hence "\<forall> k\<in> S. ?f k = 0" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

824 
hence ?thesis using a by simp} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

825 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

826 
{assume a: "a \<in> S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

827 
let ?A = "S  {a}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

828 
let ?B = "{a}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

829 
have eq: "S = ?A \<union> ?B" using a by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

830 
have dj: "?A \<inter> ?B = {}" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

831 
from fS have fAB: "finite ?A" "finite ?B" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

832 
have "setsum ?f S = setsum ?f ?A + setsum ?f ?B" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

833 
using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

834 
by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

835 
then have ?thesis using a by simp} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

836 
ultimately show ?thesis by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

837 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

838 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

839 
lemma component_le_norm: "i \<in> {1 .. dimindex(UNIV :: 'n set)} ==> \<bar>x$i\<bar> <= norm (x::real ^ 'n)" 
30040  840 
apply (simp add: vector_norm_def) 
841 
apply (rule member_le_setL2, simp_all) 

842 
done 

843 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

844 
lemma norm_bound_component_le: "norm(x::real ^ 'n) <= e 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

845 
==> \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. \<bar>x$i\<bar> <= e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

846 
by (metis component_le_norm order_trans) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

847 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

848 
lemma norm_bound_component_lt: "norm(x::real ^ 'n) < e 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

849 
==> \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. \<bar>x$i\<bar> < e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

850 
by (metis component_le_norm basic_trans_rules(21)) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

851 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

852 
lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\<lambda>i. \<bar>x$i\<bar>) {1..dimindex(UNIV::'n set)}" 
30040  853 
by (simp add: vector_norm_def setL2_le_setsum) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

854 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

855 
lemma real_abs_norm: "\<bar> norm x\<bar> = norm (x :: real ^'n)" 
30040  856 
by (rule abs_norm_cancel) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

857 
lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n)  norm y\<bar> <= norm(x  y)" 
30040  858 
by (rule norm_triangle_ineq3) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

859 
lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

860 
by (simp add: real_vector_norm_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

861 
lemma norm_lt: "norm(x::real ^'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

862 
by (simp add: real_vector_norm_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

863 
lemma norm_eq: "norm (x::real ^'n) = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

864 
by (simp add: order_eq_iff norm_le) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

865 
lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \<longleftrightarrow> x \<bullet> x = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

866 
by (simp add: real_vector_norm_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

867 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

868 
text{* Squaring equations and inequalities involving norms. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

869 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

870 
lemma dot_square_norm: "x \<bullet> x = norm(x)^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

871 
by (simp add: real_vector_norm_def dot_pos_le ) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

872 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

873 
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2" 
30040  874 
by (auto simp add: real_vector_norm_def) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

875 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

876 
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

877 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

878 
have "x^2 \<le> y^2 \<longleftrightarrow> (x y) * (y + x) \<le> 0" by (simp add: ring_simps power2_eq_square) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

879 
also have "\<dots> \<longleftrightarrow> \<bar>x\<bar> \<le> \<bar>y\<bar>" apply (simp add: zero_compare_simps real_abs_def not_less) by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

880 
finally show ?thesis .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

881 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

882 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

883 
lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2" 
30040  884 
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) 
30041  885 
using norm_ge_zero[of x] 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

886 
apply arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

887 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

888 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

889 
lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2" 
30040  890 
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) 
30041  891 
using norm_ge_zero[of x] 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

892 
apply arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

893 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

894 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

895 
lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

896 
by (metis not_le norm_ge_square) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

897 
lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

898 
by (metis norm_le_square not_less) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

899 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

900 
text{* Dot product in terms of the norm rather than conversely. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

901 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

902 
lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2  norm x ^ 2  norm y ^ 2) / 2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

903 
by (simp add: norm_pow_2 dot_ladd dot_radd dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

904 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

905 
lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2)  norm(x  y) ^ 2) / 2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

906 
by (simp add: norm_pow_2 dot_ladd dot_radd dot_lsub dot_rsub dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

907 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

908 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

909 
text{* Equality of vectors in terms of @{term "op \<bullet>"} products. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

910 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

911 
lemma vector_eq: "(x:: real ^ 'n) = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y\<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

912 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

913 
assume "?lhs" then show ?rhs by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

914 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

915 
assume ?rhs 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

916 
then have "x \<bullet> x  x \<bullet> y = 0 \<and> x \<bullet> y  y\<bullet> y = 0" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

917 
hence "x \<bullet> (x  y) = 0 \<and> y \<bullet> (x  y) = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

918 
by (simp add: dot_rsub dot_lsub dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

919 
then have "(x  y) \<bullet> (x  y) = 0" by (simp add: ring_simps dot_lsub dot_rsub) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

920 
then show "x = y" by (simp add: dot_eq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

921 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

922 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

923 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

924 
subsection{* General linear decision procedure for normed spaces. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

925 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

926 
lemma norm_cmul_rule_thm: "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(c *s x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

927 
apply (clarsimp simp add: norm_mul) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

928 
apply (rule mult_mono1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

929 
apply simp_all 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

930 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

931 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

932 
lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n) \<Longrightarrow> b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

933 
apply (rule norm_triangle_le) by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

934 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

935 
lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \<ge> b == a  b \<ge> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

936 
by (simp add: ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

937 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

938 
lemma pth_1: "(x::real^'n) == 1 *s x" by (simp only: vector_smult_lid) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

939 
lemma pth_2: "x  (y::real^'n) == x + y" by (atomize (full)) simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

940 
lemma pth_3: "(x::real^'n) == 1 *s x" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

941 
lemma pth_4: "0 *s (x::real^'n) == 0" "c *s 0 = (0::real ^ 'n)" by vector+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

942 
lemma pth_5: "c *s (d *s x) == (c * d) *s (x::real ^ 'n)" by (atomize (full)) vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

943 
lemma pth_6: "(c::real) *s (x + y) == c *s x + c *s y" by (atomize (full)) (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

944 
lemma pth_7: "0 + x == (x::real^'n)" "x + 0 == x" by simp_all 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

945 
lemma pth_8: "(c::real) *s x + d *s x == (c + d) *s x" by (atomize (full)) (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

946 
lemma pth_9: "((c::real) *s x + z) + d *s x == (c + d) *s x + z" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

947 
"c *s x + (d *s x + z) == (c + d) *s x + z" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

948 
"(c *s x + w) + (d *s x + z) == (c + d) *s x + (w + z)" by ((atomize (full)), vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

949 
lemma pth_a: "(0::real) *s x + y == y" by (atomize (full)) vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

950 
lemma pth_b: "(c::real) *s x + d *s y == c *s x + d *s y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

951 
"(c *s x + z) + d *s y == c *s x + (z + d *s y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

952 
"c *s x + (d *s y + z) == c *s x + (d *s y + z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

953 
"(c *s x + w) + (d *s y + z) == c *s x + (w + (d *s y + z))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

954 
by ((atomize (full)), vector)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

955 
lemma pth_c: "(c::real) *s x + d *s y == d *s y + c *s x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

956 
"(c *s x + z) + d *s y == d *s y + (c *s x + z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

957 
"c *s x + (d *s y + z) == d *s y + (c *s x + z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

958 
"(c *s x + w) + (d *s y + z) == d *s y + ((c *s x + w) + z)" by ((atomize (full)), vector)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

959 
lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

960 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

961 
lemma norm_imp_pos_and_ge: "norm (x::real ^ 'n) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x" 
30041  962 
by (atomize) (auto simp add: norm_ge_zero) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

963 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

964 
lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> x \<ge> 0" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

965 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

966 
lemma norm_pths: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

967 
"(x::real ^'n) = y \<longleftrightarrow> norm (x  y) \<le> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

968 
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x  y) \<le> 0)" 
30041  969 
using norm_ge_zero[of "x  y"] by auto 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

970 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

971 
use "normarith.ML" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

972 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

973 
method_setup norm = {* Method.ctxt_args (Method.SIMPLE_METHOD' o NormArith.norm_arith_tac) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

974 
*} "Proves simple linear statements about vector norms" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

975 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

976 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

977 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

978 
text{* Hence more metric properties. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

979 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

980 
lemma dist_refl: "dist x x = 0" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

981 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

982 
lemma dist_sym: "dist x y = dist y x"by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

983 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

984 
lemma dist_pos_le: "0 <= dist x y" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

985 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

986 
lemma dist_triangle: "dist x z <= dist x y + dist y z" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

987 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

988 
lemma dist_triangle_alt: "dist y z <= dist x y + dist x z" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

989 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

990 
lemma dist_eq_0: "dist x y = 0 \<longleftrightarrow> x = y" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

991 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

992 
lemma dist_pos_lt: "x \<noteq> y ==> 0 < dist x y" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

993 
lemma dist_nz: "x \<noteq> y \<longleftrightarrow> 0 < dist x y" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

994 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

995 
lemma dist_triangle_le: "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

996 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

997 
lemma dist_triangle_lt: "dist x z + dist y z < e ==> dist x y < e" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

998 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

999 
lemma dist_triangle_half_l: "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 ==> dist x1 x2 < e" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1000 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1001 
lemma dist_triangle_half_r: "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 ==> dist x1 x2 < e" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1002 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1003 
lemma dist_triangle_add: "dist (x + y) (x' + y') <= dist x x' + dist y y'" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1004 
by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1005 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1006 
lemma dist_mul: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1007 
unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1008 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1009 
lemma dist_triangle_add_half: " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 ==> dist(x + y) (x' + y') < e" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1010 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1011 
lemma dist_le_0: "dist x y <= 0 \<longleftrightarrow> x = y" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1012 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1013 
instantiation "^" :: (monoid_add,type) monoid_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1014 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1015 
instance by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1016 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1017 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1018 
lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1019 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1020 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1021 
apply (cases "finite S") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1022 
apply (rule finite_induct[of S]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1023 
apply (auto simp add: vector_component zero_index) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1024 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1025 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1026 
lemma setsum_clauses: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1027 
shows "setsum f {} = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1028 
and "finite S \<Longrightarrow> setsum f (insert x S) = 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1029 
(if x \<in> S then setsum f S else f x + setsum f S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1030 
by (auto simp add: insert_absorb) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1031 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1032 
lemma setsum_cmul: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1033 
fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1034 
shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1035 
by (simp add: setsum_eq Cart_eq Cart_lambda_beta vector_component setsum_right_distrib) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1036 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1037 
lemma setsum_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1038 
fixes f:: " 'a \<Rightarrow> ('b::semiring_1) ^'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1039 
assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1040 
shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1041 
using i by (simp add: setsum_eq Cart_lambda_beta) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1042 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1043 
(* This needs finiteness assumption due to the definition of fold!!! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1044 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1045 
lemma setsum_superset: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1046 
assumes fb: "finite B" and ab: "A \<subseteq> B" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1047 
and f0: "\<forall>x \<in> B  A. f x = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1048 
shows "setsum f B = setsum f A" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1049 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1050 
from ab fb have fa: "finite A" by (metis finite_subset) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1051 
from fb have fba: "finite (B  A)" by (metis finite_Diff) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1052 
have d: "A \<inter> (B  A) = {}" by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1053 
from ab have b: "B = A \<union> (B  A)" by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1054 
from setsum_Un_disjoint[OF fa fba d, of f] b 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1055 
setsum_0'[OF f0] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1056 
show "setsum f B = setsum f A" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1057 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1058 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1059 
lemma setsum_restrict_set: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1060 
assumes fA: "finite A" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1061 
shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1062 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1063 
from fA have fab: "finite (A \<inter> B)" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1064 
have aba: "A \<inter> B \<subseteq> A" by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1065 
let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1066 
from setsum_superset[OF fA aba, of ?g] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1067 
show ?thesis by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1068 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1069 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1070 
lemma setsum_cases: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1071 
assumes fA: "finite A" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1072 
shows "setsum (\<lambda>x. if x \<in> B then f x else g x) A = 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1073 
setsum f (A \<inter> B) + setsum g (A \<inter>  B)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1074 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1075 
have a: "A = A \<inter> B \<union> A \<inter> B" "(A \<inter> B) \<inter> (A \<inter> B) = {}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1076 
by blast+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1077 
from fA 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1078 
have f: "finite (A \<inter> B)" "finite (A \<inter> B)" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1079 
let ?g = "\<lambda>x. if x \<in> B then f x else g x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1080 
from setsum_Un_disjoint[OF f a(2), of ?g] a(1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1081 
show ?thesis by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1082 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1083 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1084 
lemma setsum_norm: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1085 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1086 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1087 
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1088 
proof(induct rule: finite_induct[OF fS]) 
30041  1089 
case 1 thus ?case by simp 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1090 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1091 
case (2 x S) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1092 
from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1093 
also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1094 
using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1095 
finally show ?case using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1096 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1097 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1098 
lemma real_setsum_norm: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1099 
fixes f :: "'a \<Rightarrow> real ^'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1100 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1101 
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1102 
proof(induct rule: finite_induct[OF fS]) 
30040  1103 
case 1 thus ?case by simp 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1104 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1105 
case (2 x S) 
30040  1106 
from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq) 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1107 
also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1108 
using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1109 
finally show ?case using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1110 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1111 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1112 
lemma setsum_norm_le: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1113 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1114 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1115 
and fg: "\<forall>x \<in> S. norm (f x) \<le> g x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1116 
shows "norm (setsum f S) \<le> setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1117 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1118 
from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1119 
by  (rule setsum_mono, simp) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1120 
then show ?thesis using setsum_norm[OF fS, of f] fg 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1121 
by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1122 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1123 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1124 
lemma real_setsum_norm_le: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1125 
fixes f :: "'a \<Rightarrow> real ^ 'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1126 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1127 
and fg: "\<forall>x \<in> S. norm (f x) \<le> g x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1128 
shows "norm (setsum f S) \<le> setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1129 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1130 
from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1131 
by  (rule setsum_mono, simp) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1132 
then show ?thesis using real_setsum_norm[OF fS, of f] fg 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1133 
by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1134 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1135 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1136 
lemma setsum_norm_bound: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1137 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1138 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1139 
and K: "\<forall>x \<in> S. norm (f x) \<le> K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1140 
shows "norm (setsum f S) \<le> of_nat (card S) * K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1141 
using setsum_norm_le[OF fS K] setsum_constant[symmetric] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1142 
by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1143 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1144 
lemma real_setsum_norm_bound: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1145 
fixes f :: "'a \<Rightarrow> real ^ 'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1146 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1147 
and K: "\<forall>x \<in> S. norm (f x) \<le> K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1148 
shows "norm (setsum f S) \<le> of_nat (card S) * K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1149 
using real_setsum_norm_le[OF fS K] setsum_constant[symmetric] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1150 
by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1151 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1152 
lemma setsum_vmul: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1153 
fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector,semiring, mult_zero}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1154 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1155 
shows "setsum f S *s v = setsum (\<lambda>x. f x *s v) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1156 
proof(induct rule: finite_induct[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1157 
case 1 then show ?case by (simp add: vector_smult_lzero) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1158 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1159 
case (2 x F) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1160 
from "2.hyps" have "setsum f (insert x F) *s v = (f x + setsum f F) *s v" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1161 
by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1162 
also have "\<dots> = f x *s v + setsum f F *s v" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1163 
by (simp add: vector_sadd_rdistrib) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1164 
also have "\<dots> = setsum (\<lambda>x. f x *s v) (insert x F)" using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1165 
finally show ?case . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1166 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1167 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1168 
(* FIXME : Problem thm setsum_vmul[of _ "f:: 'a \<Rightarrow> real ^'n"]  
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1169 
Get rid of *s and use real_vector instead! Also prove that ^ creates a real_vector !! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1170 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1171 
lemma setsum_add_split: assumes mn: "(m::nat) \<le> n + 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1172 
shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1173 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1174 
let ?A = "{m .. n}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1175 
let ?B = "{n + 1 .. n + p}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1176 
have eq: "{m .. n+p} = ?A \<union> ?B" using mn by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1177 
have d: "?A \<inter> ?B = {}" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1178 
from setsum_Un_disjoint[of "?A" "?B" f] eq d show ?thesis by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1179 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1180 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1181 
lemma setsum_reindex_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1182 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1183 
and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1184 
shows "setsum h (f ` S) = setsum (h o f) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1185 
using nz 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1186 
proof(induct rule: finite_induct[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1187 
case 1 thus ?case by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1188 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1189 
case (2 x F) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1190 
{assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1191 
then obtain y where y: "y \<in> F" "f x = f y" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1192 
from "2.hyps" y have xy: "x \<noteq> y" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1193 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1194 
from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1195 
have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1196 
also have "\<dots> = setsum (h o f) (insert x F)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1197 
using "2.hyps" "2.prems" h0 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1198 
finally have ?case .} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1199 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1200 
{assume fxF: "f x \<notin> f ` F" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1201 
have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1202 
using fxF "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1203 
also have "\<dots> = setsum (h o f) (insert x F)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1204 
using "2.hyps" "2.prems" fxF 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1205 
apply auto apply metis done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1206 
finally have ?case .} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1207 
ultimately show ?case by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1208 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1209 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1210 
lemma setsum_Un_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1211 
assumes fS: "finite S" and fF: "finite F" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1212 
and f: "\<forall> x\<in> S \<inter> F . f x = (0::'a::ab_group_add)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1213 
shows "setsum f (S \<union> F) = setsum f S + setsum f F" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1214 
using setsum_Un[OF fS fF, of f] setsum_0'[OF f] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1215 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1216 
lemma setsum_natinterval_left: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1217 
assumes mn: "(m::nat) <= n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1218 
shows "setsum f {m..n} = f m + setsum f {m + 1..n}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1219 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1220 
from mn have "{m .. n} = insert m {m+1 .. n}" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1221 
then show ?thesis by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1222 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1223 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1224 
lemma setsum_natinterval_difff: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1225 
fixes f:: "nat \<Rightarrow> ('a::ab_group_add)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1226 
shows "setsum (\<lambda>k. f k  f(k + 1)) {(m::nat) .. n} = 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1227 
(if m <= n then f m  f(n + 1) else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1228 
by (induct n, auto simp add: ring_simps not_le le_Suc_eq) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1229 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1230 
lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1231 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1232 
lemma setsum_setsum_restrict: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1233 
"finite S \<Longrightarrow> finite T \<Longrightarrow> setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y\<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1234 
apply (simp add: setsum_restrict_set'[unfolded mem_def] mem_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1235 
by (rule setsum_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1236 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1237 
lemma setsum_image_gen: assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1238 
shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1239 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1240 
{fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1241 
note th0 = this 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1242 
have "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1243 
apply (rule setsum_cong2) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1244 
by (simp add: th0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1245 
also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1246 
apply (rule setsum_setsum_restrict[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1247 
by (rule finite_imageI[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1248 
finally show ?thesis . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1249 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1250 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1251 
(* FIXME: Here too need stupid finiteness assumption on T!!! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1252 
lemma setsum_group: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1253 
assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1254 
shows "setsum (\<lambda>y. setsum g {x. x\<in> S \<and> f x = y}) T = setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1255 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1256 
apply (subst setsum_image_gen[OF fS, of g f]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1257 
apply (rule setsum_superset[OF fT fST]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1258 
by (auto intro: setsum_0') 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1259 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1260 
(* FIXME: Change the name to fold_image\<dots> *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1261 
lemma (in comm_monoid_mult) fold_1': "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1262 
apply (induct set: finite) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1263 
apply simp by (auto simp add: fold_image_insert) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1264 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1265 
lemma (in comm_monoid_mult) fold_union_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1266 
assumes fS: "finite S" and fT: "finite T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1267 
and I0: "\<forall>x \<in> S\<inter>T. f x = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1268 
shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1269 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1270 
have "fold_image op * f 1 (S \<inter> T) = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1271 
apply (rule fold_1') 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1272 
using fS fT I0 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1273 
with fold_image_Un_Int[OF fS fT] show ?thesis by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1274 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1275 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1276 
lemma setsum_union_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1277 
assumes fS: "finite S" and fT: "finite T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1278 
and I0: "\<forall>x \<in> S\<inter>T. f x = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1279 
shows "setsum f (S \<union> T) = setsum f S + setsum f T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1280 
using fS fT 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1281 
apply (simp add: setsum_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1282 
apply (rule comm_monoid_add.fold_union_nonzero) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1283 
using I0 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1284 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1285 
lemma setprod_union_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1286 
assumes fS: "finite S" and fT: "finite T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1287 
and I0: "\<forall>x \<in> S\<inter>T. f x = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1288 
shows "setprod f (S \<union> T) = setprod f S * setprod f T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1289 
using fS fT 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1290 
apply (simp add: setprod_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1291 
apply (rule fold_union_nonzero) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1292 
using I0 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1293 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1294 
lemma setsum_unions_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1295 
assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1296 
and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1297 
shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1298 
using fSS f0 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1299 
proof(induct rule: finite_induct[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1300 
case 1 thus ?case by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1301 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1302 
case (2 T F) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1303 
then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1304 
and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1305 
from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1306 
from "2.prems" TF fTF 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1307 
show ?case 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1308 
by (auto simp add: H[symmetric] intro: setsum_union_nonzero[OF fTF(1) fUF, of f]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1309 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1310 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1311 
(* FIXME : Copied from Pocklington  should be moved to Finite_Set!!!!!!!! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1312 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1313 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1314 
lemma (in comm_monoid_mult) fold_related: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1315 
assumes Re: "R e e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1316 
and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1317 
and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1318 
shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1319 
using fS by (rule finite_subset_induct) (insert assms, auto) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1320 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1321 
(* FIXME: I think we can get rid of the finite assumption!! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1322 
lemma (in comm_monoid_mult) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1323 
fold_eq_general: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1324 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1325 
and h: "\<forall>y\<in>S'. \<exists>!x. x\<in> S \<and> h(x) = y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1326 
and f12: "\<forall>x\<in>S. h x \<in> S' \<and> f2(h x) = f1 x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1327 
shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1328 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1329 
from h f12 have hS: "h ` S = S'" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1330 
{fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1331 
from f12 h H have "x = y" by auto } 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1332 
hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1333 
from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1334 
from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1335 
also have "\<dots> = fold_image (op *) (f2 o h) e S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1336 
using fold_image_reindex[OF fS hinj, of f2 e] . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1337 
also have "\<dots> = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1338 
by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1339 
finally show ?thesis .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1340 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1341 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1342 
lemma (in comm_monoid_mult) fold_eq_general_inverses: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1343 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1344 
and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1345 
and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1346 
shows "fold_image (op *) f e S = fold_image (op *) g e T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1347 
using fold_eq_general[OF fS, of T h g f e] kh hk by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1348 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1349 
lemma setsum_eq_general_reverses: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1350 
assumes fS: "finite S" and fT: "finite T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1351 
and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1352 
and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1353 
shows "setsum f S = setsum g T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1354 
apply (simp add: setsum_def fS fT) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1355 
apply (rule comm_monoid_add.fold_eq_general_inverses[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1356 
apply (erule kh) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1357 
apply (erule hk) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1358 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1359 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1360 
lemma vsum_norm_allsubsets_bound: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1361 
fixes f:: "'a \<Rightarrow> real ^'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1362 
assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1363 
shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real (dimindex(UNIV :: 'n set)) * e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1364 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1365 
let ?d = "real (dimindex (UNIV ::'n set))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1366 
let ?nf = "\<lambda>x. norm (f x)" 
4ac60c7d9b78
(Real) Vectors in Eucl 