src/HOL/Analysis/Linear_Algebra.thy
author immler
Wed May 02 13:49:38 2018 +0200 (12 months ago)
changeset 68072 493b818e8e10
parent 67982 7643b005b29a
child 68073 fad29d2a17a5
permissions -rw-r--r--
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
hoelzl@63627
     1
(*  Title:      HOL/Analysis/Linear_Algebra.thy
huffman@44133
     2
    Author:     Amine Chaieb, University of Cambridge
huffman@44133
     3
*)
huffman@44133
     4
wenzelm@60420
     5
section \<open>Elementary linear algebra on Euclidean spaces\<close>
huffman@44133
     6
huffman@44133
     7
theory Linear_Algebra
huffman@44133
     8
imports
huffman@44133
     9
  Euclidean_Space
wenzelm@66453
    10
  "HOL-Library.Infinite_Set"
huffman@44133
    11
begin
huffman@44133
    12
hoelzl@63886
    13
lemma linear_simps:
hoelzl@63886
    14
  assumes "bounded_linear f"
hoelzl@63886
    15
  shows
hoelzl@63886
    16
    "f (a + b) = f a + f b"
hoelzl@63886
    17
    "f (a - b) = f a - f b"
hoelzl@63886
    18
    "f 0 = 0"
hoelzl@63886
    19
    "f (- a) = - f a"
hoelzl@63886
    20
    "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
hoelzl@63886
    21
proof -
hoelzl@63886
    22
  interpret f: bounded_linear f by fact
hoelzl@63886
    23
  show "f (a + b) = f a + f b" by (rule f.add)
hoelzl@63886
    24
  show "f (a - b) = f a - f b" by (rule f.diff)
hoelzl@63886
    25
  show "f 0 = 0" by (rule f.zero)
immler@68072
    26
  show "f (- a) = - f a" by (rule f.neg)
immler@68072
    27
  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scale)
hoelzl@63886
    28
qed
hoelzl@63886
    29
hoelzl@63886
    30
lemma bounded_linearI:
hoelzl@63886
    31
  assumes "\<And>x y. f (x + y) = f x + f y"
hoelzl@63886
    32
    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
hoelzl@63886
    33
    and "\<And>x. norm (f x) \<le> norm x * K"
hoelzl@63886
    34
  shows "bounded_linear f"
hoelzl@63886
    35
  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
hoelzl@63886
    36
huffman@44133
    37
lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
wenzelm@49522
    38
proof -
wenzelm@53406
    39
  have eq: "{f x |x. x\<in> UNIV} = f ` UNIV"
wenzelm@53406
    40
    by auto
huffman@44133
    41
  show ?thesis unfolding eq
huffman@44133
    42
    apply (rule finite_imageI)
huffman@44133
    43
    apply (rule finite)
huffman@44133
    44
    done
huffman@44133
    45
qed
huffman@44133
    46
wenzelm@53406
    47
immler@67962
    48
subsection%unimportant \<open>More interesting properties of the norm.\<close>
hoelzl@63050
    49
hoelzl@63050
    50
notation inner (infix "\<bullet>" 70)
hoelzl@63050
    51
nipkow@67399
    52
text\<open>Equality of vectors in terms of @{term "(\<bullet>)"} products.\<close>
hoelzl@63050
    53
hoelzl@63050
    54
lemma linear_componentwise:
hoelzl@63050
    55
  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
hoelzl@63050
    56
  assumes lf: "linear f"
hoelzl@63050
    57
  shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
hoelzl@63050
    58
proof -
immler@68072
    59
  interpret linear f by fact
hoelzl@63050
    60
  have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
nipkow@64267
    61
    by (simp add: inner_sum_left)
hoelzl@63050
    62
  then show ?thesis
immler@68072
    63
    by (simp add: euclidean_representation sum[symmetric] scale[symmetric])
hoelzl@63050
    64
qed
hoelzl@63050
    65
hoelzl@63050
    66
lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x"
hoelzl@63050
    67
  (is "?lhs \<longleftrightarrow> ?rhs")
hoelzl@63050
    68
proof
hoelzl@63050
    69
  assume ?lhs
hoelzl@63050
    70
  then show ?rhs by simp
hoelzl@63050
    71
next
hoelzl@63050
    72
  assume ?rhs
hoelzl@63050
    73
  then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0"
hoelzl@63050
    74
    by simp
hoelzl@63050
    75
  then have "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0"
hoelzl@63050
    76
    by (simp add: inner_diff inner_commute)
hoelzl@63050
    77
  then have "(x - y) \<bullet> (x - y) = 0"
hoelzl@63050
    78
    by (simp add: field_simps inner_diff inner_commute)
hoelzl@63050
    79
  then show "x = y" by simp
hoelzl@63050
    80
qed
hoelzl@63050
    81
hoelzl@63050
    82
lemma norm_triangle_half_r:
hoelzl@63050
    83
  "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
hoelzl@63050
    84
  using dist_triangle_half_r unfolding dist_norm[symmetric] by auto
hoelzl@63050
    85
hoelzl@63050
    86
lemma norm_triangle_half_l:
hoelzl@63050
    87
  assumes "norm (x - y) < e / 2"
hoelzl@63050
    88
    and "norm (x' - y) < e / 2"
hoelzl@63050
    89
  shows "norm (x - x') < e"
hoelzl@63050
    90
  using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]]
hoelzl@63050
    91
  unfolding dist_norm[symmetric] .
hoelzl@63050
    92
hoelzl@63050
    93
lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
hoelzl@63050
    94
  by (rule norm_triangle_ineq [THEN order_trans])
hoelzl@63050
    95
hoelzl@63050
    96
lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
hoelzl@63050
    97
  by (rule norm_triangle_ineq [THEN le_less_trans])
hoelzl@63050
    98
lp15@66420
    99
lemma abs_triangle_half_r:
lp15@66420
   100
  fixes y :: "'a::linordered_field"
lp15@66420
   101
  shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e"
lp15@66420
   102
  by linarith
lp15@66420
   103
lp15@66420
   104
lemma abs_triangle_half_l:
lp15@66420
   105
  fixes y :: "'a::linordered_field"
lp15@66420
   106
  assumes "abs (x - y) < e / 2"
lp15@66420
   107
    and "abs (x' - y) < e / 2"
lp15@66420
   108
  shows "abs (x - x') < e"
lp15@66420
   109
  using assms by linarith
lp15@66420
   110
nipkow@64267
   111
lemma sum_clauses:
nipkow@64267
   112
  shows "sum f {} = 0"
nipkow@64267
   113
    and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
hoelzl@63050
   114
  by (auto simp add: insert_absorb)
hoelzl@63050
   115
nipkow@64267
   116
lemma sum_norm_bound:
hoelzl@63050
   117
  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
lp15@64773
   118
  assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
lp15@64773
   119
  shows "norm (sum f S) \<le> of_nat (card S)*K"
nipkow@64267
   120
  using sum_norm_le[OF K] sum_constant[symmetric]
hoelzl@63050
   121
  by simp
hoelzl@63050
   122
nipkow@64267
   123
lemma sum_group:
hoelzl@63050
   124
  assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
nipkow@64267
   125
  shows "sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) T = sum g S"
nipkow@64267
   126
  apply (subst sum_image_gen[OF fS, of g f])
nipkow@64267
   127
  apply (rule sum.mono_neutral_right[OF fT fST])
nipkow@64267
   128
  apply (auto intro: sum.neutral)
hoelzl@63050
   129
  done
hoelzl@63050
   130
hoelzl@63050
   131
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
hoelzl@63050
   132
proof
hoelzl@63050
   133
  assume "\<forall>x. x \<bullet> y = x \<bullet> z"
hoelzl@63050
   134
  then have "\<forall>x. x \<bullet> (y - z) = 0"
hoelzl@63050
   135
    by (simp add: inner_diff)
hoelzl@63050
   136
  then have "(y - z) \<bullet> (y - z) = 0" ..
hoelzl@63050
   137
  then show "y = z" by simp
hoelzl@63050
   138
qed simp
hoelzl@63050
   139
hoelzl@63050
   140
lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y"
hoelzl@63050
   141
proof
hoelzl@63050
   142
  assume "\<forall>z. x \<bullet> z = y \<bullet> z"
hoelzl@63050
   143
  then have "\<forall>z. (x - y) \<bullet> z = 0"
hoelzl@63050
   144
    by (simp add: inner_diff)
hoelzl@63050
   145
  then have "(x - y) \<bullet> (x - y) = 0" ..
hoelzl@63050
   146
  then show "x = y" by simp
hoelzl@63050
   147
qed simp
hoelzl@63050
   148
hoelzl@63050
   149
hoelzl@63050
   150
subsection \<open>Orthogonality.\<close>
hoelzl@63050
   151
immler@67962
   152
definition%important (in real_inner) "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
immler@67962
   153
hoelzl@63050
   154
context real_inner
hoelzl@63050
   155
begin
hoelzl@63050
   156
lp15@63072
   157
lemma orthogonal_self: "orthogonal x x \<longleftrightarrow> x = 0"
lp15@63072
   158
  by (simp add: orthogonal_def)
lp15@63072
   159
hoelzl@63050
   160
lemma orthogonal_clauses:
hoelzl@63050
   161
  "orthogonal a 0"
hoelzl@63050
   162
  "orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)"
hoelzl@63050
   163
  "orthogonal a x \<Longrightarrow> orthogonal a (- x)"
hoelzl@63050
   164
  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x + y)"
hoelzl@63050
   165
  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x - y)"
hoelzl@63050
   166
  "orthogonal 0 a"
hoelzl@63050
   167
  "orthogonal x a \<Longrightarrow> orthogonal (c *\<^sub>R x) a"
hoelzl@63050
   168
  "orthogonal x a \<Longrightarrow> orthogonal (- x) a"
hoelzl@63050
   169
  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
hoelzl@63050
   170
  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
hoelzl@63050
   171
  unfolding orthogonal_def inner_add inner_diff by auto
hoelzl@63050
   172
hoelzl@63050
   173
end
hoelzl@63050
   174
hoelzl@63050
   175
lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
hoelzl@63050
   176
  by (simp add: orthogonal_def inner_commute)
hoelzl@63050
   177
lp15@63114
   178
lemma orthogonal_scaleR [simp]: "c \<noteq> 0 \<Longrightarrow> orthogonal (c *\<^sub>R x) = orthogonal x"
lp15@63114
   179
  by (rule ext) (simp add: orthogonal_def)
