Quelle Linear_Algebra.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Linear_Algebra.thy
    Author:     Amine Chaieb, University of Cambridge
*)

section \<open>Elementary Linear Algebra on Euclidean Spaces\<close>

theory Linear_Algebra
imports
  Euclidean_Space
  "HOL-Library.Infinite_Set"
begin

lemma linear_simps:
  assumes "bounded_linear f"
  shows
    "f (a + b) = f a + f b"
    "f (a - b) = f a - f b"
    "f 0 = 0"
    "f (- a) = - f a"
    "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
proof -
  interpret f: bounded_linear f by fact
  show "f (a + b) = f a + f b" by (rule f.add)
  show "f (a - b) = f a - f b" by (rule f.diff)
  show "f 0 = 0" by (rule f.zero)
  show "f (- a) = - f a" by (rule f.neg)
  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scale)
qed

lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x \ (UNIV::'a::finite set)}"
  using finite finite_image_set by blast

lemma substdbasis_expansion_unique:
  includes inner_syntax
  assumes d: "d \ Basis"
  shows "(\i\d. f i *\<^sub>R i) = (x::'a::euclidean_space) \
    (\<forall>i\<in>Basis. (i \<in> d \<longrightarrow> f i = x \<bullet> i) \<and> (i \<notin> d \<longrightarrow> x \<bullet> i = 0))"
proof -
  have *: "\x a b P. x * (if P then a else b) = (if P then x * a else x * b)"
    by auto
  have **: "finite d"
    by (auto intro: finite_subset[OF assms])
  have ***: "\i. i \ Basis \ (\i\d. f i *\<^sub>R i) \ i = (\x\d. if x = i then f x else 0)"
    using d
    by (auto intro!: sum.cong simp: inner_Basis inner_sum_left)
  show ?thesis
    unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***)
qed

lemma independent_substdbasis: "d \ Basis \ independent d"
  by (rule independent_mono[OF independent_Basis])

lemma subset_translation_eq [simp]:
    fixes a :: "'a::real_vector" shows "(+) a ` s \ (+) a ` t \ s \ t"
  by auto

lemma translate_inj_on:
  fixes A :: "'a::ab_group_add set"
  shows "inj_on (\x. a + x) A"
  unfolding inj_on_def by auto

lemma translation_assoc:
  fixes a b :: "'a::ab_group_add"
  shows "(\x. b + x) ` ((\x. a + x) ` S) = (\x. (a + b) + x) ` S"
  by auto

lemma translation_invert:
  fixes a :: "'a::ab_group_add"
  assumes "(\x. a + x) ` A = (\x. a + x) ` B"
  shows "A = B"
  using assms translation_assoc by fastforce

lemma translation_galois:
  fixes a :: "'a::ab_group_add"
  shows "T = ((\x. a + x) ` S) \ S = ((\x. (- a) + x) ` T)"
  by (metis add.right_inverse group_cancel.rule0 translation_invert translation_assoc)

lemma translation_inverse_subset:
  assumes "((\x. - a + x) ` V) \ (S :: 'n::ab_group_add set)"
  shows "V \ ((\x. a + x) ` S)"
  by (metis assms subset_image_iff translation_galois)

subsection\<^marker>\<open>tag unimportant\<close> \<open>More interesting properties of the norm\<close>

unbundle inner_syntax

text\<open>Equality of vectors in terms of \<^term>\<open>(\<bullet>)\<close> products.\<close>

lemma linear_componentwise:
  fixes f:: "'a::euclidean_space \ 'b::real_inner"
  assumes lf: "linear f"
  shows "(f x) \ j = (\i\Basis. (x\i) * (f i\j))" (is "?lhs = ?rhs")
proof -
  interpret linear f by fact
  have "?rhs = (\i\Basis. (x\i) *\<^sub>R (f i))\j"
    by (simp add: inner_sum_left)
  then show ?thesis
    by (simp add: euclidean_representation sum[symmetric] scale[symmetric])
qed

lemma vector_eq: "x = y \ x \ x = x \ y \ y \ y = x \ x"
  by (metis (no_types, opaque_lifting) inner_commute inner_diff_right inner_eq_zero_iff right_minus_eq)

lemma norm_triangle_half_r:
  "norm (y - x1) < e/2 \ norm (y - x2) < e/2 \ norm (x1 - x2) < e"
  using dist_triangle_half_r unfolding dist_norm[symmetric] by auto

lemma norm_triangle_half_l:
  assumes "norm (x - y) < e/2" and "norm (x' - y) < e/2"
  shows "norm (x - x') < e"
  by (metis assms dist_norm dist_triangle_half_l)

lemma abs_triangle_half_r:
  fixes y :: "'a::linordered_field"
  shows "abs (y - x1) < e/2 \ abs (y - x2) < e/2 \ abs (x1 - x2) < e"
  by linarith

lemma abs_triangle_half_l:
  fixes y :: "'a::linordered_field"
  assumes "abs (x - y) < e/2" and "abs (x' - y) < e/2"
  shows "abs (x - x') < e"
  using assms by linarith

lemma sum_clauses:
  shows "sum f {} = 0"
    and "finite S \ sum f (insert x S) = (if x \ S then sum f S else f x + sum f S)"
  by (auto simp add: insert_absorb)

lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = z" and vector_eq_rdot: "(\z. x \ z = y \ z) \ x = y"
  by (metis inner_commute vector_eq)+

subsection \<open>Substandard Basis\<close>

lemma ex_card:
  assumes "n \ card A"
  shows "\S\A. card S = n"
  by (meson assms obtain_subset_with_card_n)

lemma subspace_substandard: "subspace {x::'a::euclidean_space. (\i\Basis. P i \ x\i = 0)}"
  by (auto simp: subspace_def inner_add_left)

lemma dim_substandard:
  assumes d: "d \ Basis"
  shows "dim {x::'a::euclidean_space. \i\Basis. i \ d \ x\i = 0} = card d" (is "dim ?A = _")
proof (rule dim_unique)
  from d show "d \ ?A"
    by (auto simp: inner_Basis)
  from d show "independent d"
    by (rule independent_mono [OF independent_Basis])
  have "x \ span d" if "\i\Basis. i \ d \ x \ i = 0" for x
  proof -
    have "finite d"
      by (rule finite_subset [OF d finite_Basis])
    then have "(\i\d. (x \ i) *\<^sub>R i) \ span d"
      by (simp add: span_sum span_clauses)
    also have "(\i\d. (x \ i) *\<^sub>R i) = (\i\Basis. (x \ i) *\<^sub>R i)"
      by (rule sum.mono_neutral_cong_left [OF finite_Basis d]) (auto simp: that)
    finally show "x \ span d"
      by (simp only: euclidean_representation)
  qed
  then show "?A \ span d" by auto
qed simp

subsection \<open>Orthogonality\<close>

definition\<^marker>\<open>tag important\<close> (in real_inner) "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"

context real_inner
begin

lemma orthogonal_self: "orthogonal x x \ x = 0"
  by (simp add: orthogonal_def)

lemma orthogonal_clauses:
  "orthogonal a 0"
  "orthogonal a x \ orthogonal a (c *\<^sub>R x)"
  "orthogonal a x \ orthogonal a (- x)"
  "orthogonal a x \ orthogonal a y \ orthogonal a (x + y)"
  "orthogonal a x \ orthogonal a y \ orthogonal a (x - y)"
  "orthogonal 0 a"
  "orthogonal x a \ orthogonal (c *\<^sub>R x) a"
  "orthogonal x a \ orthogonal (- x) a"
  "orthogonal x a \ orthogonal y a \ orthogonal (x + y) a"
  "orthogonal x a \ orthogonal y a \ orthogonal (x - y) a"
  unfolding orthogonal_def inner_add inner_diff by auto

end

lemma orthogonal_commute: "orthogonal x y \ orthogonal y x"
  by (simp add: orthogonal_def inner_commute)

lemma orthogonal_scaleR [simp]: "c \ 0 \ orthogonal (c *\<^sub>R x) = orthogonal x"
  by (rule ext) (simp add: orthogonal_def)

lemma pairwise_ortho_scaleR:
    "pairwise (\i j. orthogonal (f i) (g j)) B
    \<Longrightarrow> pairwise (\<lambda>i j. orthogonal (a i *\<^sub>R f i) (a j *\<^sub>R g j)) B"
  by (auto simp: pairwise_def orthogonal_clauses)

