author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44133  691c52e900ca 
child 50526  899c9c4e4a4c 
permissions  rwrr 
41959  1 
(* Title: HOL/Multivariate_Analysis/Operator_Norm.thy 
36581  2 
Author: Amine Chaieb, University of Cambridge 
3 
*) 

4 

5 
header {* Operator Norm *} 

6 

7 
theory Operator_Norm 

44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
41959
diff
changeset

8 
imports Linear_Algebra 
36581  9 
begin 
10 

11 
definition "onorm f = Sup {norm (f x) x. norm x = 1}" 

12 

13 
lemma norm_bound_generalize: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

14 
fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" 
36581  15 
assumes lf: "linear f" 
16 
shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)" (is "?lhs \<longleftrightarrow> ?rhs") 

17 
proof 

18 
{assume H: ?rhs 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

19 
{fix x :: "'a" assume x: "norm x = 1" 
36581  20 
from H[rule_format, of x] x have "norm (f x) \<le> b" by simp} 
21 
then have ?lhs by blast } 

22 

23 
moreover 

24 
{assume H: ?lhs 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

25 
have bp: "b \<ge> 0" applyapply(rule order_trans [OF norm_ge_zero]) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

26 
apply(rule H[rule_format, of "basis 0::'a"]) by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

27 
{fix x :: "'a" 
36581  28 
{assume "x = 0" 
29 
then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)} 

30 
moreover 

31 
{assume x0: "x \<noteq> 0" 

32 
hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero) 

33 
let ?c = "1/ norm x" 

36593
fb69c8cd27bd
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents:
36581
diff
changeset

34 
have "norm (?c *\<^sub>R x) = 1" using x0 by (simp add: n0) 
fb69c8cd27bd
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents:
36581
diff
changeset

35 
with H have "norm (f (?c *\<^sub>R x)) \<le> b" by blast 
36581  36 
hence "?c * norm (f x) \<le> b" 
37 
by (simp add: linear_cmul[OF lf]) 

38 
hence "norm (f x) \<le> b * norm x" 

39 
using n0 norm_ge_zero[of x] by (auto simp add: field_simps)} 

40 
ultimately have "norm (f x) \<le> b * norm x" by blast} 

41 
then have ?rhs by blast} 

42 
ultimately show ?thesis by blast 

43 
qed 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

44 

36581  45 
lemma onorm: 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

46 
fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" 
36581  47 
assumes lf: "linear f" 
48 
shows "norm (f x) <= onorm f * norm x" 

49 
and "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b" 

50 
proof 

51 
{ 

52 
let ?S = "{norm (f x) x. norm x = 1}" 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

53 
have "norm (f (basis 0)) \<in> ?S" unfolding mem_Collect_eq 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

54 
apply(rule_tac x="basis 0" in exI) by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

55 
hence Se: "?S \<noteq> {}" by auto 
36581  56 
from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b" 
57 
unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def) 

58 
{from Sup[OF Se b, unfolded onorm_def[symmetric]] 

59 
show "norm (f x) <= onorm f * norm x" 

60 
apply  

61 
apply (rule spec[where x = x]) 

62 
unfolding norm_bound_generalize[OF lf, symmetric] 

63 
by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} 

64 
{ 

65 
show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b" 

66 
using Sup[OF Se b, unfolded onorm_def[symmetric]] 

67 
unfolding norm_bound_generalize[OF lf, symmetric] 

68 
by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} 

69 
} 

70 
qed 

71 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

72 
lemma onorm_pos_le: assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)" shows "0 <= onorm f" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

73 
using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis 0"]] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

74 
using DIM_positive[where 'a='n] by auto 
36581  75 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

76 
lemma onorm_eq_0: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)" 
36581  77 
shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)" 
78 
using onorm[OF lf] 

79 
apply (auto simp add: onorm_pos_le) 

80 
apply atomize 

81 
apply (erule allE[where x="0::real"]) 

82 
using onorm_pos_le[OF lf] 

83 
apply arith 

84 
done 

85 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

86 
lemma onorm_const: "onorm(\<lambda>x::'a::euclidean_space. (y::'b::euclidean_space)) = norm y" 
36581  87 
proof 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

88 
let ?f = "\<lambda>x::'a. (y::'b)" 
36581  89 
have th: "{norm (?f x) x. norm x = 1} = {norm y}" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

90 
apply safe apply(rule_tac x="basis 0" in exI) by auto 
36581  91 
show ?thesis 
92 
unfolding onorm_def th 

93 
apply (rule Sup_unique) by (simp_all add: setle_def) 

94 
qed 

95 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

96 
lemma onorm_pos_lt: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)" 
36581  97 
shows "0 < onorm f \<longleftrightarrow> ~(\<forall>x. f x = 0)" 
98 
unfolding onorm_eq_0[OF lf, symmetric] 

99 
using onorm_pos_le[OF lf] by arith 

100 

101 
lemma onorm_compose: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

102 
assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

103 
and lg: "linear (g::'k::euclidean_space \<Rightarrow> 'n::euclidean_space)" 
36581  104 
shows "onorm (f o g) <= onorm f * onorm g" 
105 
apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format]) 

106 
unfolding o_def 

107 
apply (subst mult_assoc) 

108 
apply (rule order_trans) 

109 
apply (rule onorm(1)[OF lf]) 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
37489
diff
changeset

110 
apply (rule mult_left_mono) 
36581  111 
apply (rule onorm(1)[OF lg]) 
112 
apply (rule onorm_pos_le[OF lf]) 

113 
done 

114 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

115 
lemma onorm_neg_lemma: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)" 
36581  116 
shows "onorm (\<lambda>x.  f x) \<le> onorm f" 
117 
using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf] 

118 
unfolding norm_minus_cancel by metis 

119 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

120 
lemma onorm_neg: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)" 
36581  121 
shows "onorm (\<lambda>x.  f x) = onorm f" 
122 
using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]] 

123 
by simp 

124 

125 
lemma onorm_triangle: 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

126 
assumes lf: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space)" and lg: "linear g" 
36581  127 
shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g" 
128 
apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format]) 

129 
apply (rule order_trans) 

130 
apply (rule norm_triangle_ineq) 

131 
apply (simp add: distrib) 

132 
apply (rule add_mono) 

133 
apply (rule onorm(1)[OF lf]) 

134 
apply (rule onorm(1)[OF lg]) 

135 
done 

136 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

137 
lemma onorm_triangle_le: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) <= e 
36581  138 
\<Longrightarrow> onorm(\<lambda>x. f x + g x) <= e" 
139 
apply (rule order_trans) 

140 
apply (rule onorm_triangle) 

141 
apply assumption+ 

142 
done 

143 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

144 
lemma onorm_triangle_lt: "linear (f::'n::euclidean_space \<Rightarrow> 'm::euclidean_space) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) < e 
36581  145 
==> onorm(\<lambda>x. f x + g x) < e" 
146 
apply (rule order_le_less_trans) 

147 
apply (rule onorm_triangle) 

148 
by assumption+ 

149 

150 
end 