lp15@63114
   180
lp15@63114
   181
lemma pairwise_ortho_scaleR:
lp15@63114
   182
    "pairwise (\<lambda>i j. orthogonal (f i) (g j)) B
lp15@63114
   183
    \<Longrightarrow> pairwise (\<lambda>i j. orthogonal (a i *\<^sub>R f i) (a j *\<^sub>R g j)) B"
lp15@63114
   184
  by (auto simp: pairwise_def orthogonal_clauses)
lp15@63114
   185
lp15@63114
   186
lemma orthogonal_rvsum:
nipkow@64267
   187
    "\<lbrakk>finite s; \<And>y. y \<in> s \<Longrightarrow> orthogonal x (f y)\<rbrakk> \<Longrightarrow> orthogonal x (sum f s)"
lp15@63114
   188
  by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
lp15@63114
   189
lp15@63114
   190
lemma orthogonal_lvsum:
nipkow@64267
   191
    "\<lbrakk>finite s; \<And>x. x \<in> s \<Longrightarrow> orthogonal (f x) y\<rbrakk> \<Longrightarrow> orthogonal (sum f s) y"
lp15@63114
   192
  by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
lp15@63114
   193
lp15@63114
   194
lemma norm_add_Pythagorean:
lp15@63114
   195
  assumes "orthogonal a b"
lp15@63114
   196
    shows "norm(a + b) ^ 2 = norm a ^ 2 + norm b ^ 2"
lp15@63114
   197
proof -
lp15@63114
   198
  from assms have "(a - (0 - b)) \<bullet> (a - (0 - b)) = a \<bullet> a - (0 - b \<bullet> b)"
lp15@63114
   199
    by (simp add: algebra_simps orthogonal_def inner_commute)
lp15@63114
   200
  then show ?thesis
lp15@63114
   201
    by (simp add: power2_norm_eq_inner)
lp15@63114
   202
qed
lp15@63114
   203
nipkow@64267
   204
lemma norm_sum_Pythagorean:
lp15@63114
   205
  assumes "finite I" "pairwise (\<lambda>i j. orthogonal (f i) (f j)) I"
nipkow@64267
   206
    shows "(norm (sum f I))\<^sup>2 = (\<Sum>i\<in>I. (norm (f i))\<^sup>2)"
lp15@63114
   207
using assms
lp15@63114
   208
proof (induction I rule: finite_induct)
lp15@63114
   209
  case empty then show ?case by simp
lp15@63114
   210
next
lp15@63114
   211
  case (insert x I)
nipkow@64267
   212
  then have "orthogonal (f x) (sum f I)"
lp15@63114
   213
    by (metis pairwise_insert orthogonal_rvsum)
lp15@63114
   214
  with insert show ?case
lp15@63114
   215
    by (simp add: pairwise_insert norm_add_Pythagorean)
lp15@63114
   216
qed
lp15@63114
   217
hoelzl@63050
   218
hoelzl@63050
   219
subsection \<open>Bilinear functions.\<close>
hoelzl@63050
   220
immler@67962
   221
definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
hoelzl@63050
   222
hoelzl@63050
   223
lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
hoelzl@63050
   224
  by (simp add: bilinear_def linear_iff)
hoelzl@63050
   225
hoelzl@63050
   226
lemma bilinear_radd: "bilinear h \<Longrightarrow> h x (y + z) = h x y + h x z"
hoelzl@63050
   227
  by (simp add: bilinear_def linear_iff)
hoelzl@63050
   228
hoelzl@63050
   229
lemma bilinear_lmul: "bilinear h \<Longrightarrow> h (c *\<^sub>R x) y = c *\<^sub>R h x y"
hoelzl@63050
   230
  by (simp add: bilinear_def linear_iff)
hoelzl@63050
   231
hoelzl@63050
   232
lemma bilinear_rmul: "bilinear h \<Longrightarrow> h x (c *\<^sub>R y) = c *\<^sub>R h x y"
hoelzl@63050
   233
  by (simp add: bilinear_def linear_iff)
hoelzl@63050
   234
hoelzl@63050
   235
lemma bilinear_lneg: "bilinear h \<Longrightarrow> h (- x) y = - h x y"
hoelzl@63050
   236
  by (drule bilinear_lmul [of _ "- 1"]) simp
hoelzl@63050
   237
hoelzl@63050
   238
lemma bilinear_rneg: "bilinear h \<Longrightarrow> h x (- y) = - h x y"
hoelzl@63050
   239
  by (drule bilinear_rmul [of _ _ "- 1"]) simp
hoelzl@63050
   240
hoelzl@63050
   241
lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
hoelzl@63050
   242
  using add_left_imp_eq[of x y 0] by auto
hoelzl@63050
   243
hoelzl@63050
   244
lemma bilinear_lzero:
hoelzl@63050
   245
  assumes "bilinear h"
hoelzl@63050
   246
  shows "h 0 x = 0"
hoelzl@63050
   247
  using bilinear_ladd [OF assms, of 0 0 x] by (simp add: eq_add_iff field_simps)
hoelzl@63050
   248
hoelzl@63050
   249
lemma bilinear_rzero:
hoelzl@63050
   250
  assumes "bilinear h"
hoelzl@63050
   251
  shows "h x 0 = 0"
hoelzl@63050
   252
  using bilinear_radd [OF assms, of x 0 0 ] by (simp add: eq_add_iff field_simps)
hoelzl@63050
   253
hoelzl@63050
   254
lemma bilinear_lsub: "bilinear h \<Longrightarrow> h (x - y) z = h x z - h y z"
hoelzl@63050
   255
  using bilinear_ladd [of h x "- y"] by (simp add: bilinear_lneg)
hoelzl@63050
   256
hoelzl@63050
   257
lemma bilinear_rsub: "bilinear h \<Longrightarrow> h z (x - y) = h z x - h z y"
hoelzl@63050
   258
  using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg)
hoelzl@63050
   259
nipkow@64267
   260
lemma bilinear_sum:
immler@68072
   261
  assumes "bilinear h"
nipkow@64267
   262
  shows "h (sum f S) (sum g T) = sum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
hoelzl@63050
   263
proof -
immler@68072
   264
  interpret l: linear "\<lambda>x. h x y" for y using assms by (simp add: bilinear_def)
immler@68072
   265
  interpret r: linear "\<lambda>y. h x y" for x using assms by (simp add: bilinear_def)
nipkow@64267
   266
  have "h (sum f S) (sum g T) = sum (\<lambda>x. h (f x) (sum g T)) S"
immler@68072
   267
    by (simp add: l.sum)
nipkow@64267
   268
  also have "\<dots> = sum (\<lambda>x. sum (\<lambda>y. h (f x) (g y)) T) S"
immler@68072
   269
    by (rule sum.cong) (simp_all add: r.sum)
hoelzl@63050
   270
  finally show ?thesis
nipkow@64267
   271
    unfolding sum.cartesian_product .
hoelzl@63050
   272
qed
hoelzl@63050
   273
hoelzl@63050
   274
hoelzl@63050
   275
subsection \<open>Adjoints.\<close>
hoelzl@63050
   276
immler@67962
   277
definition%important "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
hoelzl@63050
   278
hoelzl@63050
   279
lemma adjoint_unique:
hoelzl@63050
   280
  assumes "\<forall>x y. inner (f x) y = inner x (g y)"
hoelzl@63050
   281
  shows "adjoint f = g"
hoelzl@63050
   282
  unfolding adjoint_def
hoelzl@63050
   283
proof (rule some_equality)
hoelzl@63050
   284
  show "\<forall>x y. inner (f x) y = inner x (g y)"
hoelzl@63050
   285
    by (rule assms)
hoelzl@63050
   286
next
hoelzl@63050
   287
  fix h
hoelzl@63050
   288
  assume "\<forall>x y. inner (f x) y = inner x (h y)"
hoelzl@63050
   289
  then have "\<forall>x y. inner x (g y) = inner x (h y)"
hoelzl@63050
   290
    using assms by simp
hoelzl@63050
   291
  then have "\<forall>x y. inner x (g y - h y) = 0"
hoelzl@63050
   292
    by (simp add: inner_diff_right)
hoelzl@63050
   293
  then have "\<forall>y. inner (g y - h y) (g y - h y) = 0"
hoelzl@63050
   294
    by simp
hoelzl@63050
   295
  then have "\<forall>y. h y = g y"
hoelzl@63050
   296
    by simp
hoelzl@63050
   297
  then show "h = g" by (simp add: ext)
hoelzl@63050
   298
qed
hoelzl@63050
   299
hoelzl@63050
   300
text \<open>TODO: The following lemmas about adjoints should hold for any
wenzelm@63680
   301
  Hilbert space (i.e. complete inner product space).
wenzelm@63680
   302
  (see \<^url>\<open>http://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
hoelzl@63050
   303
\<close>
hoelzl@63050
   304
hoelzl@63050
   305
lemma adjoint_works:
hoelzl@63050
   306
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
hoelzl@63050
   307
  assumes lf: "linear f"
hoelzl@63050
   308
  shows "x \<bullet> adjoint f y = f x \<bullet> y"
hoelzl@63050
   309
proof -
immler@68072
   310
  interpret linear f by fact
hoelzl@63050
   311
  have "\<forall>y. \<exists>w. \<forall>x. f x \<bullet> y = x \<bullet> w"
hoelzl@63050
   312
  proof (intro allI exI)
hoelzl@63050
   313
    fix y :: "'m" and x
hoelzl@63050
   314
    let ?w = "(\<Sum>i\<in>Basis. (f i \<bullet> y) *\<^sub>R i) :: 'n"
hoelzl@63050
   315
    have "f x \<bullet> y = f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i) \<bullet> y"
hoelzl@63050
   316
      by (simp add: euclidean_representation)
hoelzl@63050
   317
    also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<bullet> y"
immler@68072
   318
      by (simp add: sum scale)
hoelzl@63050
   319
    finally show "f x \<bullet> y = x \<bullet> ?w"
nipkow@64267
   320
      by (simp add: inner_sum_left inner_sum_right mult.commute)
hoelzl@63050
   321
  qed
hoelzl@63050
   322
  then show ?thesis
hoelzl@63050
   323
    unfolding adjoint_def choice_iff
hoelzl@63050
   324
    by (intro someI2_ex[where Q="\<lambda>f'. x \<bullet> f' y = f x \<bullet> y"]) auto
hoelzl@63050
   325
qed
hoelzl@63050
   326
hoelzl@63050
   327
lemma adjoint_clauses:
hoelzl@63050
   328
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
hoelzl@63050
   329
  assumes lf: "linear f"
hoelzl@63050
   330
  shows "x \<bullet> adjoint f y = f x \<bullet> y"
hoelzl@63050
   331
    and "adjoint f y \<bullet> x = y \<bullet> f x"
hoelzl@63050
   332
  by (simp_all add: adjoint_works[OF lf] inner_commute)
hoelzl@63050
   333
hoelzl@63050
   334
lemma adjoint_linear:
hoelzl@63050
   335
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
hoelzl@63050
   336
  assumes lf: "linear f"
hoelzl@63050
   337
  shows "linear (adjoint f)"
hoelzl@63050
   338
  by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]