lemma orthogonal_rvsum:
    "\finite s; \y. y \ s \ orthogonal x (f y)\ \ orthogonal x (sum f s)"
  by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)

lemma orthogonal_lvsum:
    "\finite s; \x. x \ s \ orthogonal (f x) y\ \ orthogonal (sum f s) y"
  by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)

lemma norm_add_Pythagorean:
  assumes "orthogonal a b"
    shows "(norm (a + b))\<^sup>2 = (norm a)\<^sup>2 + (norm b)\<^sup>2"
proof -
  from assms have "(a - (0 - b)) \ (a - (0 - b)) = a \ a - (0 - b \ b)"
    by (simp add: algebra_simps orthogonal_def inner_commute)
  then show ?thesis
    by (simp add: power2_norm_eq_inner)
qed

lemma norm_sum_Pythagorean:
  assumes "finite I" "pairwise (\i j. orthogonal (f i) (f j)) I"
    shows "(norm (sum f I))\<^sup>2 = (\i\I. (norm (f i))\<^sup>2)"
using assms
proof (induction I rule: finite_induct)
  case empty then show ?case by simp
next
  case (insert x I)
  then have "orthogonal (f x) (sum f I)"
    by (metis pairwise_insert orthogonal_rvsum)
  with insert show ?case
    by (simp add: pairwise_insert norm_add_Pythagorean)
qed

subsection  \<open>Orthogonality of a transformation\<close>

definition\<^marker>\<open>tag important\<close>  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation:
  "orthogonal_transformation f \ linear f \ (\v. norm (f v) = norm v)"
  by (smt (verit, ccfv_threshold) dot_norm linear_add norm_eq_sqrt_inner orthogonal_transformation_def)

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
  by (simp add: linear_iff orthogonal_transformation_def)

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_orthogonal_transformation:
    "orthogonal_transformation f \ orthogonal (f x) (f y) \ orthogonal x y"
  by (simp add: orthogonal_def orthogonal_transformation_def)

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_compose:
   "\orthogonal_transformation f; orthogonal_transformation g\ \ orthogonal_transformation(f \ g)"
  by (auto simp: orthogonal_transformation_def linear_compose)

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_neg:
  "orthogonal_transformation(\x. -(f x)) \ orthogonal_transformation f"
  by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v"
  by (simp add: linear_iff orthogonal_transformation_def)

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_linear:
   "orthogonal_transformation f \ linear f"
  by (simp add: orthogonal_transformation_def)

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_inj:
  "orthogonal_transformation f \ inj f"
  unfolding orthogonal_transformation_def inj_on_def
  by (metis vector_eq)

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_surj:
  "orthogonal_transformation f \ surj f"
  for f :: "'a::euclidean_space \ 'a::euclidean_space"
  by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_bij:
  "orthogonal_transformation f \ bij f"
  for f :: "'a::euclidean_space \ 'a::euclidean_space"
  by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_inv:
  "orthogonal_transformation f \ orthogonal_transformation (inv f)"
  for f :: "'a::euclidean_space \ 'a::euclidean_space"
  by (metis (no_types, opaque_lifting) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)

lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_norm:
  "orthogonal_transformation f \ norm (f x) = norm x"
  by (metis orthogonal_transformation)

subsection \<open>Bilinear functions\<close>

definition\<^marker>\<open>tag important\<close>
bilinear :: "('a::real_vector \ 'b::real_vector \ 'c::real_vector) \ bool" where
"bilinear f \ (\x. linear (\y. f x y)) \ (\y. linear (\x. f x y))"

lemma bilinear_ladd: "bilinear h \ h (x + y) z = h x z + h y z"
  by (simp add: bilinear_def linear_iff)

lemma bilinear_radd: "bilinear h \ h x (y + z) = h x y + h x z"
  by (simp add: bilinear_def linear_iff)

lemma bilinear_times:
  fixes c::"'a::real_algebra" shows "bilinear (\x y::'a. x*y)"
  by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI)

lemma bilinear_lmul: "bilinear h \ h (c *\<^sub>R x) y = c *\<^sub>R h x y"
  by (simp add: bilinear_def linear_iff)

lemma bilinear_rmul: "bilinear h \ h x (c *\<^sub>R y) = c *\<^sub>R h x y"
  by (simp add: bilinear_def linear_iff)

lemma bilinear_lneg: "bilinear h \ h (- x) y = - h x y"
  by (drule bilinear_lmul [of _ "- 1"]) simp

lemma bilinear_rneg: "bilinear h \ h x (- y) = - h x y"
  by (drule bilinear_rmul [of _ _ "- 1"]) simp

lemma (in ab_group_add) eq_add_iff: "x = x + y \ y = 0"
  using add_left_imp_eq[of x y 0] by auto

lemma bilinear_lzero:
  assumes "bilinear h"
  shows "h 0 x = 0"
  using bilinear_ladd [OF assms, of 0 0 x] by (simp add: eq_add_iff field_simps)

lemma bilinear_rzero:
  assumes "bilinear h"
  shows "h x 0 = 0"
  using bilinear_radd [OF assms, of x 0 0 ] by (simp add: eq_add_iff field_simps)

lemma bilinear_lsub: "bilinear h \ h (x - y) z = h x z - h y z"
  using bilinear_ladd [of h x "- y"] by (simp add: bilinear_lneg)

lemma bilinear_rsub: "bilinear h \ h z (x - y) = h z x - h z y"
  using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg)

lemma bilinear_sum:
  assumes "bilinear h"
  shows "h (sum f S) (sum g T) = sum (\(i,j). h (f i) (g j)) (S \ T) "
proof -
  interpret l: linear "\x. h x y" for y using assms by (simp add: bilinear_def)
  interpret r: linear "\y. h x y" for x using assms by (simp add: bilinear_def)
  have "h (sum f S) (sum g T) = sum (\x. h (f x) (sum g T)) S"
    by (simp add: l.sum)
  also have "\ = sum (\x. sum (\y. h (f x) (g y)) T) S"
    by (rule sum.cong) (simp_all add: r.sum)
  finally show ?thesis
    unfolding sum.cartesian_product .
qed

subsection \<open>Adjoints\<close>

definition\<^marker>\<open>tag important\<close> adjoint :: "(('a::real_inner) \<Rightarrow> ('b::real_inner)) \<Rightarrow> 'b \<Rightarrow> 'a" where
"adjoint f = (SOME f'. \x y. f x \ y = x \ f' y)"

lemma adjoint_unique:
  assumes "\x y. inner (f x) y = inner x (g y)"
  shows "adjoint f = g"
  unfolding adjoint_def
proof (rule some_equality)
  show "\x y. inner (f x) y = inner x (g y)"
    by (rule assms)
next
  fix h
  assume "\x y. inner (f x) y = inner x (h y)"
  then show "h = g"
    by (metis assms ext vector_eq_ldot)
qed

text \<open>TODO: The following lemmas about adjoints should hold for any
  Hilbert space (i.e. complete inner product space).
  (see \<^url>\<open>https://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
\<close>

lemma adjoint_works:
  fixes f :: "'n::euclidean_space \ 'm::euclidean_space"
  assumes lf: "linear f"
  shows "x \ adjoint f y = f x \ y"
proof -
  interpret linear f by fact
  have "\y. \w. \x. f x \ y = x \ w"
  proof (intro allI exI)
    fix y :: "'m" and x
    let ?w = "(\i\Basis. (f i \ y) *\<^sub>R i) :: 'n"
    have "f x \ y = f (\i\Basis. (x \ i) *\<^sub>R i) \ y"
      by (simp add: euclidean_representation)
    also have "\ = (\i\Basis. (x \ i) *\<^sub>R f i) \ y"
      by (simp add: sum scale)
    finally show "f x \ y = x \ ?w"
      by (simp add: inner_sum_left inner_sum_right mult.commute)
  qed
  then show ?thesis
    unfolding adjoint_def choice_iff
    by (intro someI2_ex[where Q="\f'. x \ f' y = f x \ y"]) auto
qed

lemma adjoint_clauses:
  fixes f :: "'n::euclidean_space \ 'm::euclidean_space"
  assumes lf: "linear f"
  shows "x \ adjoint f y = f x \ y"
    and "adjoint f y \ x = y \ f x"
  by (simp_all add: adjoint_works[OF lf] inner_commute)

lemma adjoint_linear:
  fixes f :: "'n::euclidean_space \ 'm::euclidean_space"
  assumes lf: "linear f"
  shows "linear (adjoint f)"
  by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]
    adjoint_clauses[OF lf] inner_distrib)

