src/HOL/Analysis/Linear_Algebra.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69683 8b3458ca0762
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
hoelzl@63627
     1
(*  Title:      HOL/Analysis/Linear_Algebra.thy
huffman@44133
     2
    Author:     Amine Chaieb, University of Cambridge
huffman@44133
     3
*)
huffman@44133
     4
nipkow@69517
     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)
huffman@44133
    28
qed
huffman@44133
    29
lp15@68069
    30
lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x \<in> (UNIV::'a::finite set)}"
lp15@68069
    31
  using finite finite_image_set by blast
huffman@44133
    32
immler@69675
    33
lemma substdbasis_expansion_unique:
immler@69675
    34
  includes inner_syntax
immler@69675
    35
  assumes d: "d \<subseteq> Basis"
immler@69675
    36
  shows "(\<Sum>i\<in>d. f i *\<^sub>R i) = (x::'a::euclidean_space) \<longleftrightarrow>
immler@69675
    37
    (\<forall>i\<in>Basis. (i \<in> d \<longrightarrow> f i = x \<bullet> i) \<and> (i \<notin> d \<longrightarrow> x \<bullet> i = 0))"
immler@69675
    38
proof -
immler@69675
    39
  have *: "\<And>x a b P. x * (if P then a else b) = (if P then x * a else x * b)"
immler@69675
    40
    by auto
immler@69675
    41
  have **: "finite d"
immler@69675
    42
    by (auto intro: finite_subset[OF assms])
immler@69675
    43
  have ***: "\<And>i. i \<in> Basis \<Longrightarrow> (\<Sum>i\<in>d. f i *\<^sub>R i) \<bullet> i = (\<Sum>x\<in>d. if x = i then f x else 0)"
immler@69675
    44
    using d
immler@69675
    45
    by (auto intro!: sum.cong simp: inner_Basis inner_sum_left)
immler@69675
    46
  show ?thesis
immler@69675
    47
    unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***)
immler@69675
    48
qed
immler@69675
    49
immler@69675
    50
lemma independent_substdbasis: "d \<subseteq> Basis \<Longrightarrow> independent d"
immler@69675
    51
  by (rule independent_mono[OF independent_Basis])
immler@69675
    52
immler@69675
    53
lemma sum_not_0: "sum f A \<noteq> 0 \<Longrightarrow> \<exists>a \<in> A. f a \<noteq> 0"
immler@69675
    54
  by (rule ccontr) auto
immler@69675
    55
immler@69675
    56
lemma subset_translation_eq [simp]:
immler@69675
    57
    fixes a :: "'a::real_vector" shows "(+) a ` s \<subseteq> (+) a ` t \<longleftrightarrow> s \<subseteq> t"
immler@69675
    58
  by auto
immler@69675
    59
immler@69675
    60
lemma translate_inj_on:
immler@69675
    61
  fixes A :: "'a::ab_group_add set"
immler@69675
    62
  shows "inj_on (\<lambda>x. a + x) A"
immler@69675
    63
  unfolding inj_on_def by auto
immler@69675
    64
immler@69675
    65
lemma translation_assoc:
immler@69675
    66
  fixes a b :: "'a::ab_group_add"
immler@69675
    67
  shows "(\<lambda>x. b + x) ` ((\<lambda>x. a + x) ` S) = (\<lambda>x. (a + b) + x) ` S"
immler@69675
    68
  by auto
immler@69675
    69
immler@69675
    70
lemma translation_invert:
immler@69675
    71
  fixes a :: "'a::ab_group_add"
immler@69675
    72
  assumes "(\<lambda>x. a + x) ` A = (\<lambda>x. a + x) ` B"
immler@69675
    73
  shows "A = B"
immler@69675
    74
proof -
immler@69675
    75
  have "(\<lambda>x. -a + x) ` ((\<lambda>x. a + x) ` A) = (\<lambda>x. - a + x) ` ((\<lambda>x. a + x) ` B)"
immler@69675
    76
    using assms by auto
immler@69675
    77
  then show ?thesis
immler@69675
    78
    using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto
immler@69675
    79
qed
immler@69675
    80
immler@69675
    81
lemma translation_galois:
immler@69675
    82
  fixes a :: "'a::ab_group_add"
immler@69675
    83
  shows "T = ((\<lambda>x. a + x) ` S) \<longleftrightarrow> S = ((\<lambda>x. (- a) + x) ` T)"
immler@69675
    84
  using translation_assoc[of "-a" a S]
immler@69675
    85
  apply auto
immler@69675
    86
  using translation_assoc[of a "-a" T]
immler@69675
    87
  apply auto
immler@69675
    88
  done
immler@69675
    89
immler@69675
    90
lemma translation_inverse_subset:
immler@69675
    91
  assumes "((\<lambda>x. - a + x) ` V) \<le> (S :: 'n::ab_group_add set)"
immler@69675
    92
  shows "V \<le> ((\<lambda>x. a + x) ` S)"
immler@69675
    93
proof -
immler@69675
    94
  {
immler@69675
    95
    fix x
immler@69675
    96
    assume "x \<in> V"
immler@69675
    97
    then have "x-a \<in> S" using assms by auto
immler@69675
    98
    then have "x \<in> {a + v |v. v \<in> S}"
immler@69675
    99
      apply auto
immler@69675
   100
      apply (rule exI[of _ "x-a"], simp)
immler@69675
   101
      done
immler@69675
   102
    then have "x \<in> ((\<lambda>x. a+x) ` S)" by auto
immler@69675
   103
  }
immler@69675
   104
  then show ?thesis by auto
immler@69675
   105
qed
wenzelm@53406
   106
nipkow@68901
   107
subsection%unimportant \<open>More interesting properties of the norm\<close>
hoelzl@63050
   108
immler@69674
   109
unbundle inner_syntax
hoelzl@63050
   110
wenzelm@69597
   111
text\<open>Equality of vectors in terms of \<^term>\<open>(\<bullet>)\<close> products.\<close>
hoelzl@63050
   112
hoelzl@63050
   113
lemma linear_componentwise:
hoelzl@63050
   114
  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
hoelzl@63050
   115
  assumes lf: "linear f"
hoelzl@63050
   116
  shows "(f x) \<bullet> j = (\<Sum>i\<in>Basis. (x\<bullet>i) * (f i\<bullet>j))" (is "?lhs = ?rhs")
hoelzl@63050
   117
proof -
immler@68072
   118
  interpret linear f by fact
hoelzl@63050
   119
  have "?rhs = (\<Sum>i\<in>Basis. (x\<bullet>i) *\<^sub>R (f i))\<bullet>j"
nipkow@64267
   120
    by (simp add: inner_sum_left)
hoelzl@63050
   121
  then show ?thesis
immler@68072
   122
    by (simp add: euclidean_representation sum[symmetric] scale[symmetric])
hoelzl@63050
   123
qed
hoelzl@63050
   124
hoelzl@63050
   125
lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x"
hoelzl@63050
   126
  (is "?lhs \<longleftrightarrow> ?rhs")
hoelzl@63050
   127
proof
hoelzl@63050
   128
  assume ?lhs
hoelzl@63050
   129
  then show ?rhs by simp
hoelzl@63050
   130
next
hoelzl@63050
   131
  assume ?rhs
hoelzl@63050
   132
  then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0"
hoelzl@63050
   133
    by simp
hoelzl@63050
   134
  then have "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0"
hoelzl@63050
   135
    by (simp add: inner_diff inner_commute)
hoelzl@63050
   136
  then have "(x - y) \<bullet> (x - y) = 0"
hoelzl@63050
   137
    by (simp add: field_simps inner_diff inner_commute)
hoelzl@63050
   138
  then show "x = y" by simp
hoelzl@63050
   139
qed
hoelzl@63050
   140
hoelzl@63050
   141
lemma norm_triangle_half_r:
hoelzl@63050
   142
  "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
hoelzl@63050
   143
  using dist_triangle_half_r unfolding dist_norm[symmetric] by auto
hoelzl@63050
   144
hoelzl@63050
   145
lemma norm_triangle_half_l:
hoelzl@63050
   146
  assumes "norm (x - y) < e / 2"
hoelzl@63050
   147
    and "norm (x' - y) < e / 2"
hoelzl@63050
   148
  shows "norm (x - x') < e"
hoelzl@63050
   149
  using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]]
hoelzl@63050
   150
  unfolding dist_norm[symmetric] .
hoelzl@63050
   151
lp15@66420
   152
lemma abs_triangle_half_r:
lp15@66420
   153
  fixes y :: "'a::linordered_field"
lp15@66420
   154
  shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e"
lp15@66420
   155
  by linarith
lp15@66420
   156
lp15@66420
   157
lemma abs_triangle_half_l:
lp15@66420
   158
  fixes y :: "'a::linordered_field"
lp15@66420
   159
  assumes "abs (x - y) < e / 2"
lp15@66420
   160
    and "abs (x' - y) < e / 2"
lp15@66420
   161
  shows "abs (x - x') < e"
lp15@66420
   162
  using assms by linarith
lp15@66420
   163
nipkow@64267
   164
lemma sum_clauses:
nipkow@64267
   165
  shows "sum f {} = 0"
nipkow@64267
   166
    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
   167
  by (auto simp add: insert_absorb)
hoelzl@63050
   168
hoelzl@63050
   169
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
hoelzl@63050
   170
proof
hoelzl@63050
   171
  assume "\<forall>x. x \<bullet> y = x \<bullet> z"
hoelzl@63050
   172
  then have "\<forall>x. x \<bullet> (y - z) = 0"
hoelzl@63050
   173
    by (simp add: inner_diff)
hoelzl@63050
   174
  then have "(y - z) \<bullet> (y - z) = 0" ..
hoelzl@63050
   175
  then show "y = z" by simp
hoelzl@63050
   176
qed simp
hoelzl@63050
   177
hoelzl@63050
   178
lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y"
hoelzl@63050
   179
proof
hoelzl@63050
   180
  assume "\<forall>z. x \<bullet> z = y \<bullet> z"
hoelzl@63050
   181
  then have "\<forall>z. (x - y) \<bullet> z = 0"
hoelzl@63050
   182
    by (simp add: inner_diff)
hoelzl@63050
   183
  then have "(x - y) \<bullet> (x - y) = 0" ..
hoelzl@63050
   184
  then show "x = y" by simp
hoelzl@63050
   185
qed simp
hoelzl@63050
   186
immler@69619
   187
subsection \<open>Substandard Basis\<close>
immler@69619
   188
immler@69619
   189
lemma ex_card:
immler@69619
   190
  assumes "n \<le> card A"
immler@69619
   191
  shows "\<exists>S\<subseteq>A. card S = n"
immler@69619
   192
proof (cases "finite A")
immler@69619
   193
  case True
immler@69619
   194
  from ex_bij_betw_nat_finite[OF this] obtain f where f: "bij_betw f {0..<card A} A" ..
immler@69619
   195
  moreover from f \<open>n \<le> card A\<close> have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
immler@69619
   196
    by (auto simp: bij_betw_def intro: subset_inj_on)
immler@69619
   197
  ultimately have "f ` {..< n} \<subseteq> A" "card (f ` {..< n}) = n"
immler@69619
   198
    by (auto simp: bij_betw_def card_image)
immler@69619
   199
  then show ?thesis by blast
immler@69619
   200
next
immler@69619
   201
  case False
immler@69619
   202
  with \<open>n \<le> card A\<close> show ?thesis by force
immler@69619
   203
qed
immler@69619
   204
immler@69619
   205
lemma subspace_substandard: "subspace {x::'a::euclidean_space. (\<forall>i\<in>Basis. P i \<longrightarrow> x\<bullet>i = 0)}"
immler@69619
   206
  by (auto simp: subspace_def inner_add_left)
immler@69619
   207
immler@69619
   208
lemma dim_substandard:
immler@69619
   209
  assumes d: "d \<subseteq> Basis"
immler@69619
   210
  shows "dim {x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0} = card d" (is "dim ?A = _")
immler@69619
   211
proof (rule dim_unique)
immler@69619
   212
  from d show "d \<subseteq> ?A"
immler@69619
   213
    by (auto simp: inner_Basis)
immler@69619
   214
  from d show "independent d"
immler@69619
   215
    by (rule independent_mono [OF independent_Basis])
immler@69619
   216
  have "x \<in> span d" if "\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0" for x
immler@69619
   217
  proof -
immler@69619
   218
    have "finite d"
immler@69619
   219
      by (rule finite_subset [OF d finite_Basis])
immler@69619
   220
    then have "(\<Sum>i\<in>d. (x \<bullet> i) *\<^sub>R i) \<in> span d"
immler@69619
   221
      by (simp add: span_sum span_clauses)
immler@69619
   222
    also have "(\<Sum>i\<in>d. (x \<bullet> i) *\<^sub>R i) = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i)"
immler@69619
   223
      by (rule sum.mono_neutral_cong_left [OF finite_Basis d]) (auto simp: that)
immler@69619
   224
    finally show "x \<in> span d"
immler@69619
   225
      by (simp only: euclidean_representation)
immler@69619
   226
  qed
immler@69619
   227
  then show "?A \<subseteq> span d" by auto
immler@69619
   228
qed simp
immler@69619
   229
hoelzl@63050
   230
nipkow@68901
   231
subsection \<open>Orthogonality\<close>
hoelzl@63050
   232
immler@67962
   233
definition%important (in real_inner) "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
immler@67962
   234
hoelzl@63050
   235
context real_inner
hoelzl@63050
   236
begin
hoelzl@63050
   237
lp15@63072
   238
lemma orthogonal_self: "orthogonal x x \<longleftrightarrow> x = 0"
lp15@63072
   239
  by (simp add: orthogonal_def)
lp15@63072
   240
hoelzl@63050
   241
lemma orthogonal_clauses:
hoelzl@63050
   242
  "orthogonal a 0"
hoelzl@63050
   243
  "orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)"
hoelzl@63050
   244
  "orthogonal a x \<Longrightarrow> orthogonal a (- x)"
hoelzl@63050
   245
  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x + y)"
hoelzl@63050
   246
  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x - y)"
hoelzl@63050
   247
  "orthogonal 0 a"
hoelzl@63050
   248
  "orthogonal x a \<Longrightarrow> orthogonal (c *\<^sub>R x) a"
hoelzl@63050
   249
  "orthogonal x a \<Longrightarrow> orthogonal (- x) a"
hoelzl@63050
   250
  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
hoelzl@63050
   251
  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
hoelzl@63050
   252
  unfolding orthogonal_def inner_add inner_diff by auto
hoelzl@63050
   253
hoelzl@63050
   254
end
hoelzl@63050
   255
hoelzl@63050
   256
lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
hoelzl@63050
   257
  by (simp add: orthogonal_def inner_commute)
hoelzl@63050
   258
lp15@63114
   259
lemma orthogonal_scaleR [simp]: "c \<noteq> 0 \<Longrightarrow> orthogonal (c *\<^sub>R x) = orthogonal x"
lp15@63114
   260
  by (rule ext) (simp add: orthogonal_def)