hoelzl@63050
   339
    adjoint_clauses[OF lf] inner_distrib)
hoelzl@63050
   340
hoelzl@63050
   341
lemma adjoint_adjoint:
hoelzl@63050
   342
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
hoelzl@63050
   343
  assumes lf: "linear f"
hoelzl@63050
   344
  shows "adjoint (adjoint f) = f"
hoelzl@63050
   345
  by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
hoelzl@63050
   346
hoelzl@63050
   347
immler@67962
   348
subsection%unimportant \<open>Interlude: Some properties of real sets\<close>
hoelzl@63050
   349
hoelzl@63050
   350
lemma seq_mono_lemma:
hoelzl@63050
   351
  assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
hoelzl@63050
   352
    and "\<forall>n \<ge> m. e n \<le> e m"
hoelzl@63050
   353
  shows "\<forall>n \<ge> m. d n < e m"
hoelzl@63050
   354
  using assms
hoelzl@63050
   355
  apply auto
hoelzl@63050
   356
  apply (erule_tac x="n" in allE)
hoelzl@63050
   357
  apply (erule_tac x="n" in allE)
hoelzl@63050
   358
  apply auto
hoelzl@63050
   359
  done
hoelzl@63050
   360
hoelzl@63050
   361
lemma infinite_enumerate:
hoelzl@63050
   362
  assumes fS: "infinite S"
eberlm@66447
   363
  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. r n \<in> S)"
eberlm@66447
   364
  unfolding strict_mono_def
hoelzl@63050
   365
  using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
hoelzl@63050
   366
hoelzl@63050
   367
lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
hoelzl@63050
   368
  apply auto
hoelzl@63050
   369
  apply (rule_tac x="d/2" in exI)
hoelzl@63050
   370
  apply auto
hoelzl@63050
   371
  done
hoelzl@63050
   372
wenzelm@67443
   373
lemma approachable_lt_le2:  \<comment> \<open>like the above, but pushes aside an extra formula\<close>
hoelzl@63050
   374
    "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
hoelzl@63050
   375
  apply auto
hoelzl@63050
   376
  apply (rule_tac x="d/2" in exI, auto)
hoelzl@63050
   377
  done
hoelzl@63050
   378
hoelzl@63050
   379
lemma triangle_lemma:
hoelzl@63050
   380
  fixes x y z :: real
hoelzl@63050
   381
  assumes x: "0 \<le> x"
hoelzl@63050
   382
    and y: "0 \<le> y"
hoelzl@63050
   383
    and z: "0 \<le> z"
hoelzl@63050
   384
    and xy: "x\<^sup>2 \<le> y\<^sup>2 + z\<^sup>2"
hoelzl@63050
   385
  shows "x \<le> y + z"
hoelzl@63050
   386
proof -
hoelzl@63050
   387
  have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2"
hoelzl@63050
   388
    using z y by simp
hoelzl@63050
   389
  with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2"
hoelzl@63050
   390
    by (simp add: power2_eq_square field_simps)
hoelzl@63050
   391
  from y z have yz: "y + z \<ge> 0"
hoelzl@63050
   392
    by arith
hoelzl@63050
   393
  from power2_le_imp_le[OF th yz] show ?thesis .
hoelzl@63050
   394
qed
hoelzl@63050
   395
hoelzl@63050
   396
hoelzl@63050
   397
hoelzl@63050
   398
subsection \<open>Archimedean properties and useful consequences\<close>
hoelzl@63050
   399
hoelzl@63050
   400
text\<open>Bernoulli's inequality\<close>
immler@67962
   401
proposition%important Bernoulli_inequality:
hoelzl@63050
   402
  fixes x :: real
hoelzl@63050
   403
  assumes "-1 \<le> x"
hoelzl@63050
   404
    shows "1 + n * x \<le> (1 + x) ^ n"
immler@67962
   405
proof%unimportant (induct n)
hoelzl@63050
   406
  case 0
hoelzl@63050
   407
  then show ?case by simp
hoelzl@63050
   408
next
hoelzl@63050
   409
  case (Suc n)
hoelzl@63050
   410
  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
hoelzl@63050
   411
    by (simp add: algebra_simps)
hoelzl@63050
   412
  also have "... = (1 + x) * (1 + n*x)"
hoelzl@63050
   413
    by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
hoelzl@63050
   414
  also have "... \<le> (1 + x) ^ Suc n"
hoelzl@63050
   415
    using Suc.hyps assms mult_left_mono by fastforce
hoelzl@63050
   416
  finally show ?case .
hoelzl@63050
   417
qed
hoelzl@63050
   418
hoelzl@63050
   419
corollary Bernoulli_inequality_even:
hoelzl@63050
   420
  fixes x :: real
hoelzl@63050
   421
  assumes "even n"
hoelzl@63050
   422
    shows "1 + n * x \<le> (1 + x) ^ n"
hoelzl@63050
   423
proof (cases "-1 \<le> x \<or> n=0")
hoelzl@63050
   424
  case True
hoelzl@63050
   425
  then show ?thesis
hoelzl@63050
   426
    by (auto simp: Bernoulli_inequality)
hoelzl@63050
   427
next
hoelzl@63050
   428
  case False
hoelzl@63050
   429
  then have "real n \<ge> 1"
hoelzl@63050
   430
    by simp
hoelzl@63050
   431
  with False have "n * x \<le> -1"
hoelzl@63050
   432
    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
hoelzl@63050
   433
  then have "1 + n * x \<le> 0"
hoelzl@63050
   434
    by auto
hoelzl@63050
   435
  also have "... \<le> (1 + x) ^ n"
hoelzl@63050
   436
    using assms
hoelzl@63050
   437
    using zero_le_even_power by blast
hoelzl@63050
   438
  finally show ?thesis .
hoelzl@63050
   439
qed
hoelzl@63050
   440
hoelzl@63050
   441
corollary real_arch_pow:
hoelzl@63050
   442
  fixes x :: real
hoelzl@63050
   443
  assumes x: "1 < x"
hoelzl@63050
   444
  shows "\<exists>n. y < x^n"
hoelzl@63050
   445
proof -
hoelzl@63050
   446
  from x have x0: "x - 1 > 0"
hoelzl@63050
   447
    by arith
hoelzl@63050
   448
  from reals_Archimedean3[OF x0, rule_format, of y]
hoelzl@63050
   449
  obtain n :: nat where n: "y < real n * (x - 1)" by metis
hoelzl@63050
   450
  from x0 have x00: "x- 1 \<ge> -1" by arith
hoelzl@63050
   451
  from Bernoulli_inequality[OF x00, of n] n
hoelzl@63050
   452
  have "y < x^n" by auto
hoelzl@63050
   453
  then show ?thesis by metis
hoelzl@63050
   454
qed
hoelzl@63050
   455
hoelzl@63050
   456
corollary real_arch_pow_inv:
hoelzl@63050
   457
  fixes x y :: real
hoelzl@63050
   458
  assumes y: "y > 0"
hoelzl@63050
   459
    and x1: "x < 1"
hoelzl@63050
   460
  shows "\<exists>n. x^n < y"
hoelzl@63050
   461
proof (cases "x > 0")
hoelzl@63050
   462
  case True
hoelzl@63050
   463
  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
hoelzl@63050
   464
  from real_arch_pow[OF ix, of "1/y"]
hoelzl@63050
   465
  obtain n where n: "1/y < (1/x)^n" by blast
hoelzl@63050
   466
  then show ?thesis using y \<open>x > 0\<close>
hoelzl@63050
   467
    by (auto simp add: field_simps)
hoelzl@63050
   468
next
hoelzl@63050
   469
  case False
hoelzl@63050
   470
  with y x1 show ?thesis
hoelzl@63050
   471
    apply auto
hoelzl@63050
   472
    apply (rule exI[where x=1])
hoelzl@63050
   473
    apply auto
hoelzl@63050
   474
    done
hoelzl@63050
   475
qed
hoelzl@63050
   476
hoelzl@63050
   477
lemma forall_pos_mono:
hoelzl@63050
   478
  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
hoelzl@63050
   479
    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
hoelzl@63050
   480
  by (metis real_arch_inverse)
hoelzl@63050
   481
hoelzl@63050
   482
lemma forall_pos_mono_1:
hoelzl@63050
   483
  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
hoelzl@63050
   484
    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
hoelzl@63050
   485
  apply (rule forall_pos_mono)
hoelzl@63050
   486
  apply auto
hoelzl@63050
   487
  apply (metis Suc_pred of_nat_Suc)
hoelzl@63050
   488
  done
hoelzl@63050
   489
hoelzl@63050
   490
immler@67962
   491
subsection%unimportant \<open>Euclidean Spaces as Typeclass\<close>
huffman@44133
   492
hoelzl@50526
   493
lemma independent_Basis: "independent Basis"
immler@68072
   494
  by (rule independent_Basis)
hoelzl@50526
   495
huffman@53939
   496
lemma span_Basis [simp]: "span Basis = UNIV"
immler@68072
   497
  by (rule span_Basis)
huffman@44133
   498
hoelzl@50526
   499
lemma in_span_Basis: "x \<in> span Basis"
hoelzl@50526
   500
  unfolding span_Basis ..
hoelzl@50526
   501
wenzelm@53406
   502
immler@67962
   503
subsection%unimportant \<open>Linearity and Bilinearity continued\<close>
huffman@44133
   504
huffman@44133
   505
lemma linear_bounded:
wenzelm@56444
   506
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
huffman@44133
   507
  assumes lf: "linear f"
huffman@44133
   508
  shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
huffman@53939
   509
proof
immler@68072
   510
  interpret linear f by fact
hoelzl@50526
   511
  let ?B = "\<Sum>b\<in>Basis. norm (f b)"
huffman@53939
   512
  show "\<forall>x. norm (f x) \<le> ?B * norm x"