lemma adjoint_adjoint:
  fixes f :: "'n::euclidean_space \ 'm::euclidean_space"
  assumes lf: "linear f"
  shows "adjoint (adjoint f) = f"
  by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])

subsection\<^marker>\<open>tag unimportant\<close> \<open>Euclidean Spaces as Typeclass\<close>

lemma independent_Basis: "independent Basis"
  by (rule independent_Basis)

lemma span_Basis [simp]: "span Basis = UNIV"
  by (rule span_Basis)

lemma in_span_Basis: "x \ span Basis"
  unfolding span_Basis ..

lemma representation_euclidean_space:
  "representation Basis x = (\b. if b \ Basis then inner x b else 0)"
proof (rule representation_eqI)
  have "(\b | (if b \ Basis then inner x b else 0) \ 0. (if b \ Basis then inner x b else 0) *\<^sub>R b) =
          (\<Sum>b\<in>Basis. inner x b *\<^sub>R b)"
    by (intro sum.mono_neutral_cong_left) auto
  also have "\ = x"
    by (simp add: euclidean_representation)
  finally show "(\b | (if b \ Basis then inner x b else 0) \ 0.
                  (if b \<in> Basis then inner x b else 0) *\<^sub>R b) = x" .
qed (insert independent_Basis span_Basis, auto split: if_splits)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Linearity and Bilinearity continued\<close>

lemma linear_bounded:
  fixes f :: "'a::euclidean_space \ 'b::real_normed_vector"
  assumes lf: "linear f"
  shows "\B. \x. norm (f x) \ B * norm x"
proof
  interpret linear f by fact
  let ?B = "\b\Basis. norm (f b)"
  show "\x. norm (f x) \ ?B * norm x"
  proof
    fix x :: 'a
    let ?g = "\b. (x \ b) *\<^sub>R f b"
    have "norm (f x) = norm (f (\b\Basis. (x \ b) *\<^sub>R b))"
      unfolding euclidean_representation ..
    also have "\ = norm (sum ?g Basis)"
      by (simp add: sum scale)
    finally have th0: "norm (f x) = norm (sum ?g Basis)" .
    have th: "norm (?g i) \ norm (f i) * norm x" if "i \ Basis" for i
    proof -
      from Basis_le_norm[OF that, of x]
      show "norm (?g i) \ norm (f i) * norm x"
        unfolding norm_scaleR by (metis mult.commute mult_left_mono norm_ge_zero)
    qed
    from sum_norm_le[of _ ?g, OF th]
    show "norm (f x) \ ?B * norm x"
      by (simp add: sum_distrib_right th0)
  qed
qed

lemma linear_conv_bounded_linear:
  fixes f :: "'a::euclidean_space \ 'b::real_normed_vector"
  shows "linear f \ bounded_linear f"
  by (metis mult.commute bounded_linear_axioms.intro bounded_linear_def linear_bounded)

lemmas linear_linear = linear_conv_bounded_linear[symmetric]

lemma inj_linear_imp_inv_bounded_linear:
  fixes f::"'a::euclidean_space \ 'a"
  shows "\bounded_linear f; inj f\ \ bounded_linear (inv f)"
  by (simp add: inj_linear_imp_inv_linear linear_linear)

lemma linear_bounded_pos:
  fixes f :: "'a::euclidean_space \ 'b::real_normed_vector"
  assumes lf: "linear f"
obtains B where "B > 0" "\x. norm (f x) \ B * norm x"
  by (metis bounded_linear.pos_bounded lf linear_linear mult.commute)

lemma linear_invertible_bounded_below_pos:
  fixes f :: "'a::real_normed_vector \ 'b::euclidean_space"
  assumes "linear f" "linear g" and gf: "g \ f = id"
  obtains B where "B > 0" "\x. B * norm x \ norm(f x)"
proof -
  obtain B where "B > 0" and B: "\x. norm (g x) \ B * norm x"
    using linear_bounded_pos [OF \<open>linear g\<close>] by blast
  show thesis
  proof
    show "0 < 1/B"
      by (simp add: \<open>B > 0\<close>)
    show "1/B * norm x \ norm (f x)" for x
      by (smt (verit, ccfv_SIG) B \<open>0 < B\<close> gf comp_apply divide_inverse id_apply inverse_eq_divide
              less_divide_eq mult.commute)
  qed
qed

lemma linear_inj_bounded_below_pos:
  fixes f :: "'a::real_normed_vector \ 'b::euclidean_space"
  assumes "linear f" "inj f"
  obtains B where "B > 0" "\x. B * norm x \ norm(f x)"
  using linear_injective_left_inverse [OF assms]
    linear_invertible_bounded_below_pos assms by blast

lemma bounded_linearI':
  fixes f ::"'a::euclidean_space \ 'b::real_normed_vector"
  assumes "\x y. f (x + y) = f x + f y"
    and "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
  shows "bounded_linear f"
  using assms linearI linear_conv_bounded_linear by blast

lemma bilinear_bounded:
  fixes h :: "'m::euclidean_space \ 'n::euclidean_space \ 'k::real_normed_vector"
  assumes bh: "bilinear h"
  shows "\B. \x y. norm (h x y) \ B * norm x * norm y"
proof (clarify intro!: exI[of _ "\i\Basis. \j\Basis. norm (h i j)"])
  fix x :: 'm
  fix y :: 'n
  have "norm (h x y) = norm (h (sum (\i. (x \ i) *\<^sub>R i) Basis) (sum (\i. (y \ i) *\<^sub>R i) Basis))"
    by (simp add: euclidean_representation)
  also have "\ = norm (sum (\ (i,j). h ((x \ i) *\<^sub>R i) ((y \ j) *\<^sub>R j)) (Basis \ Basis))"
    unfolding bilinear_sum[OF bh] ..
  finally have th: "norm (h x y) = \" .
  have "\i j. \i \ Basis; j \ Basis\
           \<Longrightarrow> \<bar>x \<bullet> i\<bar> * (\<bar>y \<bullet> j\<bar> * norm (h i j)) \<le> norm x * (norm y * norm (h i j))"
    by (auto simp add: zero_le_mult_iff Basis_le_norm mult_mono)
  then show "norm (h x y) \ (\i\Basis. \j\Basis. norm (h i j)) * norm x * norm y"
    unfolding sum_distrib_right th sum.cartesian_product
    by (clarsimp simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
      field_simps simp del: scaleR_scaleR intro!: sum_norm_le)
qed

lemma bilinear_conv_bounded_bilinear:
  fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector"
  shows "bilinear h \ bounded_bilinear h"
proof
  assume "bilinear h"
  show "bounded_bilinear h"
  proof
    fix x y z
    show "h (x + y) z = h x z + h y z"
      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff by simp
  next
    fix x y z
    show "h x (y + z) = h x y + h x z"
      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff by simp
  next
    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
      using \<open>bilinear h\<close> unfolding bilinear_def linear_iff
      by simp_all
  next
    have "\B. \x y. norm (h x y) \ B * norm x * norm y"
      using \<open>bilinear h\<close> by (rule bilinear_bounded)
    then show "\K. \x y. norm (h x y) \ norm x * norm y * K"
      by (simp add: ac_simps)
  qed
next
  assume "bounded_bilinear h"
  then interpret h: bounded_bilinear h .
  show "bilinear h"
    unfolding bilinear_def linear_conv_bounded_linear
    using h.bounded_linear_left h.bounded_linear_right by simp
qed

lemma bilinear_bounded_pos:
  fixes h :: "'a::euclidean_space \ 'b::euclidean_space \ 'c::real_normed_vector"
  assumes bh: "bilinear h"
  shows "\B > 0. \x y. norm (h x y) \ B * norm x * norm y"
  by (metis mult.assoc bh bilinear_conv_bounded_bilinear bounded_bilinear.pos_bounded mult.commute)

lemma bounded_linear_imp_has_derivative:
  "bounded_linear f \ (f has_derivative f) net"
  by (auto simp add: has_derivative_def linear_diff linear_linear linear_def
      dest: bounded_linear.linear)

lemma linear_imp_has_derivative:
  fixes f :: "'a::euclidean_space \ 'b::real_normed_vector"
  shows "linear f \ (f has_derivative f) net"
  by (simp add: bounded_linear_imp_has_derivative linear_conv_bounded_linear)

lemma bounded_linear_imp_differentiable: "bounded_linear f \ f differentiable net"
  using bounded_linear_imp_has_derivative differentiable_def by blast