lp15@63114
   261
lp15@63114
   262
lemma pairwise_ortho_scaleR:
lp15@63114
   263
    "pairwise (\<lambda>i j. orthogonal (f i) (g j)) B
lp15@63114
   264
    \<Longrightarrow> pairwise (\<lambda>i j. orthogonal (a i *\<^sub>R f i) (a j *\<^sub>R g j)) B"
lp15@63114
   265
  by (auto simp: pairwise_def orthogonal_clauses)
lp15@63114
   266
lp15@63114
   267
lemma orthogonal_rvsum:
nipkow@64267
   268
    "\<lbrakk>finite s; \<And>y. y \<in> s \<Longrightarrow> orthogonal x (f y)\<rbrakk> \<Longrightarrow> orthogonal x (sum f s)"
lp15@63114
   269
  by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
lp15@63114
   270
lp15@63114
   271
lemma orthogonal_lvsum:
nipkow@64267
   272
    "\<lbrakk>finite s; \<And>x. x \<in> s \<Longrightarrow> orthogonal (f x) y\<rbrakk> \<Longrightarrow> orthogonal (sum f s) y"
lp15@63114
   273
  by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
lp15@63114
   274
lp15@63114
   275
lemma norm_add_Pythagorean:
lp15@63114
   276
  assumes "orthogonal a b"
lp15@63114
   277
    shows "norm(a + b) ^ 2 = norm a ^ 2 + norm b ^ 2"
lp15@63114
   278
proof -
lp15@63114
   279
  from assms have "(a - (0 - b)) \<bullet> (a - (0 - b)) = a \<bullet> a - (0 - b \<bullet> b)"
lp15@63114
   280
    by (simp add: algebra_simps orthogonal_def inner_commute)
lp15@63114
   281
  then show ?thesis
lp15@63114
   282
    by (simp add: power2_norm_eq_inner)
lp15@63114
   283
qed
lp15@63114
   284
nipkow@64267
   285
lemma norm_sum_Pythagorean:
lp15@63114
   286
  assumes "finite I" "pairwise (\<lambda>i j. orthogonal (f i) (f j)) I"
nipkow@64267
   287
    shows "(norm (sum f I))\<^sup>2 = (\<Sum>i\<in>I. (norm (f i))\<^sup>2)"
lp15@63114
   288
using assms
lp15@63114
   289
proof (induction I rule: finite_induct)
lp15@63114
   290
  case empty then show ?case by simp
lp15@63114
   291
next
lp15@63114
   292
  case (insert x I)
nipkow@64267
   293
  then have "orthogonal (f x) (sum f I)"
lp15@63114
   294
    by (metis pairwise_insert orthogonal_rvsum)
lp15@63114
   295
  with insert show ?case
lp15@63114
   296
    by (simp add: pairwise_insert norm_add_Pythagorean)
lp15@63114
   297
qed
lp15@63114
   298
hoelzl@63050
   299
immler@69683
   300
subsection  \<open>Orthogonality of a transformation\<close>
immler@69675
   301
immler@69675
   302
definition%important  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
immler@69675
   303
immler@69675
   304
lemma%unimportant  orthogonal_transformation:
immler@69675
   305
  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)"
immler@69675
   306
  unfolding orthogonal_transformation_def
immler@69675
   307
  apply auto
immler@69675
   308
  apply (erule_tac x=v in allE)+
immler@69675
   309
  apply (simp add: norm_eq_sqrt_inner)
immler@69675
   310
  apply (simp add: dot_norm linear_add[symmetric])
immler@69675
   311
  done
immler@69675
   312
immler@69675
   313
lemma%unimportant  orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
immler@69675
   314
  by (simp add: linear_iff orthogonal_transformation_def)
immler@69675
   315
immler@69675
   316
lemma%unimportant  orthogonal_orthogonal_transformation:
immler@69675
   317
    "orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y"
immler@69675
   318
  by (simp add: orthogonal_def orthogonal_transformation_def)
immler@69675
   319
immler@69675
   320
lemma%unimportant  orthogonal_transformation_compose:
immler@69675
   321
   "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
immler@69675
   322
  by (auto simp: orthogonal_transformation_def linear_compose)
immler@69675
   323
immler@69675
   324
lemma%unimportant  orthogonal_transformation_neg:
immler@69675
   325
  "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
immler@69675
   326
  by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
immler@69675
   327
immler@69675
   328
lemma%unimportant  orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v"
immler@69675
   329
  by (simp add: linear_iff orthogonal_transformation_def)
immler@69675
   330
immler@69675
   331
lemma%unimportant  orthogonal_transformation_linear:
immler@69675
   332
   "orthogonal_transformation f \<Longrightarrow> linear f"
immler@69675
   333
  by (simp add: orthogonal_transformation_def)
immler@69675
   334
immler@69675
   335
lemma%unimportant  orthogonal_transformation_inj:
immler@69675
   336
  "orthogonal_transformation f \<Longrightarrow> inj f"
immler@69675
   337
  unfolding orthogonal_transformation_def inj_on_def
immler@69675
   338
  by (metis vector_eq)
immler@69675
   339
immler@69675
   340
lemma%unimportant  orthogonal_transformation_surj:
immler@69675
   341
  "orthogonal_transformation f \<Longrightarrow> surj f"
immler@69675
   342
  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
immler@69675
   343
  by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)
immler@69675
   344
immler@69675
   345
lemma%unimportant  orthogonal_transformation_bij:
immler@69675
   346
  "orthogonal_transformation f \<Longrightarrow> bij f"
immler@69675
   347
  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
immler@69675
   348
  by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)
immler@69675
   349
immler@69675
   350
lemma%unimportant  orthogonal_transformation_inv:
immler@69675
   351
  "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
immler@69675
   352
  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
immler@69675
   353
  by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
immler@69675
   354
immler@69675
   355
lemma%unimportant  orthogonal_transformation_norm:
immler@69675
   356
  "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
immler@69675
   357
  by (metis orthogonal_transformation)
immler@69675
   358
immler@69675
   359
nipkow@68901
   360
subsection \<open>Bilinear functions\<close>
hoelzl@63050
   361
nipkow@69600
   362
definition%important
nipkow@69600
   363
bilinear :: "('a::real_vector \<Rightarrow> 'b::real_vector \<Rightarrow> 'c::real_vector) \<Rightarrow> bool" where
nipkow@69600
   364
"bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
hoelzl@63050
   365
hoelzl@63050
   366
lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
hoelzl@63050
   367
  by (simp add: bilinear_def linear_iff)
hoelzl@63050
   368
hoelzl@63050
   369
lemma bilinear_radd: "bilinear h \<Longrightarrow> h x (y + z) = h x y + h x z"
hoelzl@63050
   370
  by (simp add: bilinear_def linear_iff)
hoelzl@63050
   371
hoelzl@63050
   372
lemma bilinear_lmul: "bilinear h \<Longrightarrow> h (c *\<^sub>R x) y = c *\<^sub>R h x y"
hoelzl@63050
   373
  by (simp add: bilinear_def linear_iff)
hoelzl@63050
   374
hoelzl@63050
   375
lemma bilinear_rmul: "bilinear h \<Longrightarrow> h x (c *\<^sub>R y) = c *\<^sub>R h x y"
hoelzl@63050
   376
  by (simp add: bilinear_def linear_iff)
hoelzl@63050
   377
hoelzl@63050
   378
lemma bilinear_lneg: "bilinear h \<Longrightarrow> h (- x) y = - h x y"
hoelzl@63050
   379
  by (drule bilinear_lmul [of _ "- 1"]) simp
hoelzl@63050
   380
hoelzl@63050
   381
lemma bilinear_rneg: "bilinear h \<Longrightarrow> h x (- y) = - h x y"
hoelzl@63050
   382
  by (drule bilinear_rmul [of _ _ "- 1"]) simp
hoelzl@63050
   383
hoelzl@63050
   384
lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
hoelzl@63050
   385
  using add_left_imp_eq[of x y 0] by auto
hoelzl@63050
   386
hoelzl@63050
   387
lemma bilinear_lzero:
hoelzl@63050
   388
  assumes "bilinear h"
hoelzl@63050
   389
  shows "h 0 x = 0"
hoelzl@63050
   390
  using bilinear_ladd [OF assms, of 0 0 x] by (simp add: eq_add_iff field_simps)
hoelzl@63050
   391
hoelzl@63050
   392
lemma bilinear_rzero:
hoelzl@63050
   393
  assumes "bilinear h"
hoelzl@63050
   394
  shows "h x 0 = 0"
hoelzl@63050
   395
  using bilinear_radd [OF assms, of x 0 0 ] by (simp add: eq_add_iff field_simps)
hoelzl@63050
   396
hoelzl@63050
   397
lemma bilinear_lsub: "bilinear h \<Longrightarrow> h (x - y) z = h x z - h y z"
hoelzl@63050
   398
  using bilinear_ladd [of h x "- y"] by (simp add: bilinear_lneg)
hoelzl@63050
   399
hoelzl@63050
   400
lemma bilinear_rsub: "bilinear h \<Longrightarrow> h z (x - y) = h z x - h z y"
hoelzl@63050
   401
  using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg)
hoelzl@63050
   402
nipkow@64267
   403
lemma bilinear_sum:
immler@68072
   404
  assumes "bilinear h"
nipkow@64267
   405
  shows "h (sum f S) (sum g T) = sum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
hoelzl@63050
   406
proof -
immler@68072
   407
  interpret l: linear "\<lambda>x. h x y" for y using assms by (simp add: bilinear_def)
immler@68072
   408
  interpret r: linear "\<lambda>y. h x y" for x using assms by (simp add: bilinear_def)
nipkow@64267
   409
  have "h (sum f S) (sum g T) = sum (\<lambda>x. h (f x) (sum g T)) S"
immler@68072
   410
    by (simp add: l.sum)
nipkow@64267
   411
  also have "\<dots> = sum (\<lambda>x. sum (\<lambda>y. h (f x) (g y)) T) S"
immler@68072
   412
    by (rule sum.cong) (simp_all add: r.sum)
hoelzl@63050
   413
  finally show ?thesis
nipkow@64267
   414
    unfolding sum.cartesian_product .
hoelzl@63050
   415
qed
hoelzl@63050
   416
hoelzl@63050
   417
nipkow@68901
   418
subsection \<open>Adjoints\<close>
hoelzl@63050
   419
nipkow@69600
   420
definition%important adjoint :: "(('a::real_inner) \<Rightarrow> ('b::real_inner)) \<Rightarrow> 'b \<Rightarrow> 'a" where
nipkow@69600
   421
"adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
hoelzl@63050
   422
hoelzl@63050
   423
lemma adjoint_unique:
hoelzl@63050
   424
  assumes "\<forall>x y. inner (f x) y = inner x (g y)"
hoelzl@63050
   425
  shows "adjoint f = g"
hoelzl@63050
   426
  unfolding adjoint_def
hoelzl@63050
   427
proof (rule some_equality)
hoelzl@63050
   428
  show "\<forall>x y. inner (f x) y = inner x (g y)"
hoelzl@63050
   429
    by (rule assms)
hoelzl@63050
   430
next
hoelzl@63050
   431
  fix h
hoelzl@63050
   432
  assume "\<forall>x y. inner (f x) y = inner x (h y)"
hoelzl@63050
   433
  then have "\<forall>x y. inner x (g y) = inner x (h y)"
hoelzl@63050
   434
    using assms by simp
hoelzl@63050
   435
  then have "\<forall>x y. inner x (g y - h y) = 0"
hoelzl@63050
   436
    by (simp add: inner_diff_right)
hoelzl@63050
   437
  then have "\<forall>y. inner (g y - h y) (g y - h y) = 0"
hoelzl@63050
   438
    by simp
hoelzl@63050
   439
  then have "\<forall>y. h y = g y"
hoelzl@63050
   440
    by simp
hoelzl@63050
   441
  then show "h = g" by (simp add: ext)
hoelzl@63050
   442
qed
hoelzl@63050
   443
hoelzl@63050
   444
text \<open>TODO: The following lemmas about adjoints should hold for any
wenzelm@63680
   445
  Hilbert space (i.e. complete inner product space).
wenzelm@68224
   446
  (see \<^url>\<open>https://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
hoelzl@63050
   447
\<close>
hoelzl@63050
   448
hoelzl@63050
   449
lemma adjoint_works:
hoelzl@63050
   450
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
hoelzl@63050
   451
  assumes lf: "linear f"
hoelzl@63050
   452
  shows "x \<bullet> adjoint f y = f x \<bullet> y"
hoelzl@63050
   453
proof -
immler@68072
   454
  interpret linear f by fact
hoelzl@63050
   455
  have "\<forall>y. \<exists>w. \<forall>x. f x \<bullet> y = x \<bullet> w"
hoelzl@63050
   456
  proof (intro allI exI)
hoelzl@63050
   457
    fix y :: "'m" and x
hoelzl@63050
   458
    let ?w = "(\<Sum>i\<in>Basis. (f i \<bullet> y) *\<^sub>R i) :: 'n"
hoelzl@63050
   459
    have "f x \<bullet> y = f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i) \<bullet> y"
hoelzl@63050
   460
      by (simp add: euclidean_representation)
hoelzl@63050
   461
    also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<bullet> y"
immler@68072
   462
      by (simp add: sum scale)
hoelzl@63050
   463
    finally show "f x \<bullet> y = x \<bullet> ?w"
nipkow@64267
   464
      by (simp add: inner_sum_left inner_sum_right mult.commute)
hoelzl@63050
   465
  qed
hoelzl@63050
   466
  then show ?thesis
hoelzl@63050
   467
    unfolding adjoint_def choice_iff
hoelzl@63050
   468
    by (intro someI2_ex[where Q="\<lambda>f'. x \<bullet> f' y = f x \<bullet> y"]) auto
hoelzl@63050
   469
qed
hoelzl@63050
   470
hoelzl@63050
   471
lemma adjoint_clauses:
hoelzl@63050
   472
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
hoelzl@63050
   473
  assumes lf: "linear f"
hoelzl@63050
   474
  shows "x \<bullet> adjoint f y = f x \<bullet> y"
hoelzl@63050
   475
    and "adjoint f y \<bullet> x = y \<bullet> f x"
hoelzl@63050
   476
  by (simp_all add: adjoint_works[OF lf] inner_commute)
hoelzl@63050
   477
hoelzl@63050
   478
lemma adjoint_linear:
hoelzl@63050
   479
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
hoelzl@63050
   480
  assumes lf: "linear f"
hoelzl@63050
   481
  shows "linear (adjoint f)"
hoelzl@63050
   482
  by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]
hoelzl@63050
   483
    adjoint_clauses[OF lf] inner_distrib)
hoelzl@63050
   484
hoelzl@63050
   485
lemma adjoint_adjoint:
hoelzl@63050
   486
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
hoelzl@63050
   487
  assumes lf: "linear f"
hoelzl@63050
   488
  shows "adjoint (adjoint f) = f"