huffman@53939
   513
  proof
wenzelm@53406
   514
    fix x :: 'a
hoelzl@50526
   515
    let ?g = "\<lambda>b. (x \<bullet> b) *\<^sub>R f b"
hoelzl@50526
   516
    have "norm (f x) = norm (f (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b))"
hoelzl@50526
   517
      unfolding euclidean_representation ..
nipkow@64267
   518
    also have "\<dots> = norm (sum ?g Basis)"
immler@68072
   519
      by (simp add: sum scale)
nipkow@64267
   520
    finally have th0: "norm (f x) = norm (sum ?g Basis)" .
lp15@64773
   521
    have th: "norm (?g i) \<le> norm (f i) * norm x" if "i \<in> Basis" for i
lp15@64773
   522
    proof -
lp15@64773
   523
      from Basis_le_norm[OF that, of x]
huffman@53939
   524
      show "norm (?g i) \<le> norm (f i) * norm x"
wenzelm@49663
   525
        unfolding norm_scaleR
haftmann@57512
   526
        apply (subst mult.commute)
wenzelm@49663
   527
        apply (rule mult_mono)
wenzelm@49663
   528
        apply (auto simp add: field_simps)
wenzelm@53406
   529
        done
huffman@53939
   530
    qed
nipkow@64267
   531
    from sum_norm_le[of _ ?g, OF th]
huffman@53939
   532
    show "norm (f x) \<le> ?B * norm x"
nipkow@64267
   533
      unfolding th0 sum_distrib_right by metis
huffman@53939
   534
  qed
huffman@44133
   535
qed
huffman@44133
   536
huffman@44133
   537
lemma linear_conv_bounded_linear:
huffman@44133
   538
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
huffman@44133
   539
  shows "linear f \<longleftrightarrow> bounded_linear f"
huffman@44133
   540
proof
huffman@44133
   541
  assume "linear f"
huffman@53939
   542
  then interpret f: linear f .
huffman@44133
   543
  show "bounded_linear f"
huffman@44133
   544
  proof
huffman@44133
   545
    have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
wenzelm@60420
   546
      using \<open>linear f\<close> by (rule linear_bounded)
wenzelm@49522
   547
    then show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
haftmann@57512
   548
      by (simp add: mult.commute)
huffman@44133
   549
  qed
huffman@44133
   550
next
huffman@44133
   551
  assume "bounded_linear f"
huffman@44133
   552
  then interpret f: bounded_linear f .
huffman@53939
   553
  show "linear f" ..
huffman@53939
   554
qed
huffman@53939
   555
paulson@61518
   556
lemmas linear_linear = linear_conv_bounded_linear[symmetric]
paulson@61518
   557
huffman@53939
   558
lemma linear_bounded_pos:
wenzelm@56444
   559
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
huffman@53939
   560
  assumes lf: "linear f"
lp15@67982
   561
 obtains B where "B > 0" "\<And>x. norm (f x) \<le> B * norm x"
huffman@53939
   562
proof -
huffman@53939
   563
  have "\<exists>B > 0. \<forall>x. norm (f x) \<le> norm x * B"
huffman@53939
   564
    using lf unfolding linear_conv_bounded_linear
huffman@53939
   565
    by (rule bounded_linear.pos_bounded)
lp15@67982
   566
  with that show ?thesis
lp15@67982
   567
    by (auto simp: mult.commute)
huffman@44133
   568
qed
huffman@44133
   569
lp15@67982
   570
lemma linear_invertible_bounded_below_pos:
lp15@67982
   571
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
lp15@67982
   572
  assumes "linear f" "linear g" "g \<circ> f = id"
lp15@67982
   573
  obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
lp15@67982
   574
proof -
lp15@67982
   575
  obtain B where "B > 0" and B: "\<And>x. norm (g x) \<le> B * norm x"
lp15@67982
   576
    using linear_bounded_pos [OF \<open>linear g\<close>] by blast
lp15@67982
   577
  show thesis
lp15@67982
   578
  proof
lp15@67982
   579
    show "0 < 1/B"
lp15@67982
   580
      by (simp add: \<open>B > 0\<close>)
lp15@67982
   581
    show "1/B * norm x \<le> norm (f x)" for x
lp15@67982
   582
    proof -
lp15@67982
   583
      have "1/B * norm x = 1/B * norm (g (f x))"
lp15@67982
   584
        using assms by (simp add: pointfree_idE)
lp15@67982
   585
      also have "\<dots> \<le> norm (f x)"
lp15@67982
   586
        using B [of "f x"] by (simp add: \<open>B > 0\<close> mult.commute pos_divide_le_eq)
lp15@67982
   587
      finally show ?thesis .
lp15@67982
   588
    qed
lp15@67982
   589
  qed
lp15@67982
   590
qed
lp15@67982
   591
lp15@67982
   592
lemma linear_inj_bounded_below_pos:
lp15@67982
   593
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
lp15@67982
   594
  assumes "linear f" "inj f"
lp15@67982
   595
  obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
immler@68072
   596
  using linear_injective_left_inverse [OF assms]
immler@68072
   597
    linear_invertible_bounded_below_pos assms by blast
lp15@67982
   598
wenzelm@49522
   599
lemma bounded_linearI':
wenzelm@56444
   600
  fixes f ::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
wenzelm@53406
   601
  assumes "\<And>x y. f (x + y) = f x + f y"
wenzelm@53406
   602
    and "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
wenzelm@49522
   603
  shows "bounded_linear f"
immler@68072
   604
  using assms linearI linear_conv_bounded_linear by blast
huffman@44133
   605
huffman@44133
   606
lemma bilinear_bounded:
wenzelm@56444
   607
  fixes h :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::real_normed_vector"
huffman@44133
   608
  assumes bh: "bilinear h"
huffman@44133
   609
  shows "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
hoelzl@50526
   610
proof (clarify intro!: exI[of _ "\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)"])
wenzelm@53406
   611
  fix x :: 'm
wenzelm@53406
   612
  fix y :: 'n
nipkow@64267
   613
  have "norm (h x y) = norm (h (sum (\<lambda>i. (x \<bullet> i) *\<^sub>R i) Basis) (sum (\<lambda>i. (y \<bullet> i) *\<^sub>R i) Basis))"
wenzelm@53406
   614
    apply (subst euclidean_representation[where 'a='m])
wenzelm@53406
   615
    apply (subst euclidean_representation[where 'a='n])
hoelzl@50526
   616
    apply rule
hoelzl@50526
   617
    done
nipkow@64267
   618
  also have "\<dots> = norm (sum (\<lambda> (i,j). h ((x \<bullet> i) *\<^sub>R i) ((y \<bullet> j) *\<^sub>R j)) (Basis \<times> Basis))"
immler@68072
   619
    unfolding bilinear_sum[OF bh] ..
hoelzl@50526
   620
  finally have th: "norm (h x y) = \<dots>" .
hoelzl@50526
   621
  show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
nipkow@64267
   622
    apply (auto simp add: sum_distrib_right th sum.cartesian_product)
nipkow@64267
   623
    apply (rule sum_norm_le)
wenzelm@53406
   624
    apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
wenzelm@53406
   625
      field_simps simp del: scaleR_scaleR)
wenzelm@53406
   626
    apply (rule mult_mono)
wenzelm@53406
   627
    apply (auto simp add: zero_le_mult_iff Basis_le_norm)
wenzelm@53406
   628
    apply (rule mult_mono)
wenzelm@53406
   629
    apply (auto simp add: zero_le_mult_iff Basis_le_norm)
wenzelm@53406
   630
    done
huffman@44133
   631
qed
huffman@44133
   632
huffman@44133
   633
lemma bilinear_conv_bounded_bilinear:
huffman@44133
   634
  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
huffman@44133
   635
  shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
huffman@44133
   636
proof
huffman@44133
   637
  assume "bilinear h"
huffman@44133
   638
  show "bounded_bilinear h"
huffman@44133
   639
  proof
wenzelm@53406
   640
    fix x y z
wenzelm@53406
   641
    show "h (x + y) z = h x z + h y z"
wenzelm@60420
   642
      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff by simp
huffman@44133
   643
  next
wenzelm@53406
   644
    fix x y z
wenzelm@53406
   645
    show "h x (y + z) = h x y + h x z"
wenzelm@60420
   646
      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff by simp
huffman@44133
   647
  next
wenzelm@53406
   648
    fix r x y
wenzelm@53406
   649
    show "h (scaleR r x) y = scaleR r (h x y)"
wenzelm@60420
   650
      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
huffman@44133
   651
      by simp
huffman@44133
   652
  next
wenzelm@53406
   653
    fix r x y
wenzelm@53406
   654
    show "h x (scaleR r y) = scaleR r (h x y)"
wenzelm@60420
   655
      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
huffman@44133
   656
      by simp
huffman@44133
   657
  next
huffman@44133
   658
    have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
wenzelm@60420
   659
      using \<open>bilinear h\<close> by (rule bilinear_bounded)
wenzelm@49522
   660
    then show "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
haftmann@57514
   661
      by (simp add: ac_simps)
huffman@44133
   662
  qed
huffman@44133
   663
next
huffman@44133
   664
  assume "bounded_bilinear h"
huffman@44133
   665
  then interpret h: bounded_bilinear h .
huffman@44133
   666
  show "bilinear h"
huffman@44133
   667
    unfolding bilinear_def linear_conv_bounded_linear
wenzelm@49522
   668
    using h.bounded_linear_left h.bounded_linear_right by simp
huffman@44133
   669
qed
huffman@44133
   670
huffman@53939
   671
lemma bilinear_bounded_pos:
wenzelm@56444
   672
  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
huffman@53939
   673
  assumes bh: "bilinear h"
huffman@53939
   674
  shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
huffman@53939
   675
proof -
huffman@53939
   676
  have "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> norm x * norm y * B"
huffman@53939
   677
    using bh [unfolded bilinear_conv_bounded_bilinear]
huffman@53939
   678
    by (rule bounded_bilinear.pos_bounded)
huffman@53939
   679
  then show ?thesis
haftmann@57514
   680
    by (simp only: ac_simps)
huffman@53939
   681
qed
huffman@53939
   682
immler@68072
   683
lemma bounded_linear_imp_has_derivative: "bounded_linear f \<Longrightarrow> (f has_derivative f) net"
immler@68072
   684
  by (auto simp add: has_derivative_def linear_diff linear_linear linear_def
immler@68072
   685
      dest: bounded_linear.linear)