lemma linear_imp_differentiable:
  fixes f :: "'a::euclidean_space \ 'b::real_normed_vector"
  shows "linear f \ f differentiable net"
  by (metis linear_imp_has_derivative differentiable_def)

lemma of_real_differentiable [simp,derivative_intros]: "of_real differentiable F"
  by (simp add: bounded_linear_imp_differentiable bounded_linear_of_real)

lemma bounded_linear_representation:
  fixes B :: "'a :: euclidean_space set"
  assumes "independent B" "span B = UNIV"
  shows   "bounded_linear (\v. representation B v b)"
proof -
  have "Vector_Spaces.linear (*\<^sub>R) (*) (\v. representation B v b)"
    by (rule real_vector.linear_representation) fact+
  then have "linear (\v. representation B v b)"
    unfolding linear_def real_scaleR_def [abs_def] .
  thus ?thesis
    by (simp add: linear_conv_bounded_linear)
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>We continue\<close>

lemma independent_bound:
  fixes S :: "'a::euclidean_space set"
  shows "independent S \ finite S \ card S \ DIM('a)"
  by (metis dim_subset_UNIV finiteI_independent dim_span_eq_card_independent)

lemmas independent_imp_finite = finiteI_independent

corollary\<^marker>\<open>tag unimportant\<close> independent_card_le:
  fixes S :: "'a::euclidean_space set"
  assumes "independent S"
  shows "card S \ DIM('a)"
  using assms independent_bound by auto

lemma dependent_biggerset:
  fixes S :: "'a::euclidean_space set"
  shows "(finite S \ card S > DIM('a)) \ dependent S"
  by (metis independent_bound not_less)

text \<open>Picking an orthogonal replacement for a spanning set.\<close>

lemma vector_sub_project_orthogonal:
  fixes b x :: "'a::euclidean_space"
  shows "b \ (x - ((b \ x) / (b \ b)) *\<^sub>R b) = 0"
  unfolding inner_simps by auto

lemma pairwise_orthogonal_insert:
  assumes "pairwise orthogonal S"
    and "\y. y \ S \ orthogonal x y"
  shows "pairwise orthogonal (insert x S)"
  using assms by (auto simp: pairwise_def orthogonal_commute)

lemma basis_orthogonal:
  fixes B :: "'a::real_inner set"
  assumes fB: "finite B"
  shows "\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C"
  (is " \C. ?P B C")
  using fB
proof (induct rule: finite_induct)
  case empty
  then show ?case
    using pairwise_empty by blast
next
  case (insert a B)
  note fB = \<open>finite B\<close> and aB = \<open>a \<notin> B\<close>
  from \<open>\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C\<close>
  obtain C where C: "finite C" "card C \ card B"
    "span C = span B" "pairwise orthogonal C" by blast
  let ?a = "a - sum (\x. (x \ a / (x \ x)) *\<^sub>R x) C"
  let ?C = "insert ?a C"
  from C(1) have fC: "finite ?C"
    by simp
  have cC: "card ?C \ card (insert a B)"
    using C aB card_insert_if local.insert(1) by fastforce
  {
    fix x k
    have th0: "\(a::'a) b c. a - (b - c) = c + (a - b)"
      by (simp add: field_simps)
    have "x - k *\<^sub>R (a - (\x\C. (x \ a / (x \ x)) *\<^sub>R x)) \ span C \ x - k *\<^sub>R a \ span C"
      unfolding scaleR_right_diff_distrib th0
      by (intro span_add_eq span_scale span_sum span_base)
  }
  then have SC: "span ?C = span (insert a B)"
    unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto
  {
    fix y
    assume yC: "y \ C"
    then have Cy: "C = insert y (C - {y})"
      by blast
    have fth: "finite (C - {y})"
      using C by simp
    have "y \ 0 \ \x\C - {y}. x \ a * (x \ y) / (x \ x) = 0"
      using \<open>pairwise orthogonal C\<close>
      by (metis Cy DiffE div_0 insertCI mult_zero_right orthogonal_def pairwise_insert)
    then have "orthogonal ?a y"
      unfolding orthogonal_def
      unfolding inner_diff inner_sum_left right_minus_eq
      unfolding sum.remove [OF \<open>finite C\<close> \<open>y \<in> C\<close>]
      by (auto simp add: sum.neutral inner_commute[of y a])
  }
  with \<open>pairwise orthogonal C\<close> have CPO: "pairwise orthogonal ?C"
    by (rule pairwise_orthogonal_insert)
  from fC cC SC CPO have "?P (insert a B) ?C"
    by blast
  then show ?case by blast
qed

lemma orthogonal_basis_exists:
  fixes V :: "('a::euclidean_space) set"
  shows "\B. independent B \ B \ span V \ V \ span B \ (card B = dim V) \ pairwise orthogonal B"
proof -
  from basis_exists[of V] obtain B where
    B: "B \ V" "independent B" "V \ span B" "card B = dim V"
    by force
  from B have fB: "finite B" "card B = dim V"
    using independent_bound by auto
  from basis_orthogonal[OF fB(1)] obtain C where
    C: "finite C" "card C \ card B" "span C = span B" "pairwise orthogonal C"
    by blast
  from C B have CSV: "C \ span V"
    by (metis span_superset span_mono subset_trans)
  from span_mono[OF B(3)] C have SVC: "span V \ span C"
    by (simp add: span_span)
  from C fB have "card C \ dim V"
    by simp
  moreover have "dim V \ card C"
    using span_card_ge_dim[OF CSV SVC C(1)]
    by simp
  ultimately have "card C = dim V"
    using C(1) by simp
  with C B CSV show ?thesis
    by (metis SVC card_eq_dim dim_span)
qed

text \<open>Low-dimensional subset is in a hyperplane (weak orthogonal complement).\<close>

lemma span_not_UNIV_orthogonal:
  fixes S :: "'a::euclidean_space set"
  assumes sU: "span S \ UNIV"
  shows "\a::'a. a \ 0 \ (\x \ span S. a \ x = 0)"