hoelzl@63050
   489
  by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
hoelzl@63050
   490
hoelzl@63050
   491
hoelzl@63050
   492
subsection \<open>Archimedean properties and useful consequences\<close>
hoelzl@63050
   493
hoelzl@63050
   494
text\<open>Bernoulli's inequality\<close>
immler@68607
   495
proposition Bernoulli_inequality:
hoelzl@63050
   496
  fixes x :: real
hoelzl@63050
   497
  assumes "-1 \<le> x"
hoelzl@63050
   498
    shows "1 + n * x \<le> (1 + x) ^ n"
immler@68607
   499
proof (induct n)
hoelzl@63050
   500
  case 0
hoelzl@63050
   501
  then show ?case by simp
hoelzl@63050
   502
next
hoelzl@63050
   503
  case (Suc n)
hoelzl@63050
   504
  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
hoelzl@63050
   505
    by (simp add: algebra_simps)
hoelzl@63050
   506
  also have "... = (1 + x) * (1 + n*x)"
hoelzl@63050
   507
    by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
hoelzl@63050
   508
  also have "... \<le> (1 + x) ^ Suc n"
hoelzl@63050
   509
    using Suc.hyps assms mult_left_mono by fastforce
hoelzl@63050
   510
  finally show ?case .
hoelzl@63050
   511
qed
hoelzl@63050
   512
hoelzl@63050
   513
corollary Bernoulli_inequality_even:
hoelzl@63050
   514
  fixes x :: real
hoelzl@63050
   515
  assumes "even n"
hoelzl@63050
   516
    shows "1 + n * x \<le> (1 + x) ^ n"
hoelzl@63050
   517
proof (cases "-1 \<le> x \<or> n=0")
hoelzl@63050
   518
  case True
hoelzl@63050
   519
  then show ?thesis
hoelzl@63050
   520
    by (auto simp: Bernoulli_inequality)
hoelzl@63050
   521
next
hoelzl@63050
   522
  case False
hoelzl@63050
   523
  then have "real n \<ge> 1"
hoelzl@63050
   524
    by simp
hoelzl@63050
   525
  with False have "n * x \<le> -1"
hoelzl@63050
   526
    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
   527
  then have "1 + n * x \<le> 0"
hoelzl@63050
   528
    by auto
hoelzl@63050
   529
  also have "... \<le> (1 + x) ^ n"
hoelzl@63050
   530
    using assms
hoelzl@63050
   531
    using zero_le_even_power by blast
hoelzl@63050
   532
  finally show ?thesis .
hoelzl@63050
   533
qed
hoelzl@63050
   534
hoelzl@63050
   535
corollary real_arch_pow:
hoelzl@63050
   536
  fixes x :: real
hoelzl@63050
   537
  assumes x: "1 < x"
hoelzl@63050
   538
  shows "\<exists>n. y < x^n"
hoelzl@63050
   539
proof -
hoelzl@63050
   540
  from x have x0: "x - 1 > 0"
hoelzl@63050
   541
    by arith
hoelzl@63050
   542
  from reals_Archimedean3[OF x0, rule_format, of y]
hoelzl@63050
   543
  obtain n :: nat where n: "y < real n * (x - 1)" by metis
hoelzl@63050
   544
  from x0 have x00: "x- 1 \<ge> -1" by arith
hoelzl@63050
   545
  from Bernoulli_inequality[OF x00, of n] n
hoelzl@63050
   546
  have "y < x^n" by auto
hoelzl@63050
   547
  then show ?thesis by metis
hoelzl@63050
   548
qed
hoelzl@63050
   549
hoelzl@63050
   550
corollary real_arch_pow_inv:
hoelzl@63050
   551
  fixes x y :: real
hoelzl@63050
   552
  assumes y: "y > 0"
hoelzl@63050
   553
    and x1: "x < 1"
hoelzl@63050
   554
  shows "\<exists>n. x^n < y"
hoelzl@63050
   555
proof (cases "x > 0")
hoelzl@63050
   556
  case True
hoelzl@63050
   557
  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
hoelzl@63050
   558
  from real_arch_pow[OF ix, of "1/y"]
hoelzl@63050
   559
  obtain n where n: "1/y < (1/x)^n" by blast
hoelzl@63050
   560
  then show ?thesis using y \<open>x > 0\<close>
hoelzl@63050
   561
    by (auto simp add: field_simps)
hoelzl@63050
   562
next
hoelzl@63050
   563
  case False
hoelzl@63050
   564
  with y x1 show ?thesis
lp15@68069
   565
    by (metis less_le_trans not_less power_one_right)
hoelzl@63050
   566
qed
hoelzl@63050
   567
hoelzl@63050
   568
lemma forall_pos_mono:
hoelzl@63050
   569
  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
hoelzl@63050
   570
    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
hoelzl@63050
   571
  by (metis real_arch_inverse)
hoelzl@63050
   572
hoelzl@63050
   573
lemma forall_pos_mono_1:
hoelzl@63050
   574
  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
hoelzl@63050
   575
    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
hoelzl@63050
   576
  apply (rule forall_pos_mono)
hoelzl@63050
   577
  apply auto
hoelzl@63050
   578
  apply (metis Suc_pred of_nat_Suc)
hoelzl@63050
   579
  done
hoelzl@63050
   580
hoelzl@63050
   581
immler@67962
   582
subsection%unimportant \<open>Euclidean Spaces as Typeclass\<close>
huffman@44133
   583
hoelzl@50526
   584
lemma independent_Basis: "independent Basis"
immler@68072
   585
  by (rule independent_Basis)
hoelzl@50526
   586
huffman@53939
   587
lemma span_Basis [simp]: "span Basis = UNIV"
immler@68072
   588
  by (rule span_Basis)
huffman@44133
   589
hoelzl@50526
   590
lemma in_span_Basis: "x \<in> span Basis"
hoelzl@50526
   591
  unfolding span_Basis ..
hoelzl@50526
   592
wenzelm@53406
   593
immler@67962
   594
subsection%unimportant \<open>Linearity and Bilinearity continued\<close>
huffman@44133
   595
huffman@44133
   596
lemma linear_bounded:
wenzelm@56444
   597
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
huffman@44133
   598
  assumes lf: "linear f"
huffman@44133
   599
  shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
huffman@53939
   600
proof
immler@68072
   601
  interpret linear f by fact
hoelzl@50526
   602
  let ?B = "\<Sum>b\<in>Basis. norm (f b)"
huffman@53939
   603
  show "\<forall>x. norm (f x) \<le> ?B * norm x"
huffman@53939
   604
  proof
wenzelm@53406
   605
    fix x :: 'a
hoelzl@50526
   606
    let ?g = "\<lambda>b. (x \<bullet> b) *\<^sub>R f b"
hoelzl@50526
   607
    have "norm (f x) = norm (f (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b))"
hoelzl@50526
   608
      unfolding euclidean_representation ..
nipkow@64267
   609
    also have "\<dots> = norm (sum ?g Basis)"
immler@68072
   610
      by (simp add: sum scale)
nipkow@64267
   611
    finally have th0: "norm (f x) = norm (sum ?g Basis)" .
lp15@64773
   612
    have th: "norm (?g i) \<le> norm (f i) * norm x" if "i \<in> Basis" for i
lp15@64773
   613
    proof -
lp15@64773
   614
      from Basis_le_norm[OF that, of x]
huffman@53939
   615
      show "norm (?g i) \<le> norm (f i) * norm x"
lp15@68069
   616
        unfolding norm_scaleR  by (metis mult.commute mult_left_mono norm_ge_zero)
huffman@53939
   617
    qed
nipkow@64267
   618
    from sum_norm_le[of _ ?g, OF th]
huffman@53939
   619
    show "norm (f x) \<le> ?B * norm x"
nipkow@64267
   620
      unfolding th0 sum_distrib_right by metis
huffman@53939
   621
  qed
huffman@44133
   622
qed
huffman@44133
   623
huffman@44133
   624
lemma linear_conv_bounded_linear:
huffman@44133
   625
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
huffman@44133
   626
  shows "linear f \<longleftrightarrow> bounded_linear f"
huffman@44133
   627
proof
huffman@44133
   628
  assume "linear f"
huffman@53939
   629
  then interpret f: linear f .
huffman@44133
   630
  show "bounded_linear f"
huffman@44133
   631
  proof
huffman@44133
   632
    have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
wenzelm@60420
   633
      using \<open>linear f\<close> by (rule linear_bounded)
wenzelm@49522
   634
    then show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
haftmann@57512
   635
      by (simp add: mult.commute)
huffman@44133
   636
  qed
huffman@44133
   637
next
huffman@44133
   638
  assume "bounded_linear f"
huffman@44133
   639
  then interpret f: bounded_linear f .
huffman@53939
   640
  show "linear f" ..
huffman@53939
   641
qed
huffman@53939
   642
paulson@61518
   643
lemmas linear_linear = linear_conv_bounded_linear[symmetric]
paulson@61518
   644
huffman@53939
   645
lemma linear_bounded_pos:
wenzelm@56444
   646
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
huffman@53939
   647
  assumes lf: "linear f"
lp15@67982
   648
 obtains B where "B > 0" "\<And>x. norm (f x) \<le> B * norm x"
huffman@53939
   649
proof -
huffman@53939
   650
  have "\<exists>B > 0. \<forall>x. norm (f x) \<le> norm x * B"
huffman@53939
   651
    using lf unfolding linear_conv_bounded_linear
huffman@53939
   652
    by (rule bounded_linear.pos_bounded)
lp15@67982
   653
  with that show ?thesis
lp15@67982
   654
    by (auto simp: mult.commute)
huffman@44133
   655
qed
huffman@44133
   656
lp15@67982
   657
lemma linear_invertible_bounded_below_pos:
lp15@67982
   658
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
lp15@67982
   659
  assumes "linear f" "linear g" "g \<circ> f = id"
lp15@67982
   660
  obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
lp15@67982
   661
proof -
lp15@67982
   662
  obtain B where "B > 0" and B: "\<And>x. norm (g x) \<le> B * norm x"
lp15@67982
   663
    using linear_bounded_pos [OF \<open>linear g\<close>] by blast
lp15@67982
   664
  show thesis
lp15@67982
   665
  proof
lp15@67982
   666
    show "0 < 1/B"
lp15@67982
   667
      by (simp add: \<open>B > 0\<close>)
lp15@67982
   668
    show "1/B * norm x \<le> norm (f x)" for x
lp15@67982
   669
    proof -
lp15@67982
   670
      have "1/B * norm x = 1/B * norm (g (f x))"
lp15@67982
   671
        using assms by (simp add: pointfree_idE)
lp15@67982
   672
      also have "\<dots> \<le> norm (f x)"
lp15@67982
   673
        using B [of "f x"] by (simp add: \<open>B > 0\<close> mult.commute pos_divide_le_eq)
lp15@67982
   674
      finally show ?thesis .
lp15@67982
   675
    qed
lp15@67982
   676
  qed
lp15@67982
   677
qed
lp15@67982
   678
lp15@67982
   679
lemma linear_inj_bounded_below_pos:
lp15@67982
   680
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
lp15@67982
   681
  assumes "linear f" "inj f"
lp15@67982
   682
  obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
immler@68072
   683
  using linear_injective_left_inverse [OF assms]
immler@68072
   684
    linear_invertible_bounded_below_pos assms by blast
lp15@67982
   685
wenzelm@49522
   686
lemma bounded_linearI':
wenzelm@56444
   687
  fixes f ::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
wenzelm@53406
   688
  assumes "\<And>x y. f (x + y) = f x + f y"
wenzelm@53406
   689
    and "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
wenzelm@49522
   690
  shows "bounded_linear f"
immler@68072
   691
  using assms linearI linear_conv_bounded_linear by blast
huffman@44133
   692
huffman@44133
   693
lemma bilinear_bounded:
wenzelm@56444
   694
  fixes h :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::real_normed_vector"
huffman@44133
   695
  assumes bh: "bilinear h"
huffman@44133
   696
  shows "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
hoelzl@50526
   697
proof (clarify intro!: exI[of _ "\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)"])
wenzelm@53406
   698
  fix x :: 'm
wenzelm@53406
   699
  fix y :: 'n
nipkow@64267
   700
  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))"
lp15@68069
   701
    by (simp add: euclidean_representation)
nipkow@64267
   702
  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
   703
    unfolding bilinear_sum[OF bh] ..
hoelzl@50526
   704
  finally have th: "norm (h x y) = \<dots>" .
lp15@68069
   705
  have "\<And>i j. \<lbrakk>i \<in> Basis; j \<in> Basis\<rbrakk>
lp15@68069
   706
           \<Longrightarrow> \<bar>x \<bullet> i\<bar> * (\<bar>y \<bullet> j\<bar> * norm (h i j)) \<le> norm x * (norm y * norm (h i j))"
lp15@68069
   707
    by (auto simp add: zero_le_mult_iff Basis_le_norm mult_mono)
lp15@68069
   708
  then show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
lp15@68069
   709
    unfolding sum_distrib_right th sum.cartesian_product
lp15@68069
   710
    by (clarsimp simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
lp15@68069
   711
      field_simps simp del: scaleR_scaleR intro!: sum_norm_le)
huffman@44133
   712
qed
huffman@44133
   713
huffman@44133
   714
lemma bilinear_conv_bounded_bilinear:
huffman@44133
   715
  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
huffman@44133
   716
  shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
huffman@44133
   717
proof
huffman@44133
   718
  assume "bilinear h"
huffman@44133
   719
  show "bounded_bilinear h"
huffman@44133
   720
  proof
wenzelm@53406
   721
    fix x y z
wenzelm@53406
   722
    show "h (x + y) z = h x z + h y z"
wenzelm@60420
   723
      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff by simp
huffman@44133
   724
  next
wenzelm@53406
   725
    fix x y z
wenzelm@53406
   726
    show "h x (y + z) = h x y + h x z"
wenzelm@60420
   727
      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff by simp
huffman@44133
   728
  next
lp15@68069
   729
    show "h (scaleR r x) y = scaleR r (h x y)" "h x (scaleR r y) = scaleR r (h x y)" for r x y
wenzelm@60420
   730
      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
lp15@68069
   731
      by simp_all
huffman@44133
   732
  next
huffman@44133
   733
    have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
wenzelm@60420
   734
      using \<open>bilinear h\<close> by (rule bilinear_bounded)
wenzelm@49522
   735
    then show "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
haftmann@57514
   736
      by (simp add: ac_simps)
huffman@44133
   737
  qed
huffman@44133
   738
next
huffman@44133
   739
  assume "bounded_bilinear h"
huffman@44133
   740
  then interpret h: bounded_bilinear h .
huffman@44133
   741
  show "bilinear h"
huffman@44133
   742
    unfolding bilinear_def linear_conv_bounded_linear
wenzelm@49522
   743
    using h.bounded_linear_left h.bounded_linear_right by simp
huffman@44133
   744
qed
huffman@44133
   745
