src/HOL/Analysis/Linear_Algebra.thy
changeset 67962 0acdcd8f4ba1
parent 67685 bdff8bf0a75b
child 67982 7643b005b29a
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Apr 05 06:15:02 2018 +0000
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Apr 06 17:34:50 2018 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4  
     1.5  subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
     1.6  
     1.7 -definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
     1.8 +definition%important hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
     1.9    where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"
    1.10  
    1.11  lemma hull_same: "S s \<Longrightarrow> S hull s = s"
    1.12 @@ -109,10 +109,10 @@
    1.13  
    1.14  subsection \<open>Linear functions.\<close>
    1.15  
    1.16 -lemma linear_iff:
    1.17 +lemma%important linear_iff:
    1.18    "linear f \<longleftrightarrow> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>R x) = c *\<^sub>R f x)"
    1.19    (is "linear f \<longleftrightarrow> ?rhs")
    1.20 -proof
    1.21 +proof%unimportant
    1.22    assume "linear f"
    1.23    then interpret f: linear f .
    1.24    show "?rhs" by (simp add: f.add f.scaleR)
    1.25 @@ -230,11 +230,11 @@
    1.26  
    1.27  subsection \<open>Subspaces of vector spaces\<close>
    1.28  
    1.29 -definition (in real_vector) subspace :: "'a set \<Rightarrow> bool"
    1.30 +definition%important (in real_vector) subspace :: "'a set \<Rightarrow> bool"
    1.31    where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S)"
    1.32  
    1.33 -definition (in real_vector) "span S = (subspace hull S)"
    1.34 -definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
    1.35 +definition%important (in real_vector) "span S = (subspace hull S)"
    1.36 +definition%important (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
    1.37  abbreviation (in real_vector) "independent s \<equiv> \<not> dependent s"
    1.38  
    1.39  text \<open>Closure properties of subspaces.\<close>
    1.40 @@ -284,7 +284,7 @@
    1.41   apply (metis add.assoc add.left_commute)
    1.42  using scaleR_add_right by blast
    1.43  
    1.44 -subsection \<open>Properties of span\<close>
    1.45 +subsection%unimportant \<open>Properties of span\<close>
    1.46  
    1.47  lemma (in real_vector) span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B"
    1.48    by (metis span_def hull_mono)
    1.49 @@ -1351,7 +1351,7 @@
    1.50  qed
    1.51  
    1.52  
    1.53 -subsection \<open>More interesting properties of the norm.\<close>
    1.54 +subsection%unimportant \<open>More interesting properties of the norm.\<close>
    1.55  
    1.56  lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
    1.57    by auto
    1.58 @@ -1498,11 +1498,11 @@
    1.59  
    1.60  subsection \<open>Orthogonality.\<close>
    1.61  
    1.62 +definition%important (in real_inner) "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
    1.63 +
    1.64  context real_inner
    1.65  begin
    1.66  
    1.67 -definition "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
    1.68 -
    1.69  lemma orthogonal_self: "orthogonal x x \<longleftrightarrow> x = 0"
    1.70    by (simp add: orthogonal_def)
    1.71  
    1.72 @@ -1567,7 +1567,7 @@
    1.73  
    1.74  subsection \<open>Bilinear functions.\<close>
    1.75  
    1.76 -definition "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
    1.77 +definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
    1.78  
    1.79  lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
    1.80    by (simp add: bilinear_def linear_iff)
    1.81 @@ -1630,7 +1630,7 @@
    1.82  
    1.83  subsection \<open>Adjoints.\<close>
    1.84  
    1.85 -definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
    1.86 +definition%important "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
    1.87  
    1.88  lemma adjoint_unique:
    1.89    assumes "\<forall>x y. inner (f x) y = inner x (g y)"
    1.90 @@ -1701,7 +1701,7 @@
    1.91    by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
    1.92  
    1.93  
    1.94 -subsection \<open>Interlude: Some properties of real sets\<close>
    1.95 +subsection%unimportant \<open>Interlude: Some properties of real sets\<close>
    1.96  
    1.97  lemma seq_mono_lemma:
    1.98    assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
    1.99 @@ -1754,11 +1754,11 @@
   1.100  subsection \<open>Archimedean properties and useful consequences\<close>
   1.101  
   1.102  text\<open>Bernoulli's inequality\<close>
   1.103 -proposition Bernoulli_inequality:
   1.104 +proposition%important Bernoulli_inequality:
   1.105    fixes x :: real
   1.106    assumes "-1 \<le> x"
   1.107      shows "1 + n * x \<le> (1 + x) ^ n"
   1.108 -proof (induct n)
   1.109 +proof%unimportant (induct n)
   1.110    case 0
   1.111    then show ?case by simp
   1.112  next
   1.113 @@ -1844,7 +1844,7 @@
   1.114    done
   1.115  
   1.116  
   1.117 -subsection \<open>Euclidean Spaces as Typeclass\<close>
   1.118 +subsection%unimportant \<open>Euclidean Spaces as Typeclass\<close>
   1.119  
   1.120  lemma independent_Basis: "independent Basis"
   1.121    unfolding dependent_def
   1.122 @@ -1905,7 +1905,7 @@
   1.123  qed
   1.124  
   1.125  
   1.126 -subsection \<open>Linearity and Bilinearity continued\<close>
   1.127 +subsection%unimportant \<open>Linearity and Bilinearity continued\<close>
   1.128  
   1.129  lemma linear_bounded:
   1.130    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   1.131 @@ -2074,7 +2074,7 @@
   1.132  by (metis linear_imp_has_derivative differentiable_def)
   1.133  
   1.134  
   1.135 -subsection \<open>We continue.\<close>
   1.136 +subsection%unimportant \<open>We continue.\<close>
   1.137  
   1.138  lemma independent_bound:
   1.139    fixes S :: "'a::euclidean_space set"
   1.140 @@ -2879,7 +2879,7 @@
   1.141  
   1.142  subsection \<open>Infinity norm\<close>
   1.143  
   1.144 -definition "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
   1.145 +definition%important "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
   1.146  
   1.147  lemma infnorm_set_image:
   1.148    fixes x :: "'a::euclidean_space"
   1.149 @@ -3115,7 +3115,7 @@
   1.150  
   1.151  subsection \<open>Collinearity\<close>
   1.152  
   1.153 -definition collinear :: "'a::real_vector set \<Rightarrow> bool"
   1.154 +definition%important collinear :: "'a::real_vector set \<Rightarrow> bool"
   1.155    where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
   1.156  
   1.157  lemma collinear_alt: