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.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.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.89    assumes "\<forall>x y. inner (f x) y = inner x (g y)"
1.90 @@ -1701,7 +1701,7 @@
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:
```