proof -
  from sU obtain a where a: "a \ span S"
    by blast
  from orthogonal_basis_exists obtain B where
    B: "independent B" "B \ span S" "S \ span B" "card B = dim S" "pairwise orthogonal B"
    by blast
  from B have fB: "finite B" "card B = dim S"
    using independent_bound by auto
  have sSB: "span S = span B"
    by (simp add: B span_eq)
  let ?a = "a - sum (\b. (a \ b / (b \ b)) *\<^sub>R b) B"
  have "sum (\b. (a \ b / (b \ b)) *\<^sub>R b) B \ span S"
    by (simp add: sSB span_base span_mul span_sum)
  with a have a0:"?a \ 0"
    by auto
  have "?a \ x = 0" if "x\span B" for x
  proof (rule span_induct [OF that])
    show "subspace {x. ?a \ x = 0}"
      by (auto simp add: subspace_def inner_add)
  next
    {
      fix x
      assume x: "x \ B"
      from x have B': "B = insert x (B - {x})"
        by blast
      have fth: "finite (B - {x})"
        using fB by simp
      have "(\b\B - {x}. a \ b * (b \ x) / (b \ b)) = 0" if "x \ 0"
        by (smt (verit) B' B(5) DiffD2 divide_eq_0_iff inner_real_def inner_zero_right insertCI orthogonal_def pairwise_insert sum.neutral)
      then have "?a \ x = 0"
        apply (subst B')
        using fB fth
        unfolding sum_clauses(2)[OF fth]
        by (auto simp add: inner_add_left inner_diff_left inner_sum_left)
    }
    then show "?a \ x = 0" if "x \ B" for x
      using that by blast
    qed
  with a0 sSB show ?thesis
    by blast
qed

lemma span_not_univ_subset_hyperplane:
  fixes S :: "'a::euclidean_space set"
  assumes SU: "span S \ UNIV"
  shows "\ a. a \0 \ span S \ {x. a \ x = 0}"
  using span_not_UNIV_orthogonal[OF SU] by auto

lemma lowdim_subset_hyperplane:
  fixes S :: "'a::euclidean_space set"
  assumes d: "dim S < DIM('a)"
  shows "\a::'a. a \ 0 \ span S \ {x. a \ x = 0}"
  using d dim_eq_full nless_le span_not_univ_subset_hyperplane by blast

lemma linear_eq_stdbasis:
  fixes f :: "'a::euclidean_space \ _"
  assumes lf: "linear f"
    and lg: "linear g"
    and fg: "\b. b \ Basis \ f b = g b"
  shows "f = g"
  using linear_eq_on_span[OF lf lg, of Basis] fg by auto

text \<open>Similar results for bilinear functions.\<close>

lemma bilinear_eq:
  assumes bf: "bilinear f"
    and bg: "bilinear g"
    and SB: "S \ span B"
    and TC: "T \ span C"
    and "x\S" "y\T"
    and fg: "\x y. \x \ B; y\ C\ \ f x y = g x y"
  shows "f x y = g x y"
proof -
  let ?P = "{x. \y\ span C. f x y = g x y}"
  from bf bg have sp: "subspace ?P"
    unfolding bilinear_def linear_iff subspace_def bf bg
    by (auto simp add: span_zero bilinear_lzero[OF bf] bilinear_lzero[OF bg]
        span_add Ball_def
      intro: bilinear_ladd[OF bf])
  have sfg: "\x. x \ B \ subspace {a. f x a = g x a}"
    by (auto simp: subspace_def bf bg bilinear_rzero bilinear_radd bilinear_rmul)
  have "\y\ span C. f x y = g x y" if "x \ span B" for x
    using span_induct [OF that sp] fg sfg span_induct by blast
  then show ?thesis
    using SB TC assms by auto
qed

lemma bilinear_eq_stdbasis:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space \ _"
  assumes bf: "bilinear f"
    and bg: "bilinear g"
    and fg: "\i j. i \ Basis \ j \ Basis \ f i j = g i j"
  shows "f = g"
  using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg by blast

subsection \<open>Infinity norm\<close>

definition\<^marker>\<open>tag important\<close> "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"

lemma infnorm_set_image:
  fixes x :: "'a::euclidean_space"
  shows "{\x \ i\ |i. i \ Basis} = (\i. \x \ i\) ` Basis"
  by blast

lemma infnorm_Max:
  fixes x :: "'a::euclidean_space"
  shows "infnorm x = Max ((\i. \x \ i\) ` Basis)"
  by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)

lemma infnorm_set_lemma:
  fixes x :: "'a::euclidean_space"
  shows "finite {\x \ i\ |i. i \ Basis}"
    and "{\x \ i\ |i. i \ Basis} \ {}"
  unfolding infnorm_set_image by auto

lemma infnorm_pos_le:
  fixes x :: "'a::euclidean_space"
  shows "0 \ infnorm x"
  by (simp add: infnorm_Max Max_ge_iff ex_in_conv)

lemma infnorm_triangle:
  fixes x :: "'a::euclidean_space"
  shows "infnorm (x + y) \ infnorm x + infnorm y"
proof -
  have *: "\a b c d :: real. \a\ \ c \ \b\ \ d \ \a + b\ \ c + d"
    by simp
  show ?thesis
    by (auto simp: infnorm_Max inner_add_left intro!: *)
qed

lemma infnorm_eq_0:
  fixes x :: "'a::euclidean_space"
  shows "infnorm x = 0 \ x = 0"
proof -
  have "infnorm x \ 0 \ x = 0"
    unfolding infnorm_Max by (simp add: euclidean_all_zero_iff)
  then show ?thesis
    using infnorm_pos_le[of x] by simp
qed

lemma infnorm_0: "infnorm 0 = 0"
  by (simp add: infnorm_eq_0)

lemma infnorm_neg: "infnorm (- x) = infnorm x"
  unfolding infnorm_def by simp

lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
  by (metis infnorm_neg minus_diff_eq)

lemma absdiff_infnorm: "\infnorm x - infnorm y\ \ infnorm (x - y)"
  by (smt (verit, del_insts) diff_add_cancel infnorm_sub infnorm_triangle)

lemma real_abs_infnorm: "\infnorm x\ = infnorm x"
  using infnorm_pos_le[of x] by arith

lemma Basis_le_infnorm:
  fixes x :: "'a::euclidean_space"
  shows "b \ Basis \ \x \ b\ \ infnorm x"
  by (simp add: infnorm_Max)

lemma infnorm_mul: "infnorm (a *\<^sub>R x) = \a\ * infnorm x"
  unfolding infnorm_Max
proof (safe intro!: Max_eqI)
  let ?B = "(\i. \x \ i\) ` Basis"
  { fix b :: 'a
    assume "b \ Basis"
    then show "\a *\<^sub>R x \ b\ \ \a\ * Max ?B"
      by (simp add: abs_mult mult_left_mono)
  next
    from Max_in[of ?B] obtain b where "b \ Basis" "Max ?B = \x \ b\"
      by (auto simp del: Max_in)
    then show "\a\ * Max ((\i. \x \ i\) ` Basis) \ (\i. \a *\<^sub>R x \ i\) ` Basis"
      by (intro image_eqI[where x=b]) (auto simp: abs_mult)
  }
qed simp

lemma infnorm_mul_lemma: "infnorm (a *\<^sub>R x) \ \a\ * infnorm x"
  unfolding infnorm_mul ..

lemma infnorm_pos_lt: "infnorm x > 0 \ x \ 0"
  using infnorm_pos_le[of x] infnorm_eq_0[of x] by arith

text \<open>Prove that it differs only up to a bound from Euclidean norm.\<close>

lemma infnorm_le_norm: "infnorm x \ norm x"
  by (simp add: Basis_le_norm infnorm_Max)

lemma norm_le_infnorm:
  fixes x :: "'a::euclidean_space"
  shows "norm x \ sqrt DIM('a) * infnorm x"
  unfolding norm_eq_sqrt_inner id_def
proof (rule real_le_lsqrt)
  show "sqrt DIM('a) * infnorm x \ 0"
    by (simp add: zero_le_mult_iff infnorm_pos_le)
  have "x \ x \ (\b\Basis. x \ b * (x \ b))"
    by (metis euclidean_inner order_refl)
  also have "\ \ DIM('a) * \infnorm x\\<^sup>2"
    by (rule sum_bounded_above) (metis Basis_le_infnorm abs_le_square_iff power2_eq_square real_abs_infnorm)
  also have "\ \ (sqrt DIM('a) * infnorm x)\<^sup>2"
    by (simp add: power_mult_distrib)
  finally show "x \ x \ (sqrt DIM('a) * infnorm x)\<^sup>2" .
qed

lemma tendsto_infnorm [tendsto_intros]:
  assumes "(f \ a) F"
  shows "((\x. infnorm (f x)) \ infnorm a) F"
proof (rule tendsto_compose [OF LIM_I assms])
  fix r :: real
  assume "r > 0"
  then show "\s>0. \x. x \ a \ norm (x - a) < s \ norm (infnorm x - infnorm a) < r"
    by (metis real_norm_def le_less_trans absdiff_infnorm infnorm_le_norm)
qed

text \<open>Equality in Cauchy-Schwarz and triangle inequalities.\<close>

lemma norm_cauchy_schwarz_eq: "x \ y = norm x * norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x"
  (is "?lhs \ ?rhs")
proof (cases "x=0")
  case True
  then show ?thesis
    by auto
next
  case False
  from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
  have "?rhs \
      (norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) -
        norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) = 0)"
    using False unfolding inner_simps
    by (auto simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
  also have "\ \ (2 * norm x * norm y * (norm x * norm y - x \ y) = 0)"
    using False  by (simp add: field_simps inner_commute)
  also have "\ \ ?lhs"
    using False by auto
  finally show ?thesis by metis
qed

lemma norm_cauchy_schwarz_abs_eq:
  "\x \ y\ = norm x * norm y \
    norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm x *\<^sub>R y = - norm y *\<^sub>R x"
  using norm_cauchy_schwarz_eq [symmetric, of x y]
  using norm_cauchy_schwarz_eq [symmetric, of "-x" y] Cauchy_Schwarz_ineq2 [of x y]
  by auto

lemma norm_triangle_eq:
  fixes x y :: "'a::real_inner"
  shows "norm (x + y) = norm x + norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x"
proof (cases "x = 0 \ y = 0")
  case True
  then show ?thesis
    by force
next
  case False
  then have n: "norm x > 0" "norm y > 0"
    by auto
  have "norm (x + y) = norm x + norm y \ (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
    by simp
  also have "\ \ norm x *\<^sub>R y = norm y *\<^sub>R x"
    by (smt (verit, best) dot_norm inner_real_def inner_simps norm_cauchy_schwarz_eq power2_eq_square)
  finally show ?thesis .
qed

lemma dist_triangle_eq:
  fixes x y z :: "'a::real_inner"
  shows "dist x z = dist x y + dist y z \
    norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
  by (metis (no_types, lifting) add_diff_eq diff_add_cancel dist_norm norm_triangle_eq)

subsection \<open>Collinearity\<close>

definition\<^marker>\<open>tag important\<close> collinear :: "'a::real_vector set \<Rightarrow> bool"
  where "collinear S \ (\u. \x \ S. \ y \ S. \c. x - y = c *\<^sub>R u)"

lemma collinear_alt:
     "collinear S \ (\u v. \x \ S. \c. x = u + c *\<^sub>R v)" (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    unfolding collinear_def by (metis add.commute diff_add_cancel)
next
  assume ?rhs
  then obtain u v where *: "\x. x \ S \ \c. x = u + c *\<^sub>R v"
    by auto
  have "\c. x - y = c *\<^sub>R v" if "x \ S" "y \ S" for x y
        by (metis *[OF \<open>x \<in> S\<close>] *[OF \<open>y \<in> S\<close>] scaleR_left.diff add_diff_cancel_left)
  then show ?lhs
    using collinear_def by blast
qed

lemma collinear:
  fixes S :: "'a::{perfect_space,real_vector} set"
  shows "collinear S \ (\u. u \ 0 \ (\x \ S. \ y \ S. \c. x - y = c *\<^sub>R u))"
proof -
  have "\v. v \ 0 \ (\x\S. \y\S. \c. x - y = c *\<^sub>R v)"
    if "\x\S. \y\S. \c. x - y = c *\<^sub>R u" "u=0" for u
  proof -
    have "\x\S. \y\S. x = y"
      using that by auto
    moreover
    obtain v::'a where "v \ 0"
      using UNIV_not_singleton [of 0] by auto
    ultimately have "\x\S. \y\S. \c. x - y = c *\<^sub>R v"
      by auto
    then show ?thesis
      using \<open>v \<noteq> 0\<close> by blast
  qed
  then show ?thesis
    by (metis collinear_def)
qed

lemma collinear_subset: "\collinear T; S \ T\ \ collinear S"
  by (meson collinear_def subsetCE)

lemma collinear_empty [iff]: "collinear {}"
  by (simp add: collinear_def)

lemma collinear_sing [iff]: "collinear {x}"
  by (simp add: collinear_def)

lemma collinear_2 [iff]: "collinear {x, y}"
  by (simp add: collinear_def) (metis minus_diff_eq scaleR_left.minus scaleR_one)

lemma collinear_lemma: "collinear {0, x, y} \ x = 0 \ y = 0 \ (\c. y = c *\<^sub>R x)"
  (is "?lhs \ ?rhs")
proof (cases "x = 0 \ y = 0")
  case True
  then show ?thesis
    by (auto simp: insert_commute)
next
  case False
  show ?thesis
  proof
    assume h: "?lhs"
    then obtain u where u: "\ x\ {0,x,y}. \y\ {0,x,y}. \c. x - y = c *\<^sub>R u"
      unfolding collinear_def by blast
    from u[rule_format, of x 0] u[rule_format, of y 0]
    obtain cx and cy where
      cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
      by auto
    from cx cy False have cx0: "cx \ 0" and cy0: "cy \ 0" by auto
    let ?d = "cy / cx"
    from cx cy cx0 have "y = ?d *\<^sub>R x"
      by simp
    then show ?rhs using False by blast
  next
    assume h: "?rhs"
    then obtain c where c: "y = c *\<^sub>R x"
      using False by blast
    show ?lhs
      apply (simp add: collinear_def c)
      by (metis (mono_tags, lifting) scaleR_left.minus scaleR_left_diff_distrib scaleR_one)
  qed
qed

lemma collinear_iff_Reals: "collinear {0::complex,w,z} \ z/w \ \"
proof
  show "z/w \ \ \ collinear {0,w,z}"
    by (metis Reals_cases collinear_lemma nonzero_divide_eq_eq scaleR_conv_of_real)
qed (auto simp: collinear_lemma scaleR_conv_of_real)

lemma collinear_scaleR_iff: "collinear {0, \ *\<^sub>R w, \ *\<^sub>R z} \ collinear {0,w,z} \ \=0 \ \=0"
  (is "?lhs = ?rhs")
proof (cases "\=0 \ \=0")
  case False
  then have "(\c. \ *\<^sub>R z = (c * \) *\<^sub>R w) = (\c. z = c *\<^sub>R w)"
    by (metis mult.commute scaleR_scaleR vector_fraction_eq_iff)
  then show ?thesis
    by (auto simp add: collinear_lemma)
qed (auto simp: collinear_lemma)

lemma norm_cauchy_schwarz_equal: "\x \ y\ = norm x * norm y \ collinear {0, x, y}"
proof (cases "x=0")
  case True
  then show ?thesis
    by (auto simp: insert_commute)
next
  case False
  then have nnz: "norm x \ 0"
    by auto
  show ?thesis
  proof
    assume "\x \ y\ = norm x * norm y"
    then show "collinear {0, x, y}"
      unfolding norm_cauchy_schwarz_abs_eq collinear_lemma
      by (meson eq_vector_fraction_iff nnz)
  next
    assume "collinear {0, x, y}"
    with False show "\x \ y\ = norm x * norm y"
      unfolding norm_cauchy_schwarz_abs_eq collinear_lemma  by (auto simp: abs_if)
  qed
qed

lemma norm_triangle_eq_imp_collinear:
  fixes x y :: "'a::real_inner"
  assumes "norm (x + y) = norm x + norm y"
  shows "collinear{0,x,y}"
  using assms norm_cauchy_schwarz_abs_eq norm_cauchy_schwarz_equal norm_triangle_eq
  by blast

subsection\<open>Properties of special hyperplanes\<close>

lemma subspace_hyperplane: "subspace {x. a \ x = 0}"
  by (simp add: subspace_def inner_right_distrib)

lemma subspace_hyperplane2: "subspace {x. x \ a = 0}"
  by (simp add: inner_commute inner_right_distrib subspace_def)

lemma special_hyperplane_span:
  fixes S :: "'n::euclidean_space set"
  assumes "k \ Basis"
  shows "{x. k \ x = 0} = span (Basis - {k})"
proof -
  have *: "x \ span (Basis - {k})" if "k \ x = 0" for x
  proof -
    have "x = (\b\Basis. (x \ b) *\<^sub>R b)"
      by (simp add: euclidean_representation)
    also have "\ = (\b \ Basis - {k}. (x \ b) *\<^sub>R b)"
      by (auto simp: sum.remove [of _ k] inner_commute assms that)
    finally have "x = (\b\Basis - {k}. (x \ b) *\<^sub>R b)" .
    then show ?thesis
      by (simp add: span_finite)
  qed
  show ?thesis
    apply (rule span_subspace [symmetric])
    using assms
    apply (auto simp: inner_not_same_Basis intro: * subspace_hyperplane)
    done
qed

lemma dim_special_hyperplane:
  fixes k :: "'n::euclidean_space"
  shows "k \ Basis \ dim {x. k \ x = 0} = DIM('n) - 1"
  by (metis Diff_subset card_Diff_singleton indep_card_eq_dim_span independent_substdbasis special_hyperplane_span)

proposition dim_hyperplane:
  fixes a :: "'a::euclidean_space"
  assumes "a \ 0"
    shows "dim {x. a \ x = 0} = DIM('a) - 1"
proof -
  have span0: "span {x. a \ x = 0} = {x. a \ x = 0}"
    by (rule span_unique) (auto simp: subspace_hyperplane)
  then obtain B where "independent B"
              and Bsub: "B \ {x. a \ x = 0}"
              and subspB: "{x. a \ x = 0} \ span B"
              and card0: "(card B = dim {x. a \ x = 0})"
              and ortho: "pairwise orthogonal B"
    using orthogonal_basis_exists by metis
  with assms have "a \ span B"
    by (metis (mono_tags, lifting) span_eq inner_eq_zero_iff mem_Collect_eq span0)
  then have ind: "independent (insert a B)"
    by (simp add: \<open>independent B\<close> independent_insert)
  have "finite B"
    using \<open>independent B\<close> independent_bound by blast
  have "UNIV \ span (insert a B)"
  proof fix y::'a
    obtain r z where "y = r *\<^sub>R a + z" "a \ z = 0"
      by (metis add.commute diff_add_cancel vector_sub_project_orthogonal)
    then show "y \ span (insert a B)"
      by (metis (mono_tags, lifting) Bsub add_diff_cancel_left'
          mem_Collect_eq span0 span_breakdown_eq span_eq subspB)
  qed
  then have "DIM('a) = dim(insert a B)"
    by (metis independent_Basis span_Basis dim_eq_card top.extremum_uniqueI)
  then show ?thesis
    by (metis One_nat_def \<open>a \<notin> span B\<close> \<open>finite B\<close> card0 card_insert_disjoint
        diff_Suc_Suc diff_zero dim_eq_card_independent ind span_base)
qed

lemma lowdim_eq_hyperplane:
  fixes S :: "'a::euclidean_space set"
  assumes "dim S = DIM('a) - 1"
  obtains a where "a \ 0" and "span S = {x. a \ x = 0}"
proof -
  obtain b where b: "b \ 0" "span S \ {a. b \ a = 0}"
    by (metis DIM_positive assms diff_less zero_less_one lowdim_subset_hyperplane)
  then show ?thesis
    by (metis assms dim_hyperplane dim_span dim_subset subspace_dim_equal subspace_hyperplane subspace_span that)
qed

lemma dim_eq_hyperplane:
  fixes S :: "'n::euclidean_space set"
  shows "dim S = DIM('n) - 1 \ (\a. a \ 0 \ span S = {x. a \ x = 0})"
by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane)

subsection\<open> Orthogonal bases and Gram-Schmidt process\<close>

lemma pairwise_orthogonal_independent:
  assumes "pairwise orthogonal S" and "0 \ S"
    shows "independent S"
proof -
  have 0: "\x y. \x \ y; x \ S; y \ S\ \ x \ y = 0"
    using assms by (simp add: pairwise_def orthogonal_def)
  have "False" if "a \ S" and a: "a \ span (S - {a})" for a
  proof -
    obtain T U where "T \ S - {a}" "a = (\v\T. U v *\<^sub>R v)"
      using a by (force simp: span_explicit)
    then have "a \ a = a \ (\v\T. U v *\<^sub>R v)"
      by simp
    also have "\ = 0"
      apply (simp add: inner_sum_right)
      by (smt (verit) "0" DiffE \<open>T \<subseteq> S - {a}\<close> in_mono insertCI mult_not_zero sum.neutral that(1))
    finally show ?thesis
      using \<open>0 \<notin> S\<close> \<open>a \<in> S\<close> by auto
  qed
  then show ?thesis
    by (force simp: dependent_def)
qed

lemma pairwise_orthogonal_imp_finite:
  fixes S :: "'a::euclidean_space set"
  assumes "pairwise orthogonal S"
    shows "finite S"
  by (metis Set.set_insert assms finite_insert independent_bound pairwise_insert
            pairwise_orthogonal_independent)

lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}"
  by (simp add: subspace_def orthogonal_clauses)