huffman@53939
   746
lemma bilinear_bounded_pos:
wenzelm@56444
   747
  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
huffman@53939
   748
  assumes bh: "bilinear h"
huffman@53939
   749
  shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
huffman@53939
   750
proof -
huffman@53939
   751
  have "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> norm x * norm y * B"
huffman@53939
   752
    using bh [unfolded bilinear_conv_bounded_bilinear]
huffman@53939
   753
    by (rule bounded_bilinear.pos_bounded)
huffman@53939
   754
  then show ?thesis
haftmann@57514
   755
    by (simp only: ac_simps)
huffman@53939
   756
qed
huffman@53939
   757
immler@68072
   758
lemma bounded_linear_imp_has_derivative: "bounded_linear f \<Longrightarrow> (f has_derivative f) net"
immler@68072
   759
  by (auto simp add: has_derivative_def linear_diff linear_linear linear_def
immler@68072
   760
      dest: bounded_linear.linear)
lp15@63469
   761
lp15@63469
   762
lemma linear_imp_has_derivative:
lp15@63469
   763
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
lp15@63469
   764
  shows "linear f \<Longrightarrow> (f has_derivative f) net"
immler@68072
   765
  by (simp add: bounded_linear_imp_has_derivative linear_conv_bounded_linear)
lp15@63469
   766
lp15@63469
   767
lemma bounded_linear_imp_differentiable: "bounded_linear f \<Longrightarrow> f differentiable net"
lp15@63469
   768
  using bounded_linear_imp_has_derivative differentiable_def by blast
lp15@63469
   769
lp15@63469
   770
lemma linear_imp_differentiable:
lp15@63469
   771
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
lp15@63469
   772
  shows "linear f \<Longrightarrow> f differentiable net"
immler@68072
   773
  by (metis linear_imp_has_derivative differentiable_def)
lp15@63469
   774
wenzelm@49522
   775
nipkow@68901
   776
subsection%unimportant \<open>We continue\<close>
huffman@44133
   777
huffman@44133
   778
lemma independent_bound:
wenzelm@53716
   779
  fixes S :: "'a::euclidean_space set"
wenzelm@53716
   780
  shows "independent S \<Longrightarrow> finite S \<and> card S \<le> DIM('a)"
immler@68072
   781
  by (metis dim_subset_UNIV finiteI_independent dim_span_eq_card_independent)
immler@68072
   782
immler@68072
   783
lemmas independent_imp_finite = finiteI_independent
huffman@44133
   784
lp15@61609
   785
corollary
paulson@60303
   786
  fixes S :: "'a::euclidean_space set"
paulson@60303
   787
  assumes "independent S"
immler@68072
   788
  shows independent_card_le:"card S \<le> DIM('a)"
immler@68072
   789
  using assms independent_bound by auto
lp15@63075
   790
wenzelm@49663
   791
lemma dependent_biggerset:
wenzelm@56444
   792
  fixes S :: "'a::euclidean_space set"
wenzelm@56444
   793
  shows "(finite S \<Longrightarrow> card S > DIM('a)) \<Longrightarrow> dependent S"
huffman@44133
   794
  by (metis independent_bound not_less)
huffman@44133
   795
wenzelm@60420
   796
text \<open>Picking an orthogonal replacement for a spanning set.\<close>
huffman@44133
   797
wenzelm@53406
   798
lemma vector_sub_project_orthogonal:
wenzelm@53406
   799
  fixes b x :: "'a::euclidean_space"
wenzelm@53406
   800
  shows "b \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *\<^sub>R b) = 0"
huffman@44133
   801
  unfolding inner_simps by auto
huffman@44133
   802
huffman@44528
   803
lemma pairwise_orthogonal_insert:
huffman@44528
   804
  assumes "pairwise orthogonal S"
wenzelm@49522
   805
    and "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
huffman@44528
   806
  shows "pairwise orthogonal (insert x S)"
huffman@44528
   807
  using assms unfolding pairwise_def
huffman@44528
   808
  by (auto simp add: orthogonal_commute)
huffman@44528
   809
huffman@44133
   810
lemma basis_orthogonal:
wenzelm@53406
   811
  fixes B :: "'a::real_inner set"
huffman@44133
   812
  assumes fB: "finite B"
huffman@44133
   813
  shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C"
huffman@44133
   814
  (is " \<exists>C. ?P B C")
wenzelm@49522
   815
  using fB
wenzelm@49522
   816
proof (induct rule: finite_induct)
wenzelm@49522
   817
  case empty
wenzelm@53406
   818
  then show ?case
wenzelm@53406
   819
    apply (rule exI[where x="{}"])
wenzelm@53406
   820
    apply (auto simp add: pairwise_def)
wenzelm@53406
   821
    done
huffman@44133
   822
next
wenzelm@49522
   823
  case (insert a B)
wenzelm@60420
   824
  note fB = \<open>finite B\<close> and aB = \<open>a \<notin> B\<close>
wenzelm@60420
   825
  from \<open>\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C\<close>
huffman@44133
   826
  obtain C where C: "finite C" "card C \<le> card B"
huffman@44133
   827
    "span C = span B" "pairwise orthogonal C" by blast
nipkow@64267
   828
  let ?a = "a - sum (\<lambda>x. (x \<bullet> a / (x \<bullet> x)) *\<^sub>R x) C"
huffman@44133
   829
  let ?C = "insert ?a C"
wenzelm@53406
   830
  from C(1) have fC: "finite ?C"
wenzelm@53406
   831
    by simp
wenzelm@49522
   832
  from fB aB C(1,2) have cC: "card ?C \<le> card (insert a B)"
wenzelm@49522
   833
    by (simp add: card_insert_if)
wenzelm@53406
   834
  {
wenzelm@53406
   835
    fix x k
wenzelm@49522
   836
    have th0: "\<And>(a::'a) b c. a - (b - c) = c + (a - b)"
wenzelm@49522
   837
      by (simp add: field_simps)
huffman@44133
   838
    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
   839
      apply (simp only: scaleR_right_diff_distrib th0)
huffman@44133
   840
      apply (rule span_add_eq)
immler@68072
   841
      apply (rule span_scale)
nipkow@64267
   842
      apply (rule span_sum)
immler@68072
   843
      apply (rule span_scale)
immler@68072
   844
      apply (rule span_base)
wenzelm@49522
   845
      apply assumption
wenzelm@53406
   846
      done
wenzelm@53406
   847
  }
huffman@44133
   848
  then have SC: "span ?C = span (insert a B)"
huffman@44133
   849
    unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto
wenzelm@53406
   850
  {
wenzelm@53406
   851
    fix y
wenzelm@53406
   852
    assume yC: "y \<in> C"
wenzelm@53406
   853
    then have Cy: "C = insert y (C - {y})"
wenzelm@53406
   854
      by blast
wenzelm@53406
   855
    have fth: "finite (C - {y})"
wenzelm@53406
   856
      using C by simp
huffman@44528
   857
    have "orthogonal ?a y"
huffman@44528
   858
      unfolding orthogonal_def
nipkow@64267
   859
      unfolding inner_diff inner_sum_left right_minus_eq
nipkow@64267
   860
      unfolding sum.remove [OF \<open>finite C\<close> \<open>y \<in> C\<close>]
huffman@44528
   861
      apply (clarsimp simp add: inner_commute[of y a])
nipkow@64267
   862
      apply (rule sum.neutral)
huffman@44528
   863
      apply clarsimp
huffman@44528
   864
      apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
wenzelm@60420
   865
      using \<open>y \<in> C\<close> by auto
wenzelm@53406
   866
  }
wenzelm@60420
   867
  with \<open>pairwise orthogonal C\<close> have CPO: "pairwise orthogonal ?C"
huffman@44528
   868
    by (rule pairwise_orthogonal_insert)
wenzelm@53406
   869
  from fC cC SC CPO have "?P (insert a B) ?C"
wenzelm@53406
   870
    by blast
huffman@44133
   871
  then show ?case by blast
huffman@44133
   872
qed
huffman@44133
   873
huffman@44133
   874
lemma orthogonal_basis_exists:
huffman@44133
   875
  fixes V :: "('a::euclidean_space) set"
immler@68072
   876
  shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and>
immler@68072
   877
  (card B = dim V) \<and> pairwise orthogonal B"
wenzelm@49663
   878
proof -
wenzelm@49522
   879
  from basis_exists[of V] obtain B where
wenzelm@53406
   880
    B: "B \<subseteq> V" "independent B" "V \<subseteq> span B" "card B = dim V"
immler@68073
   881
    by force
wenzelm@53406
   882
  from B have fB: "finite B" "card B = dim V"
wenzelm@53406
   883
    using independent_bound by auto
huffman@44133
   884
  from basis_orthogonal[OF fB(1)] obtain C where
wenzelm@53406
   885
    C: "finite C" "card C \<le> card B" "span C = span B" "pairwise orthogonal C"
wenzelm@53406
   886
    by blast
wenzelm@53406
   887
  from C B have CSV: "C \<subseteq> span V"
immler@68072
   888
    by (metis span_superset span_mono subset_trans)
wenzelm@53406
   889
  from span_mono[OF B(3)] C have SVC: "span V \<subseteq> span C"
wenzelm@53406
   890
    by (simp add: span_span)
huffman@44133
   891
  from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB
wenzelm@53406
   892
  have iC: "independent C"
huffman@44133
   893
    by (simp add: dim_span)
wenzelm@53406
   894
  from C fB have "card C \<le> dim V"
wenzelm@53406
   895
    by simp
wenzelm@53406
   896
  moreover have "dim V \<le> card C"
wenzelm@53406
   897
    using span_card_ge_dim[OF CSV SVC C(1)]
immler@68072
   898
    by simp
wenzelm@53406
   899
  ultimately have CdV: "card C = dim V"
wenzelm@53406
   900
    using C(1) by simp
wenzelm@53406
   901
  from C B CSV CdV iC show ?thesis
wenzelm@53406
   902
    by auto
huffman@44133
   903
qed
huffman@44133
   904
wenzelm@60420
   905
text \<open>Low-dimensional subset is in a hyperplane (weak orthogonal complement).\<close>
huffman@44133
   906
wenzelm@49522
   907
lemma span_not_univ_orthogonal:
wenzelm@53406
   908
  fixes S :: "'a::euclidean_space set"
huffman@44133
   909
  assumes sU: "span S \<noteq> UNIV"
wenzelm@56444
   910
  shows "\<exists>a::'a. a \<noteq> 0 \<and> (\<forall>x \<in> span S. a \<bullet> x = 0)"
wenzelm@49522
   911
proof -
wenzelm@53406
   912
  from sU obtain a where a: "a \<notin> span S"
wenzelm@53406
   913
    by blast
huffman@44133
   914
  from orthogonal_basis_exists obtain B where
immler@68072
   915
    B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B"
immler@68072
   916
    "card B = dim S" "pairwise orthogonal B"
huffman@44133
   917
    by blast
wenzelm@53406
   918
  from B have fB: "finite B" "card B = dim S"
wenzelm@53406
   919
    using independent_bound by auto
huffman@44133
   920
  from span_mono[OF B(2)] span_mono[OF B(3)]
wenzelm@53406
   921
  have sSB: "span S = span B"
wenzelm@53406
   922
    by (simp add: span_span)
nipkow@64267
   923
  let ?a = "a - sum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B"
nipkow@64267
   924
  have "sum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *\<^sub>R b) B \<in> span S"
huffman@44133
   925
    unfolding sSB
nipkow@64267
   926
    apply (rule span_sum)
immler@68072
   927
    apply (rule span_scale)
immler@68072
   928
    apply (rule span_base)
wenzelm@49522
   929
    apply assumption
wenzelm@49522
   930
    done
wenzelm@53406
   931
  with a have a0:"?a  \<noteq> 0"
wenzelm@53406
   932
    by auto
lp15@68058
   933
  have "?a \<bullet> x = 0" if "x\<in>span B" for x
lp15@68058
   934
  proof (rule span_induct [OF that])
wenzelm@49522
   935
    show "subspace {x. ?a \<bullet> x = 0}"
wenzelm@49522
   936
      by (auto simp add: subspace_def inner_add)
wenzelm@49522
   937
  next
