src/HOL/Multivariate_Analysis/Euclidean_Space.thy
 changeset 37664 2946b8f057df parent 37647 a5400b94d2dd child 37731 8c6bfe10a4ae
equal 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 `
`  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. *}`
`  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`