lemma subspace_orthogonal_to_vectors: "subspace {y. \x \ S. orthogonal x y}"
  by (simp add: subspace_def orthogonal_clauses)

lemma orthogonal_to_span:
  assumes a: "a \ span S" and x: "\y. y \ S \ orthogonal x y"
    shows "orthogonal x a"
  by (metis a orthogonal_clauses(1,2,4)
      span_induct_alt x)

proposition Gram_Schmidt_step:
  fixes S :: "'a::euclidean_space set"
  assumes S: "pairwise orthogonal S" and x: "x \ span S"
    shows "orthogonal x (a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b))"
proof -
  have "finite S"
    by (simp add: S pairwise_orthogonal_imp_finite)
  have "orthogonal (a - (\b\S. (b \ a / (b \ b)) *\<^sub>R b)) x"
       if "x \ S" for x
  proof -
    have "a \ x = (\y\S. if y = x then y \ a else 0)"
      by (simp add: \<open>finite S\<close> inner_commute that)
    also have "\ = (\b\S. b \ a * (b \ x) / (b \ b))"
      apply (rule sum.cong [OF refl], simp)
      by (meson S orthogonal_def pairwise_def that)
   finally show ?thesis
     by (simp add: orthogonal_def algebra_simps inner_sum_left)
  qed
  then show ?thesis
    using orthogonal_to_span orthogonal_commute x by blast