wenzelm@53406
   938
    {
wenzelm@53406
   939
      fix x
wenzelm@53406
   940
      assume x: "x \<in> B"
wenzelm@53406
   941
      from x have B': "B = insert x (B - {x})"
wenzelm@53406
   942
        by blast
wenzelm@53406
   943
      have fth: "finite (B - {x})"
wenzelm@53406
   944
        using fB by simp
huffman@44133
   945
      have "?a \<bullet> x = 0"
wenzelm@53406
   946
        apply (subst B')
wenzelm@53406
   947
        using fB fth
nipkow@64267
   948
        unfolding sum_clauses(2)[OF fth]
huffman@44133
   949
        apply simp unfolding inner_simps
nipkow@64267
   950
        apply (clarsimp simp add: inner_add inner_sum_left)
nipkow@64267
   951
        apply (rule sum.neutral, rule ballI)
wenzelm@63170
   952
        apply (simp only: inner_commute)
wenzelm@49711
   953
        apply (auto simp add: x field_simps
wenzelm@49711
   954
          intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
wenzelm@53406
   955
        done
wenzelm@53406
   956
    }
lp15@68058
   957
    then show "?a \<bullet> x = 0" if "x \<in> B" for x
lp15@68058
   958
      using that by blast
lp15@68058
   959
    qed
wenzelm@53406
   960
  with a0 show ?thesis
wenzelm@53406
   961
    unfolding sSB by (auto intro: exI[where x="?a"])
huffman@44133
   962
qed
huffman@44133
   963
huffman@44133
   964
lemma span_not_univ_subset_hyperplane:
wenzelm@53406
   965
  fixes S :: "'a::euclidean_space set"
wenzelm@53406
   966
  assumes SU: "span S \<noteq> UNIV"
huffman@44133
   967
  shows "\<exists> a. a \<noteq>0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
huffman@44133
   968
  using span_not_univ_orthogonal[OF SU] by auto
huffman@44133
   969
wenzelm@49663
   970
lemma lowdim_subset_hyperplane:
wenzelm@53406
   971
  fixes S :: "'a::euclidean_space set"
huffman@44133
   972
  assumes d: "dim S < DIM('a)"
wenzelm@56444
   973
  shows "\<exists>a::'a. a \<noteq> 0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
wenzelm@49522
   974
proof -
wenzelm@53406
   975
  {
wenzelm@53406
   976
    assume "span S = UNIV"
wenzelm@53406
   977
    then have "dim (span S) = dim (UNIV :: ('a) set)"
wenzelm@53406
   978
      by simp
wenzelm@53406
   979
    then have "dim S = DIM('a)"
immler@68072
   980
      by (metis Euclidean_Space.dim_UNIV dim_span)
wenzelm@53406
   981
    with d have False by arith
wenzelm@53406
   982
  }
wenzelm@53406
   983
  then have th: "span S \<noteq> UNIV"
wenzelm@53406
   984
    by blast
huffman@44133
   985
  from span_not_univ_subset_hyperplane[OF th] show ?thesis .
huffman@44133
   986
qed
huffman@44133
   987
huffman@44133
   988
lemma linear_eq_stdbasis:
wenzelm@56444
   989
  fixes f :: "'a::euclidean_space \<Rightarrow> _"
wenzelm@56444
   990
  assumes lf: "linear f"
wenzelm@49663
   991
    and lg: "linear g"
lp15@68058
   992
    and fg: "\<And>b. b \<in> Basis \<Longrightarrow> f b = g b"
huffman@44133
   993
  shows "f = g"
immler@68072
   994
  using linear_eq_on_span[OF lf lg, of Basis] fg
immler@68072
   995
  by auto
immler@68072
   996
huffman@44133
   997
wenzelm@60420
   998
text \<open>Similar results for bilinear functions.\<close>
huffman@44133
   999
huffman@44133
  1000
lemma bilinear_eq:
huffman@44133
  1001
  assumes bf: "bilinear f"
wenzelm@49522
  1002
    and bg: "bilinear g"
wenzelm@53406
  1003
    and SB: "S \<subseteq> span B"
wenzelm@53406
  1004
    and TC: "T \<subseteq> span C"
lp15@68058
  1005
    and "x\<in>S" "y\<in>T"
lp15@68058
  1006
    and fg: "\<And>x y. \<lbrakk>x \<in> B; y\<in> C\<rbrakk> \<Longrightarrow> f x y = g x y"
lp15@68058
  1007
  shows "f x y = g x y"
wenzelm@49663
  1008
proof -
huffman@44170
  1009
  let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
huffman@44133
  1010
  from bf bg have sp: "subspace ?P"
huffman@53600
  1011
    unfolding bilinear_def linear_iff subspace_def bf bg
immler@68072
  1012
    by (auto simp add: span_zero bilinear_lzero[OF bf] bilinear_lzero[OF bg]
immler@68072
  1013
        span_add Ball_def
wenzelm@49663
  1014
      intro: bilinear_ladd[OF bf])
lp15@68058
  1015
  have sfg: "\<And>x. x \<in> B \<Longrightarrow> subspace {a. f x a = g x a}"
huffman@44133
  1016
    apply (auto simp add: subspace_def)
huffman@53600
  1017
    using bf bg unfolding bilinear_def linear_iff
immler@68072
  1018
      apply (auto simp add: span_zero bilinear_rzero[OF bf] bilinear_rzero[OF bg]
immler@68072
  1019
        span_add Ball_def
wenzelm@49663
  1020
      intro: bilinear_ladd[OF bf])
wenzelm@49522
  1021
    done
lp15@68058
  1022
  have "\<forall>y\<in> span C. f x y = g x y" if "x \<in> span B" for x
lp15@68058
  1023
    apply (rule span_induct [OF that sp])
lp15@68062
  1024
    using fg sfg span_induct by blast
wenzelm@53406
  1025
  then show ?thesis
lp15@68058
  1026
    using SB TC assms by auto
huffman@44133
  1027
qed
huffman@44133
  1028
wenzelm@49522
  1029
lemma bilinear_eq_stdbasis:
wenzelm@53406
  1030
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> _"
huffman@44133
  1031
  assumes bf: "bilinear f"
wenzelm@49522
  1032
    and bg: "bilinear g"
lp15@68058
  1033
    and fg: "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> f i j = g i j"
huffman@44133
  1034
  shows "f = g"
immler@68074
  1035
  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg by blast
wenzelm@49522
  1036
immler@69619
  1037
wenzelm@60420
  1038
subsection \<open>Infinity norm\<close>
huffman@44133
  1039
immler@67962
  1040
definition%important "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
huffman@44133
  1041
huffman@44133
  1042
lemma infnorm_set_image:
wenzelm@53716
  1043
  fixes x :: "'a::euclidean_space"
wenzelm@56444
  1044
  shows "{\<bar>x \<bullet> i\<bar> |i. i \<in> Basis} = (\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
hoelzl@50526
  1045
  by blast
huffman@44133
  1046
wenzelm@53716
  1047
lemma infnorm_Max:
wenzelm@53716
  1048
  fixes x :: "'a::euclidean_space"
wenzelm@56444
  1049
  shows "infnorm x = Max ((\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis)"
haftmann@62343
  1050
  by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
hoelzl@51475
  1051
huffman@44133
  1052
lemma infnorm_set_lemma:
wenzelm@53716
  1053
  fixes x :: "'a::euclidean_space"
wenzelm@56444
  1054
  shows "finite {\<bar>x \<bullet> i\<bar> |i. i \<in> Basis}"
wenzelm@56444
  1055
    and "{\<bar>x \<bullet> i\<bar> |i. i \<in> Basis} \<noteq> {}"
huffman@44133
  1056
  unfolding infnorm_set_image
huffman@44133
  1057
  by auto
huffman@44133
  1058
wenzelm@53406
  1059
lemma infnorm_pos_le:
wenzelm@53406
  1060
  fixes x :: "'a::euclidean_space"
wenzelm@53406
  1061
  shows "0 \<le> infnorm x"
hoelzl@51475
  1062
  by (simp add: infnorm_Max Max_ge_iff ex_in_conv)
huffman@44133
  1063
wenzelm@53406
  1064
lemma infnorm_triangle:
wenzelm@53406
  1065
  fixes x :: "'a::euclidean_space"
wenzelm@53406
  1066
  shows "infnorm (x + y) \<le> infnorm x + infnorm y"
wenzelm@49522
  1067
proof -
hoelzl@51475
  1068
  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
  1069
    by simp
huffman@44133
  1070
  show ?thesis
hoelzl@51475
  1071
    by (auto simp: infnorm_Max inner_add_left intro!: *)
huffman@44133
  1072
qed
huffman@44133
  1073
wenzelm@53406
  1074
lemma infnorm_eq_0:
wenzelm@53406
  1075
  fixes x :: "'a::euclidean_space"
wenzelm@53406
  1076
  shows "infnorm x = 0 \<longleftrightarrow> x = 0"
wenzelm@49522
  1077
proof -
hoelzl@51475
  1078
  have "infnorm x \<le> 0 \<longleftrightarrow> x = 0"
hoelzl@51475
  1079
    unfolding infnorm_Max by (simp add: euclidean_all_zero_iff)
hoelzl@51475
  1080
  then show ?thesis
hoelzl@51475
  1081
    using infnorm_pos_le[of x] by simp
huffman@44133
  1082
qed
huffman@44133
  1083
huffman@44133
  1084
lemma infnorm_0: "infnorm 0 = 0"
huffman@44133
  1085
  by (simp add: infnorm_eq_0)
huffman@44133
  1086
huffman@44133
  1087
lemma infnorm_neg: "infnorm (- x) = infnorm x"
lp15@68062
  1088
  unfolding infnorm_def by simp
huffman@44133
  1089
huffman@44133
  1090
lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
lp15@68062
  1091
  by (metis infnorm_neg minus_diff_eq)
lp15@68062
  1092
lp15@68062
  1093
lemma absdiff_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
wenzelm@49522
  1094
proof -
lp15@68062
  1095
  have *: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
huffman@44133
  1096
    by arith
lp15@68062
  1097
  show ?thesis
lp15@68062
  1098
  proof (rule *)
lp15@68062
  1099
    from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
lp15@68062
  1100
    show "infnorm x \<le> infnorm (x - y) + infnorm y" "infnorm y \<le> infnorm (x - y) + infnorm x"
lp15@68062
  1101
      by (simp_all add: field_simps infnorm_neg)
lp15@68062
  1102
  qed
huffman@44133
  1103
qed
huffman@44133
  1104
wenzelm@53406
  1105
lemma real_abs_infnorm: "\<bar>infnorm x\<bar> = infnorm x"
huffman@44133
  1106
  using infnorm_pos_le[of x] by arith
huffman@44133
  1107
hoelzl@50526
  1108
lemma Basis_le_infnorm:
wenzelm@53406
  1109
  fixes x :: "'a::euclidean_space"
wenzelm@53406
  1110
  shows "b \<in> Basis \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> infnorm x"
hoelzl@51475
  1111
  by (simp add: infnorm_Max)
huffman@44133
  1112
wenzelm@56444
  1113
lemma infnorm_mul: "infnorm (a *\<^sub>R x) = \<bar>a\<bar> * infnorm x"
hoelzl@51475
  1114
  unfolding infnorm_Max
hoelzl@51475
  1115
proof (safe intro!: Max_eqI)
hoelzl@51475
  1116
  let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
lp15@68062
  1117
  { fix b :: 'a
wenzelm@53406
  1118
    assume "b \<in> Basis"
wenzelm@53406
  1119
    then show "\<bar>a *\<^sub>R x \<bullet> b\<bar> \<le> \<bar>a\<bar> * Max ?B"
wenzelm@53406
  1120
      by (simp add: abs_mult mult_left_mono)
wenzelm@53406
  1121
  next
wenzelm@53406
  1122
    from Max_in[of ?B] obtain b where "b \<in> Basis" "Max ?B = \<bar>x \<bullet> b\<bar>"
wenzelm@53406
  1123
      by (auto simp del: Max_in)
wenzelm@53406
  1124
    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
  1125
      by (intro image_eqI[where x=b]) (auto simp: abs_mult)
wenzelm@53406
  1126
  }
hoelzl@51475
  1127
qed simp
hoelzl@51475
  1128
wenzelm@53406
  1129
lemma infnorm_mul_lemma: "infnorm (a *\<^sub>R x) \<le> \<bar>a\<bar> * infnorm x"
hoelzl@51475
  1130
  unfolding infnorm_mul ..
huffman@44133
  1131
huffman@44133
  1132
lemma infnorm_pos_lt: "infnorm x > 0 \<longleftrightarrow> x \<noteq> 0"
huffman@44133
  1133
  using infnorm_pos_le[of x] infnorm_eq_0[of x] by arith
huffman@44133
  1134
wenzelm@60420
  1135
text \<open>Prove that it differs only up to a bound from Euclidean norm.\<close>
huffman@44133
  1136
huffman@44133
  1137
lemma infnorm_le_norm: "infnorm x \<le> norm x"
hoelzl@51475
  1138
  by (simp add: Basis_le_norm infnorm_Max)
hoelzl@50526
  1139
wenzelm@53716
  1140
lemma norm_le_infnorm:
wenzelm@53716
  1141
  fixes x :: "'a::euclidean_space"
wenzelm@53716
  1142
  shows "norm x \<le> sqrt DIM('a) * infnorm x"
lp15@68062
  1143
  unfolding norm_eq_sqrt_inner id_def 
lp15@68062
  1144
proof (rule real_le_lsqrt[OF inner_ge_zero])
lp15@68062
  1145
  show "sqrt DIM('a) * infnorm x \<ge> 0"
huffman@44133
  1146
    by (simp add: zero_le_mult_iff infnorm_pos_le)
lp15@68062
  1147
  have "x \<bullet> x \<le> (\<Sum>b\<in>Basis. x \<bullet> b * (x \<bullet> b))"
lp15@68062
  1148
    by (metis euclidean_inner order_refl)
lp15@68062
  1149
  also have "... \<le> DIM('a) * \<bar>infnorm x\<bar>\<^sup>2"
lp15@68062
  1150
    by (rule sum_bounded_above) (metis Basis_le_infnorm abs_le_square_iff power2_eq_square real_abs_infnorm)
lp15@68062
  1151
  also have "... \<le> (sqrt DIM('a) * infnorm x)\<^sup>2"
lp15@68062
  1152
    by (simp add: power_mult_distrib)
lp15@68062
  1153
  finally show "x \<bullet> x \<le> (sqrt DIM('a) * infnorm x)\<^sup>2" .
huffman@44133
  1154
qed
huffman@44133
  1155
huffman@44646
  1156
lemma tendsto_infnorm [tendsto_intros]:
wenzelm@61973
  1157
  assumes "(f \<longlongrightarrow> a) F"
wenzelm@61973
  1158
  shows "((\<lambda>x. infnorm (f x)) \<longlongrightarrow> infnorm a) F"
huffman@44646
  1159
proof (rule tendsto_compose [OF LIM_I assms])
wenzelm@53406
  1160
  fix r :: real
wenzelm@53406
  1161
  assume "r > 0"
wenzelm@49522
  1162
  then show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (infnorm x - infnorm a) < r"
lp15@68062
  1163
    by (metis real_norm_def le_less_trans absdiff_infnorm infnorm_le_norm)
huffman@44646
  1164
qed
huffman@44646
  1165
wenzelm@60420
  1166
text \<open>Equality in Cauchy-Schwarz and triangle inequalities.\<close>
huffman@44133
  1167
wenzelm@53406
  1168
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
  1169
  (is "?lhs \<longleftrightarrow> ?rhs")
lp15@68062
  1170
proof (cases "x=0")
lp15@68062
  1171
  case True
lp15@68062
  1172
  then show ?thesis 
lp15@68062
  1173
    by auto
lp15@68062
  1174
next
lp15@68062
  1175
  case False
lp15@68062
  1176
  from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
lp15@68062
  1177
  have "?rhs \<longleftrightarrow>
wenzelm@49522
  1178
      (norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) -
wenzelm@49522
  1179
        norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) =  0)"
lp15@68062
  1180
    using False unfolding inner_simps
lp15@68062
  1181
    by (auto simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
lp15@68062
  1182
  also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" 
lp15@68062
  1183
    using False  by (simp add: field_simps inner_commute)
lp15@68062
  1184
  also have "\<dots> \<longleftrightarrow> ?lhs" 
lp15@68062
  1185
    using False by auto
lp15@68062
  1186
  finally show ?thesis by metis
huffman@44133
  1187
qed
huffman@44133
  1188
huffman@44133
  1189
lemma norm_cauchy_schwarz_abs_eq:
wenzelm@56444
  1190
  "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow>
wenzelm@53716
  1191
    norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm x *\<^sub>R y = - norm y *\<^sub>R x"
wenzelm@53406
  1192
  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@49522
  1193
proof -
wenzelm@56444
  1194
  have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> \<bar>x\<bar> = a \<longleftrightarrow> x = a \<or> x = - a"
wenzelm@53406
  1195
    by arith
huffman@44133
  1196
  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
  1197
    by simp
lp15@68062
  1198
  also have "\<dots> \<longleftrightarrow> (x \<bullet> y = norm x * norm y \<or> (- x) \<bullet> y = norm x * norm y)"
huffman@44133
  1199
    unfolding norm_cauchy_schwarz_eq[symmetric]
huffman@44133
  1200
    unfolding norm_minus_cancel norm_scaleR ..
huffman@44133
  1201
  also have "\<dots> \<longleftrightarrow> ?lhs"
wenzelm@53406
  1202
    unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] inner_simps
wenzelm@53406
  1203
    by auto
huffman@44133
  1204
  finally show ?thesis ..
huffman@44133
  1205