lp15@63469
   686
lp15@63469
   687
lemma linear_imp_has_derivative:
lp15@63469
   688
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
lp15@63469
   689
  shows "linear f \<Longrightarrow> (f has_derivative f) net"
immler@68072
   690
  by (simp add: bounded_linear_imp_has_derivative linear_conv_bounded_linear)
lp15@63469
   691
lp15@63469
   692
lemma bounded_linear_imp_differentiable: "bounded_linear f \<Longrightarrow> f differentiable net"
lp15@63469
   693
  using bounded_linear_imp_has_derivative differentiable_def by blast
lp15@63469
   694
lp15@63469
   695
lemma linear_imp_differentiable:
lp15@63469
   696
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
lp15@63469
   697
  shows "linear f \<Longrightarrow> f differentiable net"
immler@68072
   698
  by (metis linear_imp_has_derivative differentiable_def)
lp15@63469
   699
wenzelm@49522
   700
immler@67962
   701
subsection%unimportant \<open>We continue.\<close>
huffman@44133
   702
huffman@44133
   703
lemma independent_bound:
wenzelm@53716
   704
  fixes S :: "'a::euclidean_space set"
wenzelm@53716
   705
  shows "independent S \<Longrightarrow> finite S \<and> card S \<le> DIM('a)"
immler@68072
   706
  by (metis dim_subset_UNIV finiteI_independent dim_span_eq_card_independent)
immler@68072
   707
immler@68072
   708
lemmas independent_imp_finite = finiteI_independent
huffman@44133
   709
lp15@61609
   710
corollary
paulson@60303
   711
  fixes S :: "'a::euclidean_space set"
paulson@60303
   712
  assumes "independent S"
immler@68072
   713
  shows independent_card_le:"card S \<le> DIM('a)"
immler@68072
   714
  using assms independent_bound by auto
lp15@63075
   715
wenzelm@49663
   716
lemma dependent_biggerset:
wenzelm@56444
   717
  fixes S :: "'a::euclidean_space set"
wenzelm@56444
   718
  shows "(finite S \<Longrightarrow> card S > DIM('a)) \<Longrightarrow> dependent S"
huffman@44133
   719
  by (metis independent_bound not_less)
huffman@44133
   720
wenzelm@60420
   721
text \<open>Picking an orthogonal replacement for a spanning set.\<close>
huffman@44133
   722
wenzelm@53406
   723
lemma vector_sub_project_orthogonal:
wenzelm@53406
   724
  fixes b x :: "'a::euclidean_space"
wenzelm@53406
   725
  shows "b \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *\<^sub>R b) = 0"
huffman@44133
   726
  unfolding inner_simps by auto
huffman@44133
   727
huffman@44528
   728
lemma pairwise_orthogonal_insert:
huffman@44528
   729
  assumes "pairwise orthogonal S"
wenzelm@49522
   730
    and "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
huffman@44528
   731
  shows "pairwise orthogonal (insert x S)"
huffman@44528
   732
  using assms unfolding pairwise_def
huffman@44528
   733
  by (auto simp add: orthogonal_commute)
huffman@44528
   734
huffman@44133
   735
lemma basis_orthogonal:
wenzelm@53406
   736
  fixes B :: "'a::real_inner set"
huffman@44133
   737
  assumes fB: "finite B"
huffman@44133
   738
  shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C"
huffman@44133
   739
  (is " \<exists>C. ?P B C")
wenzelm@49522
   740
  using fB
wenzelm@49522
   741
proof (induct rule: finite_induct)
wenzelm@49522
   742
  case empty
wenzelm@53406
   743
  then show ?case
wenzelm@53406
   744
    apply (rule exI[where x="{}"])
wenzelm@53406
   745
    apply (auto simp add: pairwise_def)
wenzelm@53406
   746
    done
huffman@44133
   747
next
wenzelm@49522
   748
  case (insert a B)
wenzelm@60420
   749
  note fB = \<open>finite B\<close> and aB = \<open>a \<notin> B\<close>
wenzelm@60420
   750
  from \<open>\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C\<close>
huffman@44133
   751
  obtain C where C: "finite C" "card C \<le> card B"
huffman@44133
   752
    "span C = span B" "pairwise orthogonal C" by blast
nipkow@64267
   753
  let ?a = "a - sum (\<lambda>x. (x \<bullet> a / (x \<bullet> x)) *\<^sub>R x) C"
huffman@44133
   754
  let ?C = "insert ?a C"
wenzelm@53406
   755
  from C(1) have fC: "finite ?C"
wenzelm@53406
   756
    by simp
wenzelm@49522
   757
  from fB aB C(1,2) have cC: "card ?C \<le> card (insert a B)"
wenzelm@49522
   758
    by (simp add: card_insert_if)
wenzelm@53406
   759
  {
wenzelm@53406
   760
    fix x k
wenzelm@49522
   761
    have th0: "\<And>(a::'a) b c. a - (b - c) = c + (a - b)"
wenzelm@49522
   762
      by (simp add: field_simps)
huffman@44133
   763
    have "x - k *\<^sub>R (a - (\<Sum>x\<in>C. (x \<bullet> a / (x \<bullet> x)) *\<^sub>R x)) \<in> span C \<longleftrightarrow> x - k *\<^sub>R a \<in> span C"
huffman@44133
   764
      apply (simp only: scaleR_right_diff_distrib th0)
huffman@44133
   765
      apply (rule span_add_eq)
immler@68072
   766
      apply (rule span_scale)
nipkow@64267
   767
      apply (rule span_sum)
immler@68072
   768
      apply (rule span_scale)
immler@68072
   769
      apply (rule span_base)
wenzelm@49522
   770
      apply assumption
wenzelm@53406
   771
      done
wenzelm@53406
   772
  }
huffman@44133
   773
  then have SC: "span ?C = span (insert a B)"
huffman@44133
   774
    unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto
wenzelm@53406
   775
  {
wenzelm@53406
   776
    fix y
wenzelm@53406
   777
    assume yC: "y \<in> C"
wenzelm@53406
   778
    then have Cy: "C = insert y (C - {y})"
wenzelm@53406
   779
      by blast
wenzelm@53406
   780
    have fth: "finite (C - {y})"
wenzelm@53406
   781
      using C by simp
huffman@44528
   782
    have "orthogonal ?a y"
huffman@44528
   783
      unfolding orthogonal_def
nipkow@64267
   784
      unfolding inner_diff inner_sum_left right_minus_eq
nipkow@64267
   785
      unfolding sum.remove [OF \<open>finite C\<close> \<open>y \<in> C\<close>]
huffman@44528
   786
      apply (clarsimp simp add: inner_commute[of y a])
nipkow@64267
   787
      apply (rule sum.neutral)
huffman@44528
   788
      apply clarsimp
huffman@44528
   789
      apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
wenzelm@60420
   790
      using \<open>y \<in> C\<close> by auto
wenzelm@53406
   791
  }
wenzelm@60420
   792
  with \<open>pairwise orthogonal C\<close> have CPO: "pairwise orthogonal ?C"
huffman@44528
   793
    by (rule pairwise_orthogonal_insert)
wenzelm@53406
   794
  from fC cC SC CPO have "?P (insert a B) ?C"
wenzelm@53406
   795
    by blast
huffman@44133
   796
  then show ?case by blast
huffman@44133
   797
qed
huffman@44133
   798
huffman@44133
   799
lemma orthogonal_basis_exists:
huffman@44133
   800
  fixes V :: "('a::euclidean_space) set"
immler@68072
   801
  shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and>
immler@68072
   802
  (card B = dim V) \<and> pairwise orthogonal B"
wenzelm@49663
   803
proof -
wenzelm@49522
   804
  from basis_exists[of V] obtain B where
wenzelm@53406
   805
    B: "B \<subseteq> V" "independent B" "V \<subseteq> span B" "card B = dim V"
wenzelm@53406
   806
    by blast
wenzelm@53406
   807
  from B have fB: "finite B" "card B = dim V"
wenzelm@53406
   808
    using independent_bound by auto
huffman@44133
   809
  from basis_orthogonal[OF fB(1)] obtain C where
wenzelm@53406
   810
    C: "finite C" "card C \<le> card B" "span C = span B" "pairwise orthogonal C"
wenzelm@53406
   811
    by blast
wenzelm@53406
   812
  from C B have CSV: "C \<subseteq> span V"
immler@68072
   813
    by (metis span_superset span_mono subset_trans)
wenzelm@53406
   814
  from span_mono[OF B(3)] C have SVC: "span V \<subseteq> span C"
wenzelm@53406
   815
    by (simp add: span_span)
huffman@44133
   816
  from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB
wenzelm@53406
   817
  have iC: "independent C"
huffman@44133
   818
    by (simp add: dim_span)
wenzelm@53406
   819
  from C fB have "card C \<le> dim V"
wenzelm@53406
   820
    by simp
wenzelm@53406
   821
  moreover have "dim V \<le> card C"
wenzelm@53406
   822
    using span_card_ge_dim[OF CSV SVC C(1)]
immler@68072
   823
    by simp
wenzelm@53406
   824
  ultimately have CdV: "card C = dim V"
wenzelm@53406
   825
    using C(1) by simp
wenzelm@53406
   826
  from C B CSV CdV iC show ?thesis
wenzelm@53406
   827
    by auto
huffman@44133
   828
qed
huffman@44133
   829
wenzelm@60420
   830
text \<open>Low-dimensional subset is in a hyperplane (weak orthogonal complement).\<close>
huffman@44133
   831
wenzelm@49522
   832
lemma span_not_univ_orthogonal:
wenzelm@53406
   833
  fixes S :: "'a::euclidean_space set"
huffman@44133
   834
  assumes sU: "span S \<noteq> UNIV"
wenzelm@56444
   835
  shows "\<exists>a::'a. a \<noteq> 0 \<and> (\<forall>x \<in> span S. a \<bullet> x = 0)"
wenzelm@49522
   836
proof -
wenzelm@53406
   837
  from sU obtain a where a: "a \<notin> span S"
wenzelm@53406
   838
    by blast
huffman@44133
   839
  from orthogonal_basis_exists obtain B where
immler@68072
   840
    B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B"
immler@68072
   841
    "card B = dim S" "pairwise orthogonal B"
huffman@44133
   842
    by blast
wenzelm@53406
   843
  from B have fB: "finite B" "card B = dim S"
wenzelm@53406
   844
    using independent_bound by auto
huffman@44133
   845
  from span_mono[OF B(2)] span_mono[OF B(3)]
