src/HOL/Multivariate_Analysis/Euclidean_Space.thy
changeset 37664 2946b8f057df
parent 37647 a5400b94d2dd
child 37731 8c6bfe10a4ae
equal deleted inserted replaced
37663:f2c98b8c0c5c 37664:2946b8f057df
  1400   {fix y u assume u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y"
  1400   {fix y u assume u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y"
  1401     then have "y \<in> span S" using fS unfolding span_explicit by auto}
  1401     then have "y \<in> span S" using fS unfolding span_explicit by auto}
  1402   ultimately show ?thesis by blast
  1402   ultimately show ?thesis by blast
  1403 qed
  1403 qed
  1404 
  1404 
       
  1405 lemma Int_Un_cancel: "(A \<union> B) \<inter> A = A" "(A \<union> B) \<inter> B = B" by auto
       
  1406 
       
  1407 lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
       
  1408 proof safe
       
  1409   fix x assume "x \<in> span (A \<union> B)"
       
  1410   then obtain S u where S: "finite S" "S \<subseteq> A \<union> B" and x: "x = (\<Sum>v\<in>S. u v *\<^sub>R v)"
       
  1411     unfolding span_explicit by auto
       
  1412 
       
  1413   let ?Sa = "\<Sum>v\<in>S\<inter>A. u v *\<^sub>R v"
       
  1414   let ?Sb = "(\<Sum>v\<in>S\<inter>(B - A). u v *\<^sub>R v)"
       
  1415   show "x \<in> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
       
  1416   proof
       
  1417     show "x = (case (?Sa, ?Sb) of (a, b) \<Rightarrow> a + b)"
       
  1418       unfolding x using S
       
  1419       by (simp, subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
       
  1420 
       
  1421     from S have "?Sa \<in> span A" unfolding span_explicit
       
  1422       by (auto intro!: exI[of _ "S \<inter> A"])
       
  1423     moreover from S have "?Sb \<in> span B" unfolding span_explicit
       
  1424       by (auto intro!: exI[of _ "S \<inter> (B - A)"])
       
  1425     ultimately show "(?Sa, ?Sb) \<in> span A \<times> span B" by simp
       
  1426   qed
       
  1427 next
       
  1428   fix a b assume "a \<in> span A" and "b \<in> span B"
       
  1429   then obtain Sa ua Sb ub where span:
       
  1430     "finite Sa" "Sa \<subseteq> A" "a = (\<Sum>v\<in>Sa. ua v *\<^sub>R v)"
       
  1431     "finite Sb" "Sb \<subseteq> B" "b = (\<Sum>v\<in>Sb. ub v *\<^sub>R v)"
       
  1432     unfolding span_explicit by auto
       
  1433   let "?u v" = "(if v \<in> Sa then ua v else 0) + (if v \<in> Sb then ub v else 0)"
       
  1434   from span have "finite (Sa \<union> Sb)" "Sa \<union> Sb \<subseteq> A \<union> B"
       
  1435     and "a + b = (\<Sum>v\<in>(Sa\<union>Sb). ?u v *\<^sub>R v)"
       
  1436     unfolding setsum_addf scaleR_left_distrib
       
  1437     by (auto simp add: if_distrib cond_application_beta setsum_cases Int_Un_cancel)
       
  1438   thus "a + b \<in> span (A \<union> B)"
       
  1439     unfolding span_explicit by (auto intro!: exI[of _ ?u])
       
  1440 qed
  1405 
  1441 
  1406 text {* This is useful for building a basis step-by-step. *}
  1442 text {* This is useful for building a basis step-by-step. *}
  1407 
  1443 
  1408 lemma independent_insert:
  1444 lemma independent_insert:
  1409   "independent(insert a S) \<longleftrightarrow>
  1445   "independent(insert a S) \<longleftrightarrow>
  1643   have "j < DIM('a) \<Longrightarrow> basis j \<noteq> 0"
  1679   have "j < DIM('a) \<Longrightarrow> basis j \<noteq> 0"
  1644     using independent_basis by (auto intro!: dependent_0)
  1680     using independent_basis by (auto intro!: dependent_0)
  1645   thus "basis j = 0 \<Longrightarrow> DIM('a) \<le> j" unfolding not_le[symmetric] by blast
  1681   thus "basis j = 0 \<Longrightarrow> DIM('a) \<le> j" unfolding not_le[symmetric] by blast
  1646 qed
  1682 qed
  1647 
  1683 
  1648 lemma (in real_basis) basis_range:
       
  1649     "range (basis) = {0} \<union> basis ` {..<DIM('a)}"
       
  1650   using basis_finite by (fastsimp simp: image_def)
       
  1651 
       
  1652 lemma (in real_basis) range_basis:
  1684 lemma (in real_basis) range_basis:
  1653     "range basis = insert 0 (basis ` {..<DIM('a)})"
  1685     "range basis = insert 0 (basis ` {..<DIM('a)})"
  1654 proof -
  1686 proof -
  1655   have *: "UNIV = {..<DIM('a)} \<union> {DIM('a)..}" by auto
  1687   have *: "UNIV = {..<DIM('a)} \<union> {DIM('a)..}" by auto
  1656   show ?thesis unfolding * image_Un basis_finite by auto
  1688   show ?thesis unfolding * image_Un basis_finite by auto
  1679 proof -
  1711 proof -
  1680   have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]]
  1712   have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]]
  1681   have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x"
  1713   have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x"
  1682     unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto
  1714     unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto
  1683   thus ?thesis by fastsimp
  1715   thus ?thesis by fastsimp
       
  1716 qed
       
  1717 
       
  1718 lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = UNIV"
       
  1719   apply(subst span_basis[symmetric]) unfolding range_basis by auto
       
  1720 
       
  1721 lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = DIM('a)"
       
  1722   apply(subst card_image) using basis_inj by auto
       
  1723 
       
  1724 lemma in_span_basis: "(x::'a::real_basis) \<in> span (basis ` {..<DIM('a)})"
       
  1725   unfolding span_basis' ..
       
  1726 
       
  1727 lemma independent_eq_inj_on:
       
  1728   fixes D :: nat and f :: "nat \<Rightarrow> 'c::real_vector" assumes *: "inj_on f {..<D}"
       
  1729   shows "independent (f ` {..<D}) \<longleftrightarrow> (\<forall>a u. a < D \<longrightarrow> (\<Sum>i\<in>{..<D}-{a}. u (f i) *\<^sub>R f i) \<noteq> f a)"
       
  1730 proof -
       
  1731   from * have eq: "\<And>i. i < D \<Longrightarrow> f ` {..<D} - {f i} = f`({..<D} - {i})"
       
  1732     and inj: "\<And>i. inj_on f ({..<D} - {i})"
       
  1733     by (auto simp: inj_on_def)
       
  1734   have *: "\<And>i. finite (f ` {..<D} - {i})" by simp
       
  1735   show ?thesis unfolding dependent_def span_finite[OF *]
       
  1736     by (auto simp: eq setsum_reindex[OF inj])
  1684 qed
  1737 qed
  1685 
  1738 
  1686 class real_basis_with_inner = real_inner + real_basis
  1739 class real_basis_with_inner = real_inner + real_basis
  1687 begin
  1740 begin
  1688 
  1741 
  2054     using h.bounded_linear_left h.bounded_linear_right
  2107     using h.bounded_linear_left h.bounded_linear_right
  2055     by simp
  2108     by simp
  2056 qed
  2109 qed
  2057 
  2110 
  2058 subsection {* We continue. *}
  2111 subsection {* We continue. *}
  2059 
       
  2060 (** move **)
       
  2061 lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = UNIV"
       
  2062   apply(subst span_basis[THEN sym]) unfolding basis_range by auto
       
  2063 
       
  2064 lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = DIM('a)"
       
  2065   apply(subst card_image) using basis_inj by auto
       
  2066 
  2112 
  2067 lemma independent_bound:
  2113 lemma independent_bound:
  2068   fixes S:: "('a::euclidean_space) set"
  2114   fixes S:: "('a::euclidean_space) set"
  2069   shows "independent S \<Longrightarrow> finite S \<and> card S <= DIM('a::euclidean_space)"
  2115   shows "independent S \<Longrightarrow> finite S \<and> card S <= DIM('a::euclidean_space)"
  2070   using independent_span_bound[of "(basis::nat=>'a) ` {..<DIM('a)}" S] by auto
  2116   using independent_span_bound[of "(basis::nat=>'a) ` {..<DIM('a)}" S] by auto