qed
huffman@44133
  1206
huffman@44133
  1207
lemma norm_triangle_eq:
huffman@44133
  1208
  fixes x y :: "'a::real_inner"
wenzelm@53406
  1209
  shows "norm (x + y) = norm x + norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
lp15@68062
  1210
proof (cases "x = 0 \<or> y = 0")
lp15@68062
  1211
  case True
lp15@68062
  1212
  then show ?thesis 
lp15@68062
  1213
    by force
lp15@68062
  1214
next
lp15@68062
  1215
  case False
lp15@68062
  1216
  then have n: "norm x > 0" "norm y > 0"
lp15@68062
  1217
    by auto
lp15@68062
  1218
  have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
lp15@68062
  1219
    by simp
lp15@68062
  1220
  also have "\<dots> \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
lp15@68062
  1221
    unfolding norm_cauchy_schwarz_eq[symmetric]
lp15@68062
  1222
    unfolding power2_norm_eq_inner inner_simps
lp15@68062
  1223
    by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
lp15@68062
  1224
  finally show ?thesis .
huffman@44133
  1225
qed
huffman@44133
  1226
wenzelm@49522
  1227
wenzelm@60420
  1228
subsection \<open>Collinearity\<close>
huffman@44133
  1229
immler@67962
  1230
definition%important collinear :: "'a::real_vector set \<Rightarrow> bool"
wenzelm@49522
  1231
  where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
huffman@44133
  1232
lp15@66287
  1233
lemma collinear_alt:
lp15@66287
  1234
     "collinear S \<longleftrightarrow> (\<exists>u v. \<forall>x \<in> S. \<exists>c. x = u + c *\<^sub>R v)" (is "?lhs = ?rhs")
lp15@66287
  1235
proof
lp15@66287
  1236
  assume ?lhs
lp15@66287
  1237
  then show ?rhs
lp15@66287
  1238
    unfolding collinear_def by (metis Groups.add_ac(2) diff_add_cancel)
lp15@66287
  1239
next
lp15@66287
  1240
  assume ?rhs
lp15@66287
  1241
  then obtain u v where *: "\<And>x. x \<in> S \<Longrightarrow> \<exists>c. x = u + c *\<^sub>R v"
lp15@66287
  1242
    by (auto simp: )
lp15@66287
  1243
  have "\<exists>c. x - y = c *\<^sub>R v" if "x \<in> S" "y \<in> S" for x y
lp15@66287
  1244
        by (metis *[OF \<open>x \<in> S\<close>] *[OF \<open>y \<in> S\<close>] scaleR_left.diff add_diff_cancel_left)
lp15@66287
  1245
  then show ?lhs
lp15@66287
  1246
    using collinear_def by blast
lp15@66287
  1247
qed
lp15@66287
  1248
lp15@66287
  1249
lemma collinear:
lp15@66287
  1250
  fixes S :: "'a::{perfect_space,real_vector} set"
lp15@66287
  1251
  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
  1252
proof -
lp15@66287
  1253
  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
  1254
    if "\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R u" "u=0" for u
lp15@66287
  1255
  proof -
lp15@66287
  1256
    have "\<forall>x\<in>S. \<forall>y\<in>S. x = y"
lp15@66287
  1257
      using that by auto
lp15@66287
  1258
    moreover
lp15@66287
  1259
    obtain v::'a where "v \<noteq> 0"
lp15@66287
  1260
      using UNIV_not_singleton [of 0] by auto
lp15@66287
  1261
    ultimately have "\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R v"
lp15@66287
  1262
      by auto
lp15@66287
  1263
    then show ?thesis
lp15@66287
  1264
      using \<open>v \<noteq> 0\<close> by blast
lp15@66287
  1265
  qed
lp15@66287
  1266
  then show ?thesis
lp15@66287
  1267
    apply (clarsimp simp: collinear_def)
immler@68072
  1268
    by (metis scaleR_zero_right vector_fraction_eq_iff)
lp15@66287
  1269
qed
lp15@66287
  1270
lp15@63881
  1271
lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S"
lp15@63881
  1272
  by (meson collinear_def subsetCE)
lp15@63881
  1273
paulson@60762
  1274
lemma collinear_empty [iff]: "collinear {}"
wenzelm@53406
  1275
  by (simp add: collinear_def)
huffman@44133
  1276
paulson@60762
  1277
lemma collinear_sing [iff]: "collinear {x}"
huffman@44133
  1278
  by (simp add: collinear_def)
huffman@44133
  1279
paulson@60762
  1280
lemma collinear_2 [iff]: "collinear {x, y}"
huffman@44133
  1281
  apply (simp add: collinear_def)
huffman@44133
  1282
  apply (rule exI[where x="x - y"])
lp15@68062
  1283
  by (metis minus_diff_eq scaleR_left.minus scaleR_one)
huffman@44133
  1284
wenzelm@56444
  1285
lemma collinear_lemma: "collinear {0, x, y} \<longleftrightarrow> x = 0 \<or> y = 0 \<or> (\<exists>c. y = c *\<^sub>R x)"
wenzelm@53406
  1286
  (is "?lhs \<longleftrightarrow> ?rhs")
lp15@68062
  1287
proof (cases "x = 0 \<or> y = 0")
lp15@68062
  1288
  case True
lp15@68062
  1289
  then show ?thesis
lp15@68062
  1290
    by (auto simp: insert_commute)
lp15@68062
  1291
next
lp15@68062
  1292
  case False
lp15@68062
  1293
  show ?thesis 
lp15@68062
  1294
  proof
lp15@68062
  1295
    assume h: "?lhs"
lp15@68062
  1296
    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"
lp15@68062
  1297
      unfolding collinear_def by blast
lp15@68062
  1298
    from u[rule_format, of x 0] u[rule_format, of y 0]
lp15@68062
  1299
    obtain cx and cy where
lp15@68062
  1300
      cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
lp15@68062
  1301
      by auto
lp15@68062
  1302
    from cx cy False have cx0: "cx \<noteq> 0" and cy0: "cy \<noteq> 0" by auto
lp15@68062
  1303
    let ?d = "cy / cx"
lp15@68062
  1304
    from cx cy cx0 have "y = ?d *\<^sub>R x"
lp15@68062
  1305
      by simp
lp15@68062
  1306
    then show ?rhs using False by blast
lp15@68062
  1307
  next
lp15@68062
  1308
    assume h: "?rhs"
lp15@68062
  1309
    then obtain c where c: "y = c *\<^sub>R x"
lp15@68062
  1310
      using False by blast
lp15@68062
  1311
    show ?lhs
lp15@68062
  1312
      unfolding collinear_def c
lp15@68062
  1313
      apply (rule exI[where x=x])
lp15@68062
  1314
      apply auto
lp15@68062
  1315
          apply (rule exI[where x="- 1"], simp)
lp15@68062
  1316
         apply (rule exI[where x= "-c"], simp)
huffman@44133
  1317
        apply (rule exI[where x=1], simp)
lp15@68062
  1318
       apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib)
lp15@68062
  1319
      apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib)
lp15@68062
  1320
      done
lp15@68062
  1321
  qed
huffman@44133
  1322
qed
huffman@44133
  1323
wenzelm@56444
  1324
lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
lp15@68062
  1325
proof (cases "x=0")
lp15@68062
  1326
  case True
lp15@68062
  1327
  then show ?thesis
lp15@68062
  1328
    by (auto simp: insert_commute)
lp15@68062
  1329
next
lp15@68062
  1330
  case False
lp15@68062
  1331
  then have nnz: "norm x \<noteq> 0"
lp15@68062
  1332
    by auto
lp15@68062
  1333
  show ?thesis
lp15@68062
  1334
  proof
lp15@68062
  1335
    assume "\<bar>x \<bullet> y\<bar> = norm x * norm y"
lp15@68062
  1336
    then show "collinear {0, x, y}"
lp15@68062
  1337
      unfolding norm_cauchy_schwarz_abs_eq collinear_lemma 
lp15@68062
  1338
      by (meson eq_vector_fraction_iff nnz)
lp15@68062
  1339
  next
lp15@68062
  1340
    assume "collinear {0, x, y}"
lp15@68062
  1341
    with False show "\<bar>x \<bullet> y\<bar> = norm x * norm y"
lp15@68062
  1342
      unfolding norm_cauchy_schwarz_abs_eq collinear_lemma  by (auto simp: abs_if)
lp15@68062
  1343
  qed
lp15@68062
  1344
qed
wenzelm@49522
  1345
immler@69675
  1346
immler@69675
  1347
subsection\<open>Properties of special hyperplanes\<close>
immler@69675
  1348
immler@69675
  1349
lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}"
immler@69675
  1350
  by (simp add: subspace_def inner_right_distrib)
immler@69675
  1351
immler@69675
  1352
lemma subspace_hyperplane2: "subspace {x. x \<bullet> a = 0}"
immler@69675
  1353
  by (simp add: inner_commute inner_right_distrib subspace_def)
immler@69675
  1354
immler@69675
  1355
lemma special_hyperplane_span:
immler@69675
  1356
  fixes S :: "'n::euclidean_space set"
immler@69675
  1357
  assumes "k \<in> Basis"
immler@69675
  1358
  shows "{x. k \<bullet> x = 0} = span (Basis - {k})"
immler@69675
  1359
proof -
immler@69675
  1360
  have *: "x \<in> span (Basis - {k})" if "k \<bullet> x = 0" for x
immler@69675
  1361
  proof -
immler@69675
  1362
    have "x = (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b)"
immler@69675
  1363
      by (simp add: euclidean_representation)
immler@69675
  1364
    also have "... = (\<Sum>b \<in> Basis - {k}. (x \<bullet> b) *\<^sub>R b)"
immler@69675
  1365
      by (auto simp: sum.remove [of _ k] inner_commute assms that)
immler@69675
  1366
    finally have "x = (\<Sum>b\<in>Basis - {k}. (x \<bullet> b) *\<^sub>R b)" .
immler@69675
  1367
    then show ?thesis
immler@69675
  1368
      by (simp add: span_finite)
immler@69675
  1369
  qed
immler@69675
  1370
  show ?thesis
immler@69675
  1371
    apply (rule span_subspace [symmetric])
immler@69675
  1372
    using assms
immler@69675
  1373
    apply (auto simp: inner_not_same_Basis intro: * subspace_hyperplane)
immler@69675
  1374
    done
immler@69675
  1375
qed
immler@69675
  1376
immler@69675
  1377
lemma dim_special_hyperplane:
immler@69675
  1378
  fixes k :: "'n::euclidean_space"
immler@69675
  1379
  shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1"
immler@69675
  1380
apply (simp add: special_hyperplane_span)
immler@69675
  1381
apply (rule dim_unique [OF subset_refl])
immler@69675
  1382
apply (auto simp: independent_substdbasis)
immler@69675
  1383
apply (metis member_remove remove_def span_base)
immler@69675
  1384
done
immler@69675
  1385
immler@69675
  1386
proposition dim_hyperplane:
immler@69675
  1387
  fixes a :: "'a::euclidean_space"
immler@69675
  1388
  assumes "a \<noteq> 0"
immler@69675
  1389
    shows "dim {x. a \<bullet> x = 0} = DIM('a) - 1"
immler@69675
  1390
proof -
immler@69675
  1391
  have span0: "span {x. a \<bullet> x = 0} = {x. a \<bullet> x = 0}"
immler@69675
  1392
    by (rule span_unique) (auto simp: subspace_hyperplane)
immler@69675
  1393
  then obtain B where "independent B"
immler@69675
  1394
              and Bsub: "B \<subseteq> {x. a \<bullet> x = 0}"
immler@69675
  1395
              and subspB: "{x. a \<bullet> x = 0} \<subseteq> span B"
immler@69675
  1396
              and card0: "(card B = dim {x. a \<bullet> x = 0})"
immler@69675
  1397
              and ortho: "pairwise orthogonal B"
immler@69675
  1398
    using orthogonal_basis_exists by metis
immler@69675
  1399
  with assms have "a \<notin> span B"
immler@69675
  1400
    by (metis (mono_tags, lifting) span_eq inner_eq_zero_iff mem_Collect_eq span0)
immler@69675
  1401
  then have ind: "independent (insert a B)"
immler@69675
  1402
    by (simp add: \<open>independent B\<close> independent_insert)
immler@69675
  1403
  have "finite B"
immler@69675
  1404
    using \<open>independent B\<close> independent_bound by blast
immler@69675
  1405
  have "UNIV \<subseteq> span (insert a B)"
immler@69675
  1406
  proof fix y::'a
immler@69675
  1407
    obtain r z where z: "y = r *\<^sub>R a + z" "a \<bullet> z = 0"
immler@69675
  1408
      apply (rule_tac r="(a \<bullet> y) / (a \<bullet> a)" and z = "y - ((a \<bullet> y) / (a \<bullet> a)) *\<^sub>R a" in that)
immler@69675
  1409
      using assms
immler@69675
  1410
      by (auto simp: algebra_simps)
immler@69675
  1411
    show "y \<in> span (insert a B)"
immler@69675
  1412
      by (metis (mono_tags, lifting) z Bsub span_eq_iff
immler@69675
  1413
         add_diff_cancel_left' mem_Collect_eq span0 span_breakdown_eq span_subspace subspB)
immler@69675
  1414
  qed
immler@69675
  1415
  then have dima: "DIM('a) = dim(insert a B)"
immler@69675
  1416
    by (metis independent_Basis span_Basis dim_eq_card top.extremum_uniqueI)
immler@69675
  1417
  then show ?thesis
immler@69675
  1418
    by (metis (mono_tags, lifting) Bsub Diff_insert_absorb \<open>a \<notin> span B\<close> ind card0
immler@69675
  1419
        card_Diff_singleton dim_span indep_card_eq_dim_span insertI1 subsetCE
immler@69675
  1420
        subspB)
immler@69675
  1421
qed
immler@69675
  1422
immler@69675
  1423
lemma lowdim_eq_hyperplane:
immler@69675
  1424
  fixes S :: "'a::euclidean_space set"
immler@69675
  1425
  assumes "dim S = DIM('a) - 1"
immler@69675
  1426
  obtains a where "a \<noteq> 0" and "span S = {x. a \<bullet> x = 0}"
immler@69675
  1427
proof -
immler@69675
  1428
  have dimS: "dim S < DIM('a)"
immler@69675
  1429
    by (simp add: assms)
immler@69675
  1430
  then obtain b where b: "b \<noteq> 0" "span S \<subseteq> {a. b \<bullet> a = 0}"
immler@69675
  1431
    using lowdim_subset_hyperplane [of S] by fastforce
immler@69675
  1432
  show ?thesis
immler@69675
  1433
    apply (rule that[OF b(1)])
immler@69675
  1434
    apply (rule subspace_dim_equal)
immler@69675
  1435
    by (auto simp: assms b dim_hyperplane dim_span subspace_hyperplane
immler@69675
  1436
        subspace_span)
immler@69675
  1437
qed
immler@69675
  1438
immler@69675
  1439
lemma dim_eq_hyperplane:
immler@69675
  1440
  fixes S :: "'n::euclidean_space set"
immler@69675
  1441
  shows "dim S = DIM('n) - 1 \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> span S = {x. a \<bullet> x = 0})"
immler@69675
  1442
by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane)
immler@69675
  1443