wenzelm@53406
   846
  have sSB: "span S = span B"
wenzelm@53406
   847
    by (simp add: span_span)
nipkow@64267
   848
  let ?a = "a - sum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B"
nipkow@64267
   849
  have "sum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B \<in> span S"
huffman@44133
   850
    unfolding sSB
nipkow@64267
   851
    apply (rule span_sum)
immler@68072
   852
    apply (rule span_scale)
immler@68072
   853
    apply (rule span_base)
wenzelm@49522
   854
    apply assumption
wenzelm@49522
   855
    done
wenzelm@53406
   856
  with a have a0:"?a  \<noteq> 0"
wenzelm@53406
   857
    by auto
huffman@44133
   858
  have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
wenzelm@49522
   859
  proof (rule span_induct')
wenzelm@49522
   860
    show "subspace {x. ?a \<bullet> x = 0}"
wenzelm@49522
   861
      by (auto simp add: subspace_def inner_add)
wenzelm@49522
   862
  next
wenzelm@53406
   863
    {
wenzelm@53406
   864
      fix x
wenzelm@53406
   865
      assume x: "x \<in> B"
wenzelm@53406
   866
      from x have B': "B = insert x (B - {x})"
wenzelm@53406
   867
        by blast
wenzelm@53406
   868
      have fth: "finite (B - {x})"
wenzelm@53406
   869
        using fB by simp
huffman@44133
   870
      have "?a \<bullet> x = 0"
wenzelm@53406
   871
        apply (subst B')
wenzelm@53406
   872
        using fB fth
nipkow@64267
   873
        unfolding sum_clauses(2)[OF fth]
huffman@44133
   874
        apply simp unfolding inner_simps
nipkow@64267
   875
        apply (clarsimp simp add: inner_add inner_sum_left)
nipkow@64267
   876
        apply (rule sum.neutral, rule ballI)
wenzelm@63170
   877
        apply (simp only: inner_commute)
wenzelm@49711
   878
        apply (auto simp add: x field_simps
wenzelm@49711
   879
          intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
wenzelm@53406
   880
        done
wenzelm@53406
   881
    }
wenzelm@53406
   882
    then show "\<forall>x \<in> B. ?a \<bullet> x = 0"
wenzelm@53406
   883
      by blast
huffman@44133
   884
  qed
wenzelm@53406
   885
  with a0 show ?thesis
wenzelm@53406
   886
    unfolding sSB by (auto intro: exI[where x="?a"])
huffman@44133
   887
qed
huffman@44133
   888
huffman@44133
   889
lemma span_not_univ_subset_hyperplane:
wenzelm@53406
   890
  fixes S :: "'a::euclidean_space set"
wenzelm@53406
   891
  assumes SU: "span S \<noteq> UNIV"
huffman@44133
   892
  shows "\<exists> a. a \<noteq>0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
huffman@44133
   893
  using span_not_univ_orthogonal[OF SU] by auto
huffman@44133
   894
wenzelm@49663
   895
lemma lowdim_subset_hyperplane:
wenzelm@53406
   896
  fixes S :: "'a::euclidean_space set"
huffman@44133
   897
  assumes d: "dim S < DIM('a)"
wenzelm@56444
   898
  shows "\<exists>a::'a. a \<noteq> 0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
wenzelm@49522
   899
proof -
wenzelm@53406
   900
  {
wenzelm@53406
   901
    assume "span S = UNIV"
wenzelm@53406
   902
    then have "dim (span S) = dim (UNIV :: ('a) set)"
wenzelm@53406
   903
      by simp
wenzelm@53406
   904
    then have "dim S = DIM('a)"
immler@68072
   905
      by (metis Euclidean_Space.dim_UNIV dim_span)
wenzelm@53406
   906
    with d have False by arith
wenzelm@53406
   907
  }
wenzelm@53406
   908
  then have th: "span S \<noteq> UNIV"
wenzelm@53406
   909
    by blast
huffman@44133
   910
  from span_not_univ_subset_hyperplane[OF th] show ?thesis .
huffman@44133
   911
qed
huffman@44133
   912
huffman@44133
   913
lemma linear_eq_stdbasis:
wenzelm@56444
   914
  fixes f :: "'a::euclidean_space \<Rightarrow> _"
wenzelm@56444
   915
  assumes lf: "linear f"
wenzelm@49663
   916
    and lg: "linear g"
immler@68072
   917
    and fg: "\<And>b. b \<in> Basis \<Longrightarrow> f b = g b"
huffman@44133
   918
  shows "f = g"
immler@68072
   919
  using linear_eq_on_span[OF lf lg, of Basis] fg
immler@68072
   920
  by auto
immler@68072
   921
huffman@44133
   922
wenzelm@60420
   923
text \<open>Similar results for bilinear functions.\<close>
huffman@44133
   924
huffman@44133
   925
lemma bilinear_eq:
huffman@44133
   926
  assumes bf: "bilinear f"
wenzelm@49522
   927
    and bg: "bilinear g"
wenzelm@53406
   928
    and SB: "S \<subseteq> span B"
wenzelm@53406
   929
    and TC: "T \<subseteq> span C"
wenzelm@49522
   930
    and fg: "\<forall>x\<in> B. \<forall>y\<in> C. f x y = g x y"
huffman@44133
   931
  shows "\<forall>x\<in>S. \<forall>y\<in>T. f x y = g x y "
wenzelm@49663
   932
proof -
huffman@44170
   933
  let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
huffman@44133
   934
  from bf bg have sp: "subspace ?P"
huffman@53600
   935
    unfolding bilinear_def linear_iff subspace_def bf bg
immler@68072
   936
    by (auto simp add: span_zero bilinear_lzero[OF bf] bilinear_lzero[OF bg]
immler@68072
   937
        span_add Ball_def
wenzelm@49663
   938
      intro: bilinear_ladd[OF bf])
huffman@44133
   939
huffman@44133
   940
  have "\<forall>x \<in> span B. \<forall>y\<in> span C. f x y = g x y"
huffman@44170
   941
    apply (rule span_induct' [OF _ sp])
huffman@44133
   942
    apply (rule ballI)
huffman@44170
   943
    apply (rule span_induct')
huffman@44170
   944
    apply (simp add: fg)
huffman@44133
   945
    apply (auto simp add: subspace_def)
huffman@53600
   946
    using bf bg unfolding bilinear_def linear_iff
immler@68072
   947
      apply (auto simp add: span_zero bilinear_rzero[OF bf] bilinear_rzero[OF bg]
immler@68072
   948
        span_add Ball_def
wenzelm@49663
   949
      intro: bilinear_ladd[OF bf])
wenzelm@49522
   950
    done
wenzelm@53406
   951
  then show ?thesis
wenzelm@53406
   952
    using SB TC by auto
huffman@44133
   953
qed
huffman@44133
   954
wenzelm@49522
   955
lemma bilinear_eq_stdbasis:
wenzelm@53406
   956
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> _"
huffman@44133
   957
  assumes bf: "bilinear f"
wenzelm@49522
   958
    and bg: "bilinear g"
hoelzl@50526
   959
    and fg: "\<forall>i\<in>Basis. \<forall>j\<in>Basis. f i j = g i j"
huffman@44133
   960
  shows "f = g"
hoelzl@50526
   961
  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
huffman@44133
   962
wenzelm@60420
   963
subsection \<open>Infinity norm\<close>
huffman@44133
   964
immler@67962
   965
definition%important "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
huffman@44133
   966
huffman@44133
   967
lemma infnorm_set_image:
wenzelm@53716
   968
  fixes x :: "'a::euclidean_space"
wenzelm@56444
   969
  shows "{\<bar>x \<bullet> i\<bar> |i. i \<in> Basis} = (\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
hoelzl@50526
   970
  by blast
huffman@44133
   971
wenzelm@53716
   972
lemma infnorm_Max:
wenzelm@53716
   973
  fixes x :: "'a::euclidean_space"
wenzelm@56444
   974
  shows "infnorm x = Max ((\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis)"
haftmann@62343
   975
  by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
hoelzl@51475
   976
huffman@44133
   977
lemma infnorm_set_lemma:
wenzelm@53716
   978
  fixes x :: "'a::euclidean_space"
wenzelm@56444
   979
  shows "finite {\<bar>x \<bullet> i\<bar> |i. i \<in> Basis}"
wenzelm@56444
   980
    and "{\<bar>x \<bullet> i\<bar> |i. i \<in> Basis} \<noteq> {}"
huffman@44133
   981
  unfolding infnorm_set_image
huffman@44133
   982
  by auto
huffman@44133
   983
wenzelm@53406
   984
lemma infnorm_pos_le:
wenzelm@53406
   985
  fixes x :: "'a::euclidean_space"
wenzelm@53406
   986
  shows "0 \<le> infnorm x"
hoelzl@51475
   987
  by (simp add: infnorm_Max Max_ge_iff ex_in_conv)
huffman@44133
   988
wenzelm@53406
   989
lemma infnorm_triangle:
wenzelm@53406
   990
  fixes x :: "'a::euclidean_space"
wenzelm@53406
   991
  shows "infnorm (x + y) \<le> infnorm x + infnorm y"
wenzelm@49522
   992
proof -
hoelzl@51475
   993
  have *: "\<And>a b c d :: real. \<bar>a\<bar> \<le> c \<Longrightarrow> \<bar>b\<bar> \<le> d \<Longrightarrow> \<bar>a + b\<bar> \<le> c + d"
hoelzl@51475
   994
    by simp
huffman@44133
   995
  show ?thesis
hoelzl@51475
   996
    by (auto simp: infnorm_Max inner_add_left intro!: *)
huffman@44133
   997
qed
huffman@44133
   998
wenzelm@53406
   999
lemma infnorm_eq_0:
wenzelm@53406
  1000
  fixes x :: "'a::euclidean_space"
wenzelm@53406
  1001
  shows "infnorm x = 0 \<longleftrightarrow> x = 0"
wenzelm@49522
  1002
proof -
hoelzl@51475
  1003
  have "infnorm x \<le> 0 \<longleftrightarrow> x = 0"
hoelzl@51475
  1004
    unfolding infnorm_Max by (simp add: euclidean_all_zero_iff)
hoelzl@51475
  1005
  then show ?thesis
hoelzl@51475
  1006
    using infnorm_pos_le[of x] by simp
huffman@44133
  1007
qed
huffman@44133
  1008
huffman@44133
  1009
lemma infnorm_0: "infnorm 0 = 0"
huffman@44133
  1010
  by (simp add: infnorm_eq_0)
huffman@44133
  1011
huffman@44133
  1012
lemma infnorm_neg: "infnorm (- x) = infnorm x"
huffman@44133
  1013
  unfolding infnorm_def
huffman@44133
  1014
  apply (rule cong[of "Sup" "Sup"])
wenzelm@49522
  1015
  apply blast
wenzelm@49522
  1016
  apply auto
wenzelm@49522
  1017
  done
huffman@44133
  1018
huffman@44133
  1019
lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
wenzelm@49522
  1020
proof -
huffman@44133
  1021
  have "y - x = - (x - y)" by simp
wenzelm@53406
  1022
  then show ?thesis
wenzelm@53406
  1023
    by (metis infnorm_neg)
huffman@44133
  1024
qed
huffman@44133
  1025
wenzelm@53406
  1026
lemma real_abs_sub_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
wenzelm@49522
  1027
proof -
wenzelm@56444
  1028
  have th: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
huffman@44133
  1029
    by arith
huffman@44133
  1030
  from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
huffman@44133
  1031
  have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
huffman@44133
  1032
    "infnorm y \<le> infnorm (x - y) + infnorm x"
huffman@44454
  1033
    by (simp_all add: field_simps infnorm_neg)
wenzelm@53406
  1034
  from th[OF ths] show ?thesis .
huffman@44133
  1035
qed
huffman@44133
  1036
wenzelm@53406
  1037
lemma real_abs_infnorm: "\<bar>infnorm x\<bar> = infnorm x"
huffman@44133
  1038
  using infnorm_pos_le[of x] by arith
huffman@44133
  1039
hoelzl@50526
  1040
lemma Basis_le_infnorm:
wenzelm@53406
  1041
  fixes x :: "'a::euclidean_space"
wenzelm@53406
  1042
  shows "b \<in> Basis \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> infnorm x"
hoelzl@51475
  1043
  by (simp add: infnorm_Max)
huffman@44133
  1044
wenzelm@56444
  1045
lemma infnorm_mul: "infnorm (a *\<^sub>R x) = \<bar>a\<bar> * infnorm x"
hoelzl@51475
  1046
  unfolding infnorm_Max
hoelzl@51475
  1047
proof (safe intro!: Max_eqI)
hoelzl@51475
  1048
  let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
wenzelm@53406
  1049
  {
wenzelm@53406
  1050
    fix b :: 'a
wenzelm@53406
  1051
    assume "b \<in> Basis"
wenzelm@53406
  1052
    then show "\<bar>a *\<^sub>R x \<bullet> b\<bar> \<le> \<bar>a\<bar> * Max ?B"
wenzelm@53406
  1053
      by (simp add: abs_mult mult_left_mono)
wenzelm@53406
  1054
  next
wenzelm@53406
  1055
    from Max_in[of ?B] obtain b where "b \<in> Basis" "Max ?B = \<bar>x \<bullet> b\<bar>"
wenzelm@53406
  1056
      by (auto simp del: Max_in)
wenzelm@53406
  1057
    then show "\<bar>a\<bar> * Max ((\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis) \<in> (\<lambda>i. \<bar>a *\<^sub>R x \<bullet> i\<bar>) ` Basis"
wenzelm@53406
  1058
      by (intro image_eqI[where x=b]) (auto simp: abs_mult)
wenzelm@53406
  1059
  }
hoelzl@51475
  1060
qed simp
hoelzl@51475
  1061
wenzelm@53406
  1062
lemma infnorm_mul_lemma: "infnorm (a *\<^sub>R x) \<le> \<bar>a\<bar> * infnorm x"
hoelzl@51475
  1063
  unfolding infnorm_mul ..
huffman@44133
  1064
huffman@44133
  1065
lemma infnorm_pos_lt: "infnorm x > 0 \<longleftrightarrow> x \<noteq> 0"
huffman@44133
  1066
  using infnorm_pos_le[of x] infnorm_eq_0[of x] by arith
huffman@44133
  1067
wenzelm@60420
  1068
text \<open>Prove that it differs only up to a bound from Euclidean norm.\<close>
huffman@44133
  1069
huffman@44133
  1070
lemma infnorm_le_norm: "infnorm x \<le> norm x"
hoelzl@51475
  1071
  by (simp add: Basis_le_norm infnorm_Max)
hoelzl@50526
  1072
wenzelm@53716
  1073
lemma norm_le_infnorm:
wenzelm@53716
  1074
  fixes x :: "'a::euclidean_space"
wenzelm@53716
  1075
  shows "norm x \<le> sqrt DIM('a) * infnorm x"
wenzelm@49522
  1076
proof -
huffman@44133
  1077
  let ?d = "DIM('a)"
wenzelm@53406
  1078
  have "real ?d \<ge> 0"
wenzelm@53406
  1079
    by simp
wenzelm@53077
  1080
  then have d2: "(sqrt (real ?d))\<^sup>2 = real ?d"
huffman@44133
  1081
    by (auto intro: real_sqrt_pow2)
huffman@44133
  1082
  have th: "sqrt (real ?d) * infnorm x \<ge> 0"
huffman@44133
  1083
    by (simp add: zero_le_mult_iff infnorm_pos_le)
wenzelm@53077
  1084
  have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
huffman@44133
  1085
    unfolding power_mult_distrib d2
wenzelm@53716
  1086
    apply (subst euclidean_inner)
huffman@44133
  1087
    apply (subst power2_abs[symmetric])
nipkow@64267
  1088
    apply (rule order_trans[OF sum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
wenzelm@49663
  1089
    apply (auto simp add: power2_eq_square[symmetric])
huffman@44133
  1090
    apply (subst power2_abs[symmetric])
huffman@44133
  1091
    apply (rule power_mono)
hoelzl@51475
  1092
    apply (auto simp: infnorm_Max)
wenzelm@49522
  1093
    done
huffman@44133
  1094
  from real_le_lsqrt[OF inner_ge_zero th th1]
wenzelm@53406
  1095
  show ?thesis
wenzelm@53406
  1096
    unfolding norm_eq_sqrt_inner id_def .
huffman@44133
  1097
qed
huffman@44133
  1098
huffman@44646
  1099
lemma tendsto_infnorm [tendsto_intros]:
wenzelm@61973
  1100
  assumes "(f \<longlongrightarrow> a) F"
wenzelm@61973
  1101
  shows "((\<lambda>x. infnorm (f x)) \<longlongrightarrow> infnorm a) F"
huffman@44646
  1102
proof (rule tendsto_compose [OF LIM_I assms])
wenzelm@53406
  1103
  fix r :: real
wenzelm@53406
  1104
  assume "r > 0"
wenzelm@49522
  1105
  then show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (infnorm x - infnorm a) < r"
huffman@44646
  1106
    by (metis real_norm_def le_less_trans real_abs_sub_infnorm infnorm_le_norm)
huffman@44646
  1107
qed
huffman@44646
  1108
wenzelm@60420
  1109
text \<open>Equality in Cauchy-Schwarz and triangle inequalities.\<close>
huffman@44133
  1110
wenzelm@53406
  1111
lemma norm_cauchy_schwarz_eq: "x \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
wenzelm@53406
  1112
  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@49522
  1113
proof -
wenzelm@53406
  1114
  {
wenzelm@53406
  1115
    assume h: "x = 0"
wenzelm@53406
  1116
    then have ?thesis by simp
wenzelm@53406
  1117
  }
huffman@44133
  1118
  moreover
wenzelm@53406
  1119
  {
wenzelm@53406
  1120
    assume h: "y = 0"
wenzelm@53406
  1121
    then have ?thesis by simp
wenzelm@53406
  1122
  }
huffman@44133
  1123
  moreover
wenzelm@53406
  1124
  {
wenzelm@53406
  1125
    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
huffman@44133
  1126
    from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
wenzelm@49522
  1127
    have "?rhs \<longleftrightarrow>
wenzelm@49522
  1128
      (norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) -
wenzelm@49522
  1129
        norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) =  0)"
huffman@44133
  1130
      using x y
huffman@44133
  1131
      unfolding inner_simps
haftmann@54230
  1132
      unfolding power2_norm_eq_inner[symmetric] power2_eq_square right_minus_eq
wenzelm@49522
  1133
      apply (simp add: inner_commute)
wenzelm@49522
  1134
      apply (simp add: field_simps)
wenzelm@49522
  1135
      apply metis
wenzelm@49522
  1136
      done
huffman@44133
  1137
    also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
huffman@44133
  1138
      by (simp add: field_simps inner_commute)
huffman@44133
  1139
    also have "\<dots> \<longleftrightarrow> ?lhs" using x y
huffman@44133
  1140
      apply simp
wenzelm@49522
  1141
      apply metis
wenzelm@49522
  1142
      done
wenzelm@53406
  1143
    finally have ?thesis by blast
wenzelm@53406
  1144
  }
huffman@44133
  1145
  ultimately show ?thesis by blast
huffman@44133
  1146
qed
huffman@44133
  1147
huffman@44133
  1148
lemma norm_cauchy_schwarz_abs_eq:
wenzelm@56444
  1149
  "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow>
wenzelm@53716
  1150
    norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm x *\<^sub>R y = - norm y *\<^sub>R x"
wenzelm@53406
  1151
  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@49522
  1152
proof -
wenzelm@56444
  1153
  have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> \<bar>x\<bar> = a \<longleftrightarrow> x = a \<or> x = - a"
wenzelm@53406
  1154
    by arith
huffman@44133
  1155
  have "?rhs \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)"
huffman@44133
  1156
    by simp
wenzelm@53406
  1157
  also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or> (- x) \<bullet> y = norm x * norm y)"
huffman@44133
  1158
    unfolding norm_cauchy_schwarz_eq[symmetric]
huffman@44133
  1159
    unfolding norm_minus_cancel norm_scaleR ..
huffman@44133
  1160
  also have "\<dots> \<longleftrightarrow> ?lhs"
wenzelm@53406
  1161
    unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] inner_simps
wenzelm@53406
  1162
    by auto
huffman@44133
  1163
  finally show ?thesis ..
huffman@44133
  1164
qed
huffman@44133
  1165
huffman@44133
  1166
lemma norm_triangle_eq:
huffman@44133
  1167
  fixes x y :: "'a::real_inner"
wenzelm@53406
  1168
  shows "norm (x + y) = norm x + norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
wenzelm@49522
  1169
proof -
wenzelm@53406
  1170
  {
wenzelm@53406
  1171
    assume x: "x = 0 \<or> y = 0"
wenzelm@53406
  1172
    then have ?thesis
wenzelm@53406
  1173
      by (cases "x = 0") simp_all
wenzelm@53406
  1174
  }
huffman@44133
  1175
  moreover
wenzelm@53406
  1176
  {
wenzelm@53406
  1177
    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
wenzelm@49522
  1178
    then have "norm x \<noteq> 0" "norm y \<noteq> 0"
huffman@44133
  1179
      by simp_all
wenzelm@49522
  1180
    then have n: "norm x > 0" "norm y > 0"
wenzelm@49522
  1181
      using norm_ge_zero[of x] norm_ge_zero[of y] by arith+
wenzelm@53406
  1182
    have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 \<Longrightarrow> a = b + c \<longleftrightarrow> a\<^sup>2 = (b + c)\<^sup>2"
wenzelm@49522
  1183
      by algebra
wenzelm@53077
  1184
    have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
wenzelm@53406
  1185
      apply (rule th)
wenzelm@53406
  1186
      using n norm_ge_zero[of "x + y"]
wenzelm@49522
  1187
      apply arith
wenzelm@49522
  1188
      done
huffman@44133
  1189
    also have "\<dots> \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
huffman@44133
  1190
      unfolding norm_cauchy_schwarz_eq[symmetric]
huffman@44133
  1191
      unfolding power2_norm_eq_inner inner_simps
huffman@44133
  1192
      by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
wenzelm@53406
  1193
    finally have ?thesis .
wenzelm@53406
  1194
  }
huffman@44133
  1195
  ultimately show ?thesis by blast
huffman@44133
  1196
qed
huffman@44133
  1197
wenzelm@49522
  1198
wenzelm@60420
  1199
subsection \<open>Collinearity\<close>
huffman@44133
  1200
immler@67962
  1201
definition%important collinear :: "'a::real_vector set \<Rightarrow> bool"
wenzelm@49522
  1202
  where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
huffman@44133
  1203
lp15@66287
  1204
lemma collinear_alt:
lp15@66287
  1205
     "collinear S \<longleftrightarrow> (\<exists>u v. \<forall>x \<in> S. \<exists>c. x = u + c *\<^sub>R v)" (is "?lhs = ?rhs")
lp15@66287
  1206
proof
lp15@66287
  1207
  assume ?lhs
lp15@66287
  1208
  then show ?rhs
lp15@66287
  1209
    unfolding collinear_def by (metis Groups.add_ac(2) diff_add_cancel)
lp15@66287
  1210
next
lp15@66287
  1211
  assume ?rhs
lp15@66287
  1212
  then obtain u v where *: "\<And>x. x \<in> S \<Longrightarrow> \<exists>c. x = u + c *\<^sub>R v"
lp15@66287
  1213
    by (auto simp: )
lp15@66287
  1214
  have "\<exists>c. x - y = c *\<^sub>R v" if "x \<in> S" "y \<in> S" for x y
lp15@66287
  1215
        by (metis *[OF \<open>x \<in> S\<close>] *[OF \<open>y \<in> S\<close>] scaleR_left.diff add_diff_cancel_left)
lp15@66287
  1216
  then show ?lhs
lp15@66287
  1217
    using collinear_def by blast
lp15@66287
  1218
qed
lp15@66287
  1219
lp15@66287
  1220
lemma collinear:
lp15@66287
  1221
  fixes S :: "'a::{perfect_space,real_vector} set"
lp15@66287
  1222
  shows "collinear S \<longleftrightarrow> (\<exists>u. u \<noteq> 0 \<and> (\<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u))"
lp15@66287
  1223
proof -
lp15@66287
  1224
  have "\<exists>v. v \<noteq> 0 \<and> (\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R v)"
lp15@66287
  1225
    if "\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R u" "u=0" for u
lp15@66287
  1226
  proof -
lp15@66287
  1227
    have "\<forall>x\<in>S. \<forall>y\<in>S. x = y"
lp15@66287
  1228
      using that by auto
lp15@66287
  1229
    moreover
lp15@66287
  1230
    obtain v::'a where "v \<noteq> 0"
lp15@66287
  1231
      using UNIV_not_singleton [of 0] by auto
lp15@66287
  1232
    ultimately have "\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R v"
lp15@66287
  1233
      by auto
lp15@66287
  1234
    then show ?thesis
lp15@66287
  1235
      using \<open>v \<noteq> 0\<close> by blast
lp15@66287
  1236
  qed
lp15@66287
  1237
  then show ?thesis
lp15@66287
  1238
    apply (clarsimp simp: collinear_def)
immler@68072
  1239
    by (metis scaleR_zero_right vector_fraction_eq_iff)
lp15@66287
  1240
qed
lp15@66287
  1241
lp15@63881
  1242
lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S"
lp15@63881
  1243
  by (meson collinear_def subsetCE)
lp15@63881
  1244
paulson@60762
  1245
lemma collinear_empty [iff]: "collinear {}"
wenzelm@53406
  1246
  by (simp add: collinear_def)
huffman@44133
  1247
paulson@60762
  1248
lemma collinear_sing [iff]: "collinear {x}"
huffman@44133
  1249
  by (simp add: collinear_def)
huffman@44133
  1250
paulson@60762
  1251
lemma collinear_2 [iff]: "collinear {x, y}"
huffman@44133
  1252
  apply (simp add: collinear_def)
huffman@44133
  1253
  apply (rule exI[where x="x - y"])
huffman@44133
  1254
  apply auto
huffman@44133
  1255
  apply (rule exI[where x=1], simp)
huffman@44133
  1256
  apply (rule exI[where x="- 1"], simp)
huffman@44133
  1257
  done
huffman@44133
  1258
wenzelm@56444
  1259
lemma collinear_lemma: "collinear {0, x, y} \<longleftrightarrow> x = 0 \<or> y = 0 \<or> (\<exists>c. y = c *\<^sub>R x)"
wenzelm@53406
  1260
  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@49522
  1261
proof -
wenzelm@53406
  1262
  {
wenzelm@53406
  1263
    assume "x = 0 \<or> y = 0"
wenzelm@53406
  1264
    then have ?thesis
wenzelm@53406
  1265
      by (cases "x = 0") (simp_all add: collinear_2 insert_commute)
wenzelm@53406
  1266
  }
huffman@44133
  1267
  moreover
wenzelm@53406
  1268
  {
wenzelm@53406
  1269
    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
wenzelm@53406
  1270
    have ?thesis
wenzelm@53406
  1271
    proof
wenzelm@53406
  1272
      assume h: "?lhs"
wenzelm@49522
  1273
      then obtain u where u: "\<forall> x\<in> {0,x,y}. \<forall>y\<in> {0,x,y}. \<exists>c. x - y = c *\<^sub>R u"
wenzelm@49522
  1274
        unfolding collinear_def by blast
huffman@44133
  1275
      from u[rule_format, of x 0] u[rule_format, of y 0]
huffman@44133
  1276
      obtain cx and cy where
huffman@44133
  1277
        cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
huffman@44133
  1278
        by auto
huffman@44133
  1279
      from cx x have cx0: "cx \<noteq> 0" by auto
huffman@44133
  1280
      from cy y have cy0: "cy \<noteq> 0" by auto
huffman@44133
  1281
      let ?d = "cy / cx"
huffman@44133
  1282
      from cx cy cx0 have "y = ?d *\<^sub>R x"
huffman@44133
  1283
        by simp
wenzelm@53406
  1284
      then show ?rhs using x y by blast
wenzelm@53406
  1285
    next
wenzelm@53406
  1286
      assume h: "?rhs"
wenzelm@53406
  1287
      then obtain c where c: "y = c *\<^sub>R x"
wenzelm@53406
  1288
        using x y by blast
wenzelm@53406
  1289
      show ?lhs
wenzelm@53406
  1290
        unfolding collinear_def c
huffman@44133
  1291
        apply (rule exI[where x=x])
huffman@44133
  1292
        apply auto
huffman@44133
  1293
        apply (rule exI[where x="- 1"], simp)
huffman@44133
  1294
        apply (rule exI[where x= "-c"], simp)
huffman@44133
  1295
        apply (rule exI[where x=1], simp)
huffman@44133
  1296
        apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib)
huffman@44133
  1297
        apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib)
wenzelm@53406
  1298
        done
wenzelm@53406
  1299
    qed
wenzelm@53406
  1300
  }
huffman@44133
  1301
  ultimately show ?thesis by blast
huffman@44133
  1302
qed
huffman@44133
  1303
wenzelm@56444
  1304
lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
wenzelm@49522
  1305
  unfolding norm_cauchy_schwarz_abs_eq
lp15@63075
  1306
  apply (cases "x=0", simp_all)
lp15@63075
  1307
  apply (cases "y=0", simp_all add: insert_commute)
wenzelm@49522
  1308
  unfolding collinear_lemma
wenzelm@49522
  1309
  apply simp
wenzelm@49522
  1310
  apply (subgoal_tac "norm x \<noteq> 0")
wenzelm@49522
  1311
  apply (subgoal_tac "norm y \<noteq> 0")
wenzelm@49522
  1312
  apply (rule iffI)
wenzelm@49522
  1313
  apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x")
wenzelm@49522
  1314
  apply (rule exI[where x="(1/norm x) * norm y"])
wenzelm@49522
  1315
  apply (drule sym)
wenzelm@49522
  1316
  unfolding scaleR_scaleR[symmetric]
wenzelm@49522
  1317
  apply (simp add: field_simps)
wenzelm@49522
  1318
  apply (rule exI[where x="(1/norm x) * - norm y"])
wenzelm@49522
  1319
  apply clarify
wenzelm@49522
  1320
  apply (drule sym)
wenzelm@49522
  1321
  unfolding scaleR_scaleR[symmetric]
wenzelm@49522
  1322
  apply (simp add: field_simps)
wenzelm@49522
  1323
  apply (erule exE)
wenzelm@49522
  1324
  apply (erule ssubst)
wenzelm@49522
  1325
  unfolding scaleR_scaleR
wenzelm@49522
  1326
  unfolding norm_scaleR
wenzelm@49522
  1327
  apply (subgoal_tac "norm x * c = \<bar>c\<bar> * norm x \<or> norm x * c = - \<bar>c\<bar> * norm x")
lp15@55775
  1328
  apply (auto simp add: field_simps)
wenzelm@49522
  1329
  done
wenzelm@49522
  1330
immler@54776
  1331
end