Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/L2_Norm.thy
changeset 67006 b1278ed3cd46
parent 66453 cc19f7ca2ed6
child 67143 db609ac2c307
equal deleted inserted replaced
67005:11fca474d87a 67006:b1278ed3cd46 
     3 *)
 
     3 *)
 
     4 
     4 
     5 section \<open>Square root of sum of squares\<close>
 
     5 section \<open>Square root of sum of squares\<close>
 
     6 
     6 
     7 theory L2_Norm
 
     7 theory L2_Norm
 
     8 imports HOL.NthRoot
 
     8 imports Complex_Main
 
     9 begin
 
     9 begin
 
    10 
    10 
    11 definition
 
    11 definition
 
    12   "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
 
    12   "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
 
    13 
    13
isabelle