immler@69675
  1444
immler@69675
  1445
subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
immler@69675
  1446
immler@69675
  1447
lemma pairwise_orthogonal_independent:
immler@69675
  1448
  assumes "pairwise orthogonal S" and "0 \<notin> S"
immler@69675
  1449
    shows "independent S"
immler@69675
  1450
proof -
immler@69675
  1451
  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
immler@69675
  1452
    using assms by (simp add: pairwise_def orthogonal_def)
immler@69675
  1453
  have "False" if "a \<in> S" and a: "a \<in> span (S - {a})" for a
immler@69675
  1454
  proof -
immler@69675
  1455
    obtain T U where "T \<subseteq> S - {a}" "a = (\<Sum>v\<in>T. U v *\<^sub>R v)"
immler@69675
  1456
      using a by (force simp: span_explicit)
immler@69675
  1457
    then have "a \<bullet> a = a \<bullet> (\<Sum>v\<in>T. U v *\<^sub>R v)"
immler@69675
  1458
      by simp
immler@69675
  1459
    also have "... = 0"
immler@69675
  1460
      apply (simp add: inner_sum_right)
immler@69675
  1461
      apply (rule comm_monoid_add_class.sum.neutral)
immler@69675
  1462
      by (metis "0" DiffE \<open>T \<subseteq> S - {a}\<close> mult_not_zero singletonI subsetCE \<open>a \<in> S\<close>)
immler@69675
  1463
    finally show ?thesis
immler@69675
  1464
      using \<open>0 \<notin> S\<close> \<open>a \<in> S\<close> by auto
immler@69675
  1465
  qed
immler@69675
  1466
  then show ?thesis
immler@69675
  1467
    by (force simp: dependent_def)
immler@69675
  1468
qed
immler@69675
  1469
immler@69675
  1470
lemma pairwise_orthogonal_imp_finite:
immler@69675
  1471
  fixes S :: "'a::euclidean_space set"
immler@69675
  1472
  assumes "pairwise orthogonal S"
immler@69675
  1473
    shows "finite S"
immler@69675
  1474
proof -
immler@69675
  1475
  have "independent (S - {0})"
immler@69675
  1476
    apply (rule pairwise_orthogonal_independent)
immler@69675
  1477
     apply (metis Diff_iff assms pairwise_def)
immler@69675
  1478
    by blast
immler@69675
  1479
  then show ?thesis
immler@69675
  1480
    by (meson independent_imp_finite infinite_remove)
immler@69675
  1481
qed
immler@69675
  1482
immler@69675
  1483
lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}"
immler@69675
  1484
  by (simp add: subspace_def orthogonal_clauses)
immler@69675
  1485
immler@69675
  1486
lemma subspace_orthogonal_to_vectors: "subspace {y. \<forall>x \<in> S. orthogonal x y}"
immler@69675
  1487
  by (simp add: subspace_def orthogonal_clauses)
immler@69675
  1488
immler@69675
  1489
lemma orthogonal_to_span:
immler@69675
  1490
  assumes a: "a \<in> span S" and x: "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
immler@69675
  1491
    shows "orthogonal x a"
immler@69675
  1492
  by (metis a orthogonal_clauses(1,2,4)
immler@69675
  1493
      span_induct_alt x)
immler@69675
  1494
immler@69675
  1495
proposition Gram_Schmidt_step:
immler@69675
  1496
  fixes S :: "'a::euclidean_space set"
immler@69675
  1497
  assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
immler@69675
  1498
    shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
immler@69675
  1499
proof -
immler@69675
  1500
  have "finite S"
immler@69675
  1501
    by (simp add: S pairwise_orthogonal_imp_finite)
immler@69675
  1502
  have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
immler@69675
  1503
       if "x \<in> S" for x
immler@69675
  1504
  proof -
immler@69675
  1505
    have "a \<bullet> x = (\<Sum>y\<in>S. if y = x then y \<bullet> a else 0)"
immler@69675
  1506
      by (simp add: \<open>finite S\<close> inner_commute sum.delta that)
immler@69675
  1507
    also have "... =  (\<Sum>b\<in>S. b \<bullet> a * (b \<bullet> x) / (b \<bullet> b))"
immler@69675
  1508
      apply (rule sum.cong [OF refl], simp)
immler@69675
  1509
      by (meson S orthogonal_def pairwise_def that)
immler@69675
  1510
   finally show ?thesis
immler@69675
  1511
     by (simp add: orthogonal_def algebra_simps inner_sum_left)
immler@69675
  1512
  qed
immler@69675
  1513
  then show ?thesis
immler@69675
  1514
    using orthogonal_to_span orthogonal_commute x by blast
immler@69675
  1515
qed
immler@69675
  1516
immler@69675
  1517
immler@69675
  1518
lemma orthogonal_extension_aux:
immler@69675
  1519
  fixes S :: "'a::euclidean_space set"
immler@69675
  1520
  assumes "finite T" "finite S" "pairwise orthogonal S"
immler@69675
  1521
    shows "\<exists>U. pairwise orthogonal (S \<union> U) \<and> span (S \<union> U) = span (S \<union> T)"
immler@69675
  1522
using assms
immler@69675
  1523
proof (induction arbitrary: S)
immler@69675
  1524
  case empty then show ?case
immler@69675
  1525
    by simp (metis sup_bot_right)
immler@69675
  1526
next
immler@69675
  1527
  case (insert a T)
immler@69675
  1528
  have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
immler@69675
  1529
    using insert by (simp add: pairwise_def orthogonal_def)
immler@69675
  1530
  define a' where "a' = a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)"
immler@69675
  1531
  obtain U where orthU: "pairwise orthogonal (S \<union> insert a' U)"
immler@69675
  1532
             and spanU: "span (insert a' S \<union> U) = span (insert a' S \<union> T)"
immler@69675
  1533
    by (rule exE [OF insert.IH [of "insert a' S"]])
immler@69675
  1534
      (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute
immler@69675
  1535
        pairwise_orthogonal_insert span_clauses)
immler@69675
  1536
  have orthS: "\<And>x. x \<in> S \<Longrightarrow> a' \<bullet> x = 0"
immler@69675
  1537
    apply (simp add: a'_def)
immler@69675
  1538
    using Gram_Schmidt_step [OF \<open>pairwise orthogonal S\<close>]
immler@69675
  1539
    apply (force simp: orthogonal_def inner_commute span_superset [THEN subsetD])
immler@69675
  1540
    done
immler@69675
  1541
  have "span (S \<union> insert a' U) = span (insert a' (S \<union> T))"
immler@69675
  1542
    using spanU by simp
immler@69675
  1543
  also have "... = span (insert a (S \<union> T))"
immler@69675
  1544
    apply (rule eq_span_insert_eq)
immler@69675
  1545
    apply (simp add: a'_def span_neg span_sum span_base span_mul)
immler@69675
  1546
    done
immler@69675
  1547
  also have "... = span (S \<union> insert a T)"
immler@69675
  1548
    by simp
immler@69675
  1549
  finally show ?case
immler@69675
  1550
    by (rule_tac x="insert a' U" in exI) (use orthU in auto)
immler@69675
  1551
qed
immler@69675
  1552
immler@69675
  1553
immler@69675
  1554
proposition orthogonal_extension:
immler@69675
  1555
  fixes S :: "'a::euclidean_space set"
immler@69675
  1556
  assumes S: "pairwise orthogonal S"
immler@69675
  1557
  obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
immler@69675
  1558
proof -
immler@69675
  1559
  obtain B where "finite B" "span B = span T"
immler@69675
  1560
    using basis_subspace_exists [of "span T"] subspace_span by metis
immler@69675
  1561
  with orthogonal_extension_aux [of B S]
immler@69675
  1562
  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> B)"
immler@69675
  1563
    using assms pairwise_orthogonal_imp_finite by auto
immler@69675
  1564
  with \<open>span B = span T\<close> show ?thesis
immler@69675
  1565
    by (rule_tac U=U in that) (auto simp: span_Un)
immler@69675
  1566
qed
immler@69675
  1567
immler@69675
  1568
corollary%unimportant orthogonal_extension_strong:
immler@69675
  1569
  fixes S :: "'a::euclidean_space set"
immler@69675
  1570
  assumes S: "pairwise orthogonal S"
immler@69675
  1571
  obtains U where "U \<inter> (insert 0 S) = {}" "pairwise orthogonal (S \<union> U)"
immler@69675
  1572
                  "span (S \<union> U) = span (S \<union> T)"
immler@69675
  1573
proof -
immler@69675
  1574
  obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
immler@69675
  1575
    using orthogonal_extension assms by blast
immler@69675
  1576
  then show ?thesis
immler@69675
  1577
    apply (rule_tac U = "U - (insert 0 S)" in that)
immler@69675
  1578
      apply blast
immler@69675
  1579
     apply (force simp: pairwise_def)
immler@69675
  1580
    apply (metis Un_Diff_cancel Un_insert_left span_redundant span_zero)
immler@69675
  1581
    done
immler@69675
  1582
qed
immler@69675
  1583
immler@69675
  1584
subsection\<open>Decomposing a vector into parts in orthogonal subspaces\<close>
immler@69675
  1585
immler@69675
  1586
text\<open>existence of orthonormal basis for a subspace.\<close>
immler@69675
  1587
immler@69675
  1588
lemma orthogonal_spanningset_subspace:
immler@69675
  1589
  fixes S :: "'a :: euclidean_space set"
immler@69675
  1590
  assumes "subspace S"
immler@69675
  1591
  obtains B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
immler@69675
  1592
proof -
immler@69675
  1593
  obtain B where "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
immler@69675
  1594
    using basis_exists by blast
immler@69675
  1595
  with orthogonal_extension [of "{}" B]
immler@69675
  1596
  show ?thesis
immler@69675
  1597
    by (metis Un_empty_left assms pairwise_empty span_superset span_subspace that)
immler@69675
  1598
qed
immler@69675
  1599
immler@69675
  1600
lemma orthogonal_basis_subspace:
immler@69675
  1601
  fixes S :: "'a :: euclidean_space set"
immler@69675
  1602
  assumes "subspace S"
immler@69675
  1603
  obtains B where "0 \<notin> B" "B \<subseteq> S" "pairwise orthogonal B" "independent B"
immler@69675
  1604
                  "card B = dim S" "span B = S"
immler@69675
  1605
proof -
immler@69675
  1606
  obtain B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S"
immler@69675
  1607
    using assms orthogonal_spanningset_subspace by blast
immler@69675
  1608
  then show ?thesis
immler@69675
  1609
    apply (rule_tac B = "B - {0}" in that)
immler@69675
  1610
    apply (auto simp: indep_card_eq_dim_span pairwise_subset pairwise_orthogonal_independent elim: pairwise_subset)
immler@69675
  1611
    done
immler@69675
  1612
qed
immler@69675
  1613
immler@69675
  1614
proposition orthonormal_basis_subspace:
immler@69675
  1615
  fixes S :: "'a :: euclidean_space set"
immler@69675
  1616
  assumes "subspace S"
immler@69675
  1617
  obtains B where "B \<subseteq> S" "pairwise orthogonal B"
immler@69675
  1618
              and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
immler@69675
  1619
              and "independent B" "card B = dim S" "span B = S"
immler@69675
  1620
proof -
immler@69675
  1621
  obtain B where "0 \<notin> B" "B \<subseteq> S"
immler@69675
  1622
             and orth: "pairwise orthogonal B"
immler@69675
  1623
             and "independent B" "card B = dim S" "span B = S"
immler@69675
  1624
    by (blast intro: orthogonal_basis_subspace [OF assms])
immler@69675
  1625
  have 1: "(\<lambda>x. x /\<^sub>R norm x) ` B \<subseteq> S"
immler@69675
  1626
    using \<open>span B = S\<close> span_superset span_mul by fastforce
immler@69675
  1627
  have 2: "pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` B)"
immler@69675
  1628
    using orth by (force simp: pairwise_def orthogonal_clauses)
immler@69675
  1629
  have 3: "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` B \<Longrightarrow> norm x = 1"
immler@69675
  1630
    by (metis (no_types, lifting) \<open>0 \<notin> B\<close> image_iff norm_sgn sgn_div_norm)
immler@69675
  1631
  have 4: "independent ((\<lambda>x. x /\<^sub>R norm x) ` B)"
immler@69675
  1632
    by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one)
immler@69675
  1633
  have "inj_on (\<lambda>x. x /\<^sub>R norm x) B"
immler@69675
  1634
  proof
immler@69675
  1635
    fix x y
immler@69675
  1636
    assume "x \<in> B" "y \<in> B" "x /\<^sub>R norm x = y /\<^sub>R norm y"
immler@69675
  1637
    moreover have "\<And>i. i \<in> B \<Longrightarrow> norm (i /\<^sub>R norm i) = 1"
immler@69675
  1638
      using 3 by blast
immler@69675
  1639
    ultimately show "x = y"
immler@69675
  1640
      by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one)
immler@69675
  1641
  qed
immler@69675
  1642
  then have 5: "card ((\<lambda>x. x /\<^sub>R norm x) ` B) = dim S"
immler@69675
  1643
    by (metis \<open>card B = dim S\<close> card_image)
immler@69675
  1644
  have 6: "span ((\<lambda>x. x /\<^sub>R norm x) ` B) = S"
immler@69675
  1645
    by (metis "1" "4" "5" assms card_eq_dim independent_imp_finite span_subspace)
immler@69675
  1646
  show ?thesis
immler@69675
  1647
    by (rule that [OF 1 2 3 4 5 6])
immler@69675
  1648
qed
immler@69675
  1649
immler@69675
  1650
immler@69675
  1651
proposition%unimportant orthogonal_to_subspace_exists_gen:
immler@69675
  1652
  fixes S :: "'a :: euclidean_space set"
immler@69675
  1653
  assumes "span S \<subset> span T"
immler@69675
  1654
  obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
immler@69675
  1655
proof -
immler@69675
  1656
  obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
immler@69675
  1657
             and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
immler@69675
  1658
             and "independent B" "card B = dim S" "span B = span S"
immler@69675
  1659
    by (rule orthonormal_basis_subspace [of "span S", OF subspace_span])
immler@69675
  1660
      (auto simp: dim_span)
immler@69675
  1661
  with assms obtain u where spanBT: "span B \<subseteq> span T" and "u \<notin> span B" "u \<in> span T"
immler@69675
  1662
    by auto
immler@69675
  1663
  obtain C where orthBC: "pairwise orthogonal (B \<union> C)" and spanBC: "span (B \<union> C) = span (B \<union> {u})"
immler@69675
  1664
    by (blast intro: orthogonal_extension [OF orthB])