qed

lemma orthogonal_extension_aux:
  fixes S :: "'a::euclidean_space set"
  assumes "finite T" "finite S" "pairwise orthogonal S"
    shows "\U. pairwise orthogonal (S \ U) \ span (S \ U) = span (S \ T)"
using assms
proof (induction arbitrary: S)
  case empty then show ?case
    by simp (metis sup_bot_right)
next
  case (insert a T)
  have 0: "\x y. \x \ y; x \ S; y \ S\ \ x \ y = 0"
    using insert by (simp add: pairwise_def orthogonal_def)
  define a' where "a' = a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)"
  obtain U where orthU: "pairwise orthogonal (S \ insert a' U)"
             and spanU: "span (insert a' S \ U) = span (insert a' S \ T)"
    by (rule exE [OF insert.IH [of "insert a' S"]])
      (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute
        pairwise_orthogonal_insert span_clauses)
  have orthS: "\x. x \ S \ a' \ x = 0"
    using Gram_Schmidt_step a'_def insert.prems orthogonal_commute orthogonal_def span_base by blast
  have "span (S \ insert a' U) = span (insert a' (S \ T))"
    using spanU by simp
  also have "\ = span (insert a (S \ T))"
    by (simp add: a'_def span_neg span_sum span_base span_mul eq_span_insert_eq)
  also have "\ = span (S \ insert a T)"
    by simp
  finally show ?case
    using orthU by blast
qed

proposition orthogonal_extension:
  fixes S :: "'a::euclidean_space set"
  assumes S: "pairwise orthogonal S"
  obtains U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ T)"
proof -
  obtain B where "finite B" "span B = span T"
    using basis_subspace_exists [of "span T"] subspace_span by metis
  with orthogonal_extension_aux [of B S]
  obtain U where "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ B)"
    using assms pairwise_orthogonal_imp_finite by auto
  with \<open>span B = span T\<close> show ?thesis
    by (rule_tac U=U in that) (auto simp: span_Un)
qed

corollary\<^marker>\<open>tag unimportant\<close> orthogonal_extension_strong:
  fixes S :: "'a::euclidean_space set"
  assumes S: "pairwise orthogonal S"
  obtains U where "U \ (insert 0 S) = {}" "pairwise orthogonal (S \ U)"
                  "span (S \ U) = span (S \ T)"
proof -
  obtain U where U: "pairwise orthogonal (S \ U)" "span (S \ U) = span (S \ T)"
    using orthogonal_extension assms by blast
  moreover have "pairwise orthogonal (S \ (U - insert 0 S))"
    by (smt (verit, best) Un_Diff_Int Un_iff U pairwise_def)
  ultimately show ?thesis
    by (metis Diff_disjoint Un_Diff_cancel Un_insert_left inf_commute span_insert_0 that)
qed

subsection\<open>Decomposing a vector into parts in orthogonal subspaces\<close>

text\<open>existence of orthonormal basis for a subspace.\<close>

lemma orthogonal_spanningset_subspace:
  fixes S :: "'a :: euclidean_space set"
  assumes "subspace S"
  obtains B where "B \ S" "pairwise orthogonal B" "span B = S"
  by (metis assms basis_orthogonal basis_subspace_exists span_eq)

lemma orthogonal_basis_subspace:
  fixes S :: "'a :: euclidean_space set"
  assumes "subspace S"
  obtains B where "0 \ B" "B \ S" "pairwise orthogonal B" "independent B"
                  "card B = dim S" "span B = S"
  by (metis assms dependent_zero orthogonal_basis_exists span_eq span_eq_iff)

proposition orthonormal_basis_subspace:
  fixes S :: "'a :: euclidean_space set"
  assumes "subspace S"
  obtains B where "B \ S" "pairwise orthogonal B"
              and "\x. x \ B \ norm x = 1"
              and "independent B" "card B = dim S" "span B = S"
