| changeset 44133 | 691c52e900ca |
| parent 41959 | b460124855b8 |
| child 50526 | 899c9c4e4a4c |
| 44132:0f35a870ecf1 | 44133:691c52e900ca |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Operator Norm *} |
5 header {* Operator Norm *} |
6 |
6 |
7 theory Operator_Norm |
7 theory Operator_Norm |
8 imports Euclidean_Space |
8 imports Linear_Algebra |
9 begin |
9 begin |
10 |
10 |
11 definition "onorm f = Sup {norm (f x)| x. norm x = 1}" |
11 definition "onorm f = Sup {norm (f x)| x. norm x = 1}" |
12 |
12 |
13 lemma norm_bound_generalize: |
13 lemma norm_bound_generalize: |