initial version of Analysis document
authornipkow
Wed Dec 06 15:17:05 2017 +0100 (6 weeks ago)
changeset 67143db609ac2c307
parent 67142 fa1173288322
child 67144 cef9a1514ed0
initial version of Analysis document
src/Doc/ROOT
src/HOL/Analysis/L2_Norm.thy
src/HOL/Analysis/document/root.tex
     1.1 --- a/src/Doc/ROOT	Wed Dec 06 09:11:27 2017 +0100
     1.2 +++ b/src/Doc/ROOT	Wed Dec 06 15:17:05 2017 +0100
     1.3 @@ -1,5 +1,19 @@
     1.4  chapter Doc
     1.5  
     1.6 +session Analysis (doc) in "../HOL/Analysis" = HOL +
     1.7 +  options [document_variants = "analysis",
     1.8 +    (*skip_proofs = true,*) quick_and_dirty,
     1.9 +    document = pdf, document_output = "output",
    1.10 +    document_variants = "document=-proof,-ML,+important,-unimportant",
    1.11 +    document_tags = "unimportant"]
    1.12 +  sessions
    1.13 +    "HOL-Library"
    1.14 +    "HOL-Computational_Algebra"
    1.15 +  theories
    1.16 +    Analysis
    1.17 +  document_files
    1.18 +    "root.tex"
    1.19 +
    1.20  session Classes (doc) in "Classes" = HOL +
    1.21    options [document_variants = "classes", quick_and_dirty]
    1.22    theories [document = false] Setup
     2.1 --- a/src/HOL/Analysis/L2_Norm.thy	Wed Dec 06 09:11:27 2017 +0100
     2.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Wed Dec 06 15:17:05 2017 +0100
     2.3 @@ -2,13 +2,13 @@
     2.4      Author:     Brian Huffman, Portland State University
     2.5  *)
     2.6  
     2.7 -section \<open>Square root of sum of squares\<close>
     2.8 +section \<open>L2 Norm\<close>
     2.9  
    2.10  theory L2_Norm
    2.11  imports Complex_Main
    2.12  begin
    2.13  
    2.14 -definition
    2.15 +definition %important
    2.16    "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
    2.17  
    2.18  lemma setL2_cong:
    2.19 @@ -74,9 +74,9 @@
    2.20    unfolding setL2_def
    2.21    by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
    2.22  
    2.23 -lemma setL2_triangle_ineq:
    2.24 +lemma %important setL2_triangle_ineq:
    2.25    shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
    2.26 -proof (cases "finite A")
    2.27 +proof %unimportant (cases "finite A")
    2.28    case False
    2.29    thus ?thesis by simp
    2.30  next
     3.1 --- a/src/HOL/Analysis/document/root.tex	Wed Dec 06 09:11:27 2017 +0100
     3.2 +++ b/src/HOL/Analysis/document/root.tex	Wed Dec 06 15:17:05 2017 +0100
     3.3 @@ -15,7 +15,7 @@
     3.4  
     3.5  \begin{document}
     3.6  
     3.7 -\title{Multivariate Analysis}
     3.8 +\title{Analysis}
     3.9  \maketitle
    3.10  
    3.11  \tableofcontents