proof -
  obtain B where "0 \ B" "B \ S"
             and orth: "pairwise orthogonal B"
             and "independent B" "card B = dim S" "span B = S"
    by (blast intro: orthogonal_basis_subspace [OF assms])
  have 1: "(\x. x /\<^sub>R norm x) ` B \ S"
    using \<open>span B = S\<close> span_superset span_mul by fastforce
  have 2: "pairwise orthogonal ((\x. x /\<^sub>R norm x) ` B)"
    using orth by (force simp: pairwise_def orthogonal_clauses)
  have 3: "\x. x \ (\x. x /\<^sub>R norm x) ` B \ norm x = 1"
    by (metis (no_types, lifting) \<open>0 \<notin> B\<close> image_iff norm_sgn sgn_div_norm)
  have 4: "independent ((\x. x /\<^sub>R norm x) ` B)"
    by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one)
  have "inj_on (\x. x /\<^sub>R norm x) B"
  proof
    fix x y
    assume "x \ B" "y \ B" "x /\<^sub>R norm x = y /\<^sub>R norm y"
    moreover have "\i. i \ B \ norm (i /\<^sub>R norm i) = 1"
      using 3 by blast
    ultimately show "x = y"
      by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one)
  qed
  then have 5: "card ((\x. x /\<^sub>R norm x) ` B) = dim S"
    by (metis \<open>card B = dim S\<close> card_image)
  have 6: "span ((\x. x /\<^sub>R norm x) ` B) = S"
    by (metis "1" "4" "5" assms card_eq_dim independent_imp_finite span_subspace)
  show ?thesis
    by (rule that [OF 1 2 3 4 5 6])
qed

proposition\<^marker>\<open>tag unimportant\<close> orthogonal_to_subspace_exists_gen:
  fixes S :: "'a :: euclidean_space set"
  assumes "span S \ span T"
  obtains x where "x \ 0" "x \ span T" "\y. y \ span S \ orthogonal x y"
proof -
  obtain B where "B \ span S" and orthB: "pairwise orthogonal B"
             and "\x. x \ B \ norm x = 1"
             and "independent B" "card B = dim S" "span B = span S"
    by (metis dim_span orthonormal_basis_subspace subspace_span)
  with assms obtain u where spanBT: "span B \ span T" and "u \ span B" "u \ span T"
    by auto
  obtain C where orthBC: "pairwise orthogonal (B \ C)" and spanBC: "span (B \ C) = span (B \ {u})"
    by (blast intro: orthogonal_extension [OF orthB])
  show thesis
  proof (cases "C \ insert 0 B")
    case True
    then have "C \ span B"
      using span_eq
      by (metis span_insert_0 subset_trans)
    moreover have "u \ span (B \ C)"
      using \<open>span (B \<union> C) = span (B \<union> {u})\<close> span_superset by force
    ultimately show ?thesis
      using True \<open>u \<notin> span B\<close>
      by (metis Un_insert_left span_insert_0 sup.orderE)
  next
    case False
    then obtain x where "x \ C" "x \ 0" "x \ B"
      by blast
    then have "x \ span T"
      by (smt (verit, ccfv_SIG) Set.set_insert  \<open>u \<in> span T\<close> empty_subsetI insert_subset
          le_sup_iff spanBC spanBT span_mono span_span span_superset subset_trans)
    moreover have "orthogonal x y" if "y \ span B" for y
      using that
    proof (rule span_induct)
      show "subspace {a. orthogonal x a}"
        by (simp add: subspace_orthogonal_to_vector)
      show "\b. b \ B \ orthogonal x b"
        by (metis Un_iff \<open>x \<in> C\<close> \<open>x \<notin> B\<close> orthBC pairwise_def)
    qed
    ultimately show ?thesis
      using \<open>x \<noteq> 0\<close> that \<open>span B = span S\<close> by auto
  qed
qed

corollary\<^marker>\<open>tag unimportant\<close> orthogonal_to_subspace_exists:
  fixes S :: "'a :: euclidean_space set"
  assumes "dim S < DIM('a)"
  obtains x where "x \ 0" "\y. y \ span S \ orthogonal x y"
proof -
  have "span S \ UNIV"
    by (metis assms dim_eq_full order_less_imp_not_less top.not_eq_extremum)
  with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis
    by (auto)
qed

corollary\<^marker>\<open>tag unimportant\<close> orthogonal_to_vector_exists:
  fixes x :: "'a :: euclidean_space"
  assumes "2 \ DIM('a)"
  obtains y where "y \ 0" "orthogonal x y"
proof -
  have "dim {x} < DIM('a)"
    using assms by auto
  then show thesis
    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
qed

proposition\<^marker>\<open>tag unimportant\<close> orthogonal_subspace_decomp_exists:
  fixes S :: "'a :: euclidean_space set"
  obtains y z
  where "y \ span S"
    and "\w. w \ span S \ orthogonal z w"
    and "x = y + z"
proof -
  obtain T where "0 \ T" "T \ span S" "pairwise orthogonal T" "independent T"
    "card T = dim (span S)" "span T = span S"
    using orthogonal_basis_subspace subspace_span by blast
  let ?a = "\b\T. (b \ x / (b \ b)) *\<^sub>R b"
  have orth: "orthogonal (x - ?a) w" if "w \ span S" for w
    by (simp add: Gram_Schmidt_step \<open>pairwise orthogonal T\<close> \<open>span T = span S\<close>
        orthogonal_commute that)
  with that[of ?a "x-?a"] \<open>T \<subseteq> span S\<close> show ?thesis
    by (simp add: span_mul span_sum subsetD)
qed

lemma orthogonal_subspace_decomp_unique:
  fixes S :: "'a :: euclidean_space set"
  assumes "x + y = x' + y'"
      and ST: "x \ span S" "x' \ span S" "y \ span T" "y' \ span T"
      and orth: "\a b. \a \ S; b \ T\ \ orthogonal a b"
  shows "x = x' \ y = y'"
proof -
  have "x + y - y' = x'"
    by (simp add: assms)
  moreover have "\a b. \a \ span S; b \ span T\ \ orthogonal a b"
    by (meson orth orthogonal_commute orthogonal_to_span)
  ultimately have "0 = x' - x"
    using assms
    by (metis add.commute add_diff_cancel_right' diff_right_commute orthogonal_self span_diff)
  with assms show ?thesis by auto
qed

lemma vector_in_orthogonal_spanningset:
  fixes a :: "'a::euclidean_space"
  obtains S where "a \ S" "pairwise orthogonal S" "span S = UNIV"
  by (metis UnI1 Un_UNIV_right insertI1 orthogonal_extension pairwise_singleton span_UNIV)

lemma vector_in_orthogonal_basis:
  fixes a :: "'a::euclidean_space"
  assumes "a \ 0"
  obtains S where "a \ S" "0 \ S" "pairwise orthogonal S" "independent S" "finite S"
                  "span S = UNIV" "card S = DIM('a)"
proof -
  obtain S where S: "a \ S" "pairwise orthogonal S" "span S = UNIV"
    using vector_in_orthogonal_spanningset .
  show thesis
  proof
    show "pairwise orthogonal (S - {0})"
      using pairwise_mono S(2) by blast
    show "independent (S - {0})"
      by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent)
    show "finite (S - {0})"
      using \<open>independent (S - {0})\<close> independent_imp_finite by blast
    show "card (S - {0}) = DIM('a)"
      using span_delete_0 [of S] S
      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span)
  qed (use S \<open>a \<noteq> 0\<close> in auto)
qed

lemma vector_in_orthonormal_basis:
  fixes a :: "'a::euclidean_space"
  assumes "norm a = 1"
  obtains S where "a \ S" "pairwise orthogonal S" "\x. x \ S \ norm x = 1"
    "independent S" "card S = DIM('a)" "span S = UNIV"
proof -
  have "a \ 0"
    using assms by auto
  then obtain S where "a \ S" "0 \ S" "finite S"
          and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)"
    by (metis vector_in_orthogonal_basis)
  let ?S = "(\x. x /\<^sub>R norm x) ` S"
  show thesis
  proof
    show "a \ ?S"
      using \<open>a \<in> S\<close> assms image_iff by fastforce
  next
    show "pairwise orthogonal ?S"
      using \<open>pairwise orthogonal S\<close> by (auto simp: pairwise_def orthogonal_def)
    show "\x. x \ (\x. x /\<^sub>R norm x) ` S \ norm x = 1"
      using \<open>0 \<notin> S\<close> by (auto simp: field_split_simps)
    then show ind: "independent ?S"
      by (metis \<open>pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` S)\<close> norm_zero pairwise_orthogonal_independent zero_neq_one)
    have "inj_on (\x. x /\<^sub>R norm x) S"
      unfolding inj_on_def
      by (metis (full_types) S(1) \<open>0 \<notin> S\<close> inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def)
--> --------------------

--> maximum size reached

--> --------------------

quality98%

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.