equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Operator Norm *} |
6 header {* Operator Norm *} |
7 |
7 |
8 theory Operator_Norm |
8 theory Operator_Norm |
9 imports Linear_Algebra |
9 imports Complex_Main |
10 begin |
10 begin |
11 |
11 |
12 text {* This formulation yields zero if @{text 'a} is the trivial vector space. *} |
12 text {* This formulation yields zero if @{text 'a} is the trivial vector space. *} |
13 |
13 |
14 definition onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real" |
14 definition onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real" |