immler@69675
  1665
  show thesis
immler@69675
  1666
  proof (cases "C \<subseteq> insert 0 B")
immler@69675
  1667
    case True
immler@69675
  1668
    then have "C \<subseteq> span B"
immler@69675
  1669
      using span_eq
immler@69675
  1670
      by (metis span_insert_0 subset_trans)
immler@69675
  1671
    moreover have "u \<in> span (B \<union> C)"
immler@69675
  1672
      using \<open>span (B \<union> C) = span (B \<union> {u})\<close> span_superset by force
immler@69675
  1673
    ultimately show ?thesis
immler@69675
  1674
      using True \<open>u \<notin> span B\<close>
immler@69675
  1675
      by (metis Un_insert_left span_insert_0 sup.orderE)
immler@69675
  1676
  next
immler@69675
  1677
    case False
immler@69675
  1678
    then obtain x where "x \<in> C" "x \<noteq> 0" "x \<notin> B"
immler@69675
  1679
      by blast
immler@69675
  1680
    then have "x \<in> span T"
immler@69675
  1681
      by (metis (no_types, lifting) Un_insert_right Un_upper2 \<open>u \<in> span T\<close> spanBT spanBC
immler@69675
  1682
          \<open>u \<in> span T\<close> insert_subset span_superset span_mono
immler@69675
  1683
          span_span subsetCE subset_trans sup_bot.comm_neutral)
immler@69675
  1684
    moreover have "orthogonal x y" if "y \<in> span B" for y
immler@69675
  1685
      using that
immler@69675
  1686
    proof (rule span_induct)
immler@69675
  1687
      show "subspace {a. orthogonal x a}"
immler@69675
  1688
        by (simp add: subspace_orthogonal_to_vector)
immler@69675
  1689
      show "\<And>b. b \<in> B \<Longrightarrow> orthogonal x b"
immler@69675
  1690
        by (metis Un_iff \<open>x \<in> C\<close> \<open>x \<notin> B\<close> orthBC pairwise_def)
immler@69675
  1691
    qed
immler@69675
  1692
    ultimately show ?thesis
immler@69675
  1693
      using \<open>x \<noteq> 0\<close> that \<open>span B = span S\<close> by auto
immler@69675
  1694
  qed
immler@69675
  1695
qed
immler@69675
  1696
immler@69675
  1697
corollary%unimportant orthogonal_to_subspace_exists:
immler@69675
  1698
  fixes S :: "'a :: euclidean_space set"
immler@69675
  1699
  assumes "dim S < DIM('a)"
immler@69675
  1700
  obtains x where "x \<noteq> 0" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
immler@69675
  1701
proof -
immler@69675
  1702
have "span S \<subset> UNIV"
immler@69675
  1703
  by (metis (mono_tags) UNIV_I assms inner_eq_zero_iff less_le lowdim_subset_hyperplane
immler@69675
  1704
      mem_Collect_eq top.extremum_strict top.not_eq_extremum)
immler@69675
  1705
  with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis
immler@69675
  1706
    by (auto simp: span_UNIV)
immler@69675
  1707
qed
immler@69675
  1708
immler@69675
  1709
corollary%unimportant orthogonal_to_vector_exists:
immler@69675
  1710
  fixes x :: "'a :: euclidean_space"
immler@69675
  1711
  assumes "2 \<le> DIM('a)"
immler@69675
  1712
  obtains y where "y \<noteq> 0" "orthogonal x y"
immler@69675
  1713
proof -
immler@69675
  1714
  have "dim {x} < DIM('a)"
immler@69675
  1715
    using assms by auto
immler@69675
  1716
  then show thesis
immler@69675
  1717
    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
immler@69675
  1718
qed
immler@69675
  1719
immler@69675
  1720
proposition%unimportant orthogonal_subspace_decomp_exists:
immler@69675
  1721
  fixes S :: "'a :: euclidean_space set"
immler@69675
  1722
  obtains y z
immler@69675
  1723
  where "y \<in> span S"
immler@69675
  1724
    and "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w"
immler@69675
  1725
    and "x = y + z"
immler@69675
  1726
proof -
immler@69675
  1727
  obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T"
immler@69675
  1728
    "card T = dim (span S)" "span T = span S"
immler@69675
  1729
    using orthogonal_basis_subspace subspace_span by blast
immler@69675
  1730
  let ?a = "\<Sum>b\<in>T. (b \<bullet> x / (b \<bullet> b)) *\<^sub>R b"
immler@69675
  1731
  have orth: "orthogonal (x - ?a) w" if "w \<in> span S" for w
immler@69675
  1732
    by (simp add: Gram_Schmidt_step \<open>pairwise orthogonal T\<close> \<open>span T = span S\<close>
immler@69675
  1733
        orthogonal_commute that)
immler@69675
  1734
  show ?thesis
immler@69675
  1735
    apply (rule_tac y = "?a" and z = "x - ?a" in that)
immler@69675
  1736
      apply (meson \<open>T \<subseteq> span S\<close> span_scale span_sum subsetCE)
immler@69675
  1737
     apply (fact orth, simp)
immler@69675
  1738
    done
immler@69675
  1739
qed
immler@69675
  1740
immler@69675
  1741
lemma orthogonal_subspace_decomp_unique:
immler@69675
  1742
  fixes S :: "'a :: euclidean_space set"
immler@69675
  1743
  assumes "x + y = x' + y'"
immler@69675
  1744
      and ST: "x \<in> span S" "x' \<in> span S" "y \<in> span T" "y' \<in> span T"
immler@69675
  1745
      and orth: "\<And>a b. \<lbrakk>a \<in> S; b \<in> T\<rbrakk> \<Longrightarrow> orthogonal a b"
immler@69675
  1746
  shows "x = x' \<and> y = y'"
immler@69675
  1747
proof -
immler@69675
  1748
  have "x + y - y' = x'"
immler@69675
  1749
    by (simp add: assms)
immler@69675
  1750
  moreover have "\<And>a b. \<lbrakk>a \<in> span S; b \<in> span T\<rbrakk> \<Longrightarrow> orthogonal a b"
immler@69675
  1751
    by (meson orth orthogonal_commute orthogonal_to_span)
immler@69675
  1752
  ultimately have "0 = x' - x"
immler@69675
  1753
    by (metis (full_types) add_diff_cancel_left' ST diff_right_commute orthogonal_clauses(10) orthogonal_clauses(5) orthogonal_self)
immler@69675
  1754
  with assms show ?thesis by auto
immler@69675
  1755
qed
immler@69675
  1756
immler@69675
  1757
lemma vector_in_orthogonal_spanningset:
immler@69675
  1758
  fixes a :: "'a::euclidean_space"
immler@69675
  1759
  obtains S where "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
immler@69675
  1760
  by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def
immler@69675
  1761
      pairwise_orthogonal_insert span_UNIV subsetI subset_antisym)
immler@69675
  1762
immler@69675
  1763
lemma vector_in_orthogonal_basis:
immler@69675
  1764
  fixes a :: "'a::euclidean_space"
immler@69675
  1765
  assumes "a \<noteq> 0"
immler@69675
  1766
  obtains S where "a \<in> S" "0 \<notin> S" "pairwise orthogonal S" "independent S" "finite S"
immler@69675
  1767
                  "span S = UNIV" "card S = DIM('a)"
immler@69675
  1768
proof -
immler@69675
  1769
  obtain S where S: "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
immler@69675
  1770
    using vector_in_orthogonal_spanningset .
immler@69675
  1771
  show thesis
immler@69675
  1772
  proof
immler@69675
  1773
    show "pairwise orthogonal (S - {0})"
immler@69675
  1774
      using pairwise_mono S(2) by blast
immler@69675
  1775
    show "independent (S - {0})"
immler@69675
  1776
      by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent)
immler@69675
  1777
    show "finite (S - {0})"
immler@69675
  1778
      using \<open>independent (S - {0})\<close> independent_imp_finite by blast
immler@69675
  1779
    show "card (S - {0}) = DIM('a)"
immler@69675
  1780
      using span_delete_0 [of S] S
immler@69675
  1781
      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span dim_UNIV)
immler@69675
  1782
  qed (use S \<open>a \<noteq> 0\<close> in auto)
immler@69675
  1783
qed
immler@69675
  1784
immler@69675
  1785
lemma vector_in_orthonormal_basis:
immler@69675
  1786
  fixes a :: "'a::euclidean_space"
immler@69675
  1787
  assumes "norm a = 1"
immler@69675
  1788
  obtains S where "a \<in> S" "pairwise orthogonal S" "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
immler@69675
  1789
    "independent S" "card S = DIM('a)" "span S = UNIV"
immler@69675
  1790
proof -
immler@69675
  1791
  have "a \<noteq> 0"
immler@69675
  1792
    using assms by auto
immler@69675
  1793
  then obtain S where "a \<in> S" "0 \<notin> S" "finite S"
immler@69675
  1794
          and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)"
immler@69675
  1795
    by (metis vector_in_orthogonal_basis)
immler@69675
  1796
  let ?S = "(\<lambda>x. x /\<^sub>R norm x) ` S"
immler@69675
  1797
  show thesis
immler@69675
  1798
  proof
immler@69675
  1799
    show "a \<in> ?S"
immler@69675
  1800
      using \<open>a \<in> S\<close> assms image_iff by fastforce
immler@69675
  1801
  next
immler@69675
  1802
    show "pairwise orthogonal ?S"
immler@69675
  1803
      using \<open>pairwise orthogonal S\<close> by (auto simp: pairwise_def orthogonal_def)
immler@69675
  1804
    show "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` S \<Longrightarrow> norm x = 1"
immler@69675
  1805
      using \<open>0 \<notin> S\<close> by (auto simp: divide_simps)
immler@69675
  1806
    then show "independent ?S"
immler@69675
  1807
      by (metis \<open>pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` S)\<close> norm_zero pairwise_orthogonal_independent zero_neq_one)
immler@69675
  1808
    have "inj_on (\<lambda>x. x /\<^sub>R norm x) S"
immler@69675
  1809
      unfolding inj_on_def
immler@69675
  1810
      by (metis (full_types) S(1) \<open>0 \<notin> S\<close> inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def)
immler@69675
  1811
    then show "card ?S = DIM('a)"
immler@69675
  1812
      by (simp add: card_image S)
immler@69675
  1813
    show "span ?S = UNIV"
immler@69675
  1814
      by (metis (no_types) \<open>0 \<notin> S\<close> \<open>finite S\<close> \<open>span S = UNIV\<close>
immler@69675
  1815
          field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale
immler@69675
  1816
          zero_less_norm_iff)
immler@69675
  1817
  qed
immler@69675
  1818
qed
immler@69675
  1819
immler@69675
  1820
proposition dim_orthogonal_sum:
immler@69675
  1821
  fixes A :: "'a::euclidean_space set"
immler@69675
  1822
  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
immler@69675
  1823
    shows "dim(A \<union> B) = dim A + dim B"
immler@69675
  1824
proof -
immler@69675
  1825
  have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
immler@69675
  1826
    by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
immler@69675
  1827
  have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
immler@69675
  1828
    using 1 by (simp add: span_induct [OF _ subspace_hyperplane])
immler@69675
  1829
  then have 0: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
immler@69675
  1830
    by simp
immler@69675
  1831
  have "dim(A \<union> B) = dim (span (A \<union> B))"
immler@69675
  1832
    by (simp add: dim_span)
immler@69675
  1833
  also have "span (A \<union> B) = ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
immler@69675
  1834
    by (auto simp add: span_Un image_def)
immler@69675
  1835
  also have "dim \<dots> = dim {x + y |x y. x \<in> span A \<and> y \<in> span B}"
immler@69675
  1836
    by (auto intro!: arg_cong [where f=dim])
immler@69675
  1837
  also have "... = dim {x + y |x y. x \<in> span A \<and> y \<in> span B} + dim(span A \<inter> span B)"
immler@69675
  1838
    by (auto simp: dest: 0)
immler@69675
  1839
  also have "... = dim (span A) + dim (span B)"
immler@69675
  1840
    by (rule dim_sums_Int) (auto simp: subspace_span)
immler@69675
  1841
  also have "... = dim A + dim B"
immler@69675
  1842
    by (simp add: dim_span)
immler@69675
  1843
  finally show ?thesis .
immler@69675
  1844
qed
immler@69675
  1845
immler@69675
  1846
lemma dim_subspace_orthogonal_to_vectors:
immler@69675
  1847
  fixes A :: "'a::euclidean_space set"
immler@69675
  1848
  assumes "subspace A" "subspace B" "A \<subseteq> B"
immler@69675
  1849
    shows "dim {y \<in> B. \<forall>x \<in> A. orthogonal x y} + dim A = dim B"
immler@69675
  1850
proof -
immler@69675
  1851
  have "dim (span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)) = dim (span B)"
immler@69675
  1852
  proof (rule arg_cong [where f=dim, OF subset_antisym])
immler@69675
  1853
    show "span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A) \<subseteq> span B"
immler@69675
  1854
      by (simp add: \<open>A \<subseteq> B\<close> Collect_restrict span_mono)
immler@69675
  1855
  next
immler@69675
  1856
    have *: "x \<in> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
immler@69675
  1857
         if "x \<in> B" for x
immler@69675
  1858
    proof -
immler@69675
  1859
      obtain y z where "x = y + z" "y \<in> span A" and orth: "\<And>w. w \<in> span A \<Longrightarrow> orthogonal z w"
immler@69675
  1860
        using orthogonal_subspace_decomp_exists [of A x] that by auto
immler@69675
  1861
      have "y \<in> span B"
immler@69675
  1862
        using \<open>y \<in> span A\<close> assms(3) span_mono by blast
immler@69675
  1863
      then have "z \<in> {a \<in> B. \<forall>x. x \<in> A \<longrightarrow> orthogonal x a}"
immler@69675
  1864
        apply simp
immler@69675
  1865
        using \<open>x = y + z\<close> assms(1) assms(2) orth orthogonal_commute span_add_eq
immler@69675
  1866
          span_eq_iff that by blast
immler@69675
  1867
      then have z: "z \<in> span {y \<in> B. \<forall>x\<in>A. orthogonal x y}"
immler@69675
  1868
        by (meson span_superset subset_iff)
immler@69675
  1869
      then show ?thesis
immler@69675
  1870
        apply (auto simp: span_Un image_def  \<open>x = y + z\<close> \<open>y \<in> span A\<close>)
immler@69675
  1871
        using \<open>y \<in> span A\<close> add.commute by blast
immler@69675
  1872
    qed
immler@69675
  1873
    show "span B \<subseteq> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
immler@69675
  1874
      by (rule span_minimal)
immler@69675
  1875
        (auto intro: * span_minimal simp: subspace_span)
immler@69675
  1876
  qed
immler@69675
  1877
  then show ?thesis
immler@69675
  1878
    by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq
immler@69675
  1879
        orthogonal_commute orthogonal_def)
immler@69675
  1880
qed
immler@69675
  1881
immler@54776
  1882
end