src/HOL/Analysis/Linear_Algebra.thy
 changeset 69619 3f7d8e05e0f2 parent 69600 86e8e7347ac0 child 69674 fc252acb7100
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Mon Jan 07 13:33:29 2019 +0100
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Jan 07 14:06:54 2019 +0100
1.3 @@ -111,6 +111,49 @@
1.4    then show "x = y" by simp
1.5  qed simp
1.6
1.7 +subsection \<open>Substandard Basis\<close>
1.8 +
1.9 +lemma ex_card:
1.10 +  assumes "n \<le> card A"
1.11 +  shows "\<exists>S\<subseteq>A. card S = n"
1.12 +proof (cases "finite A")
1.13 +  case True
1.14 +  from ex_bij_betw_nat_finite[OF this] obtain f where f: "bij_betw f {0..<card A} A" ..
1.15 +  moreover from f \<open>n \<le> card A\<close> have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
1.16 +    by (auto simp: bij_betw_def intro: subset_inj_on)
1.17 +  ultimately have "f ` {..< n} \<subseteq> A" "card (f ` {..< n}) = n"
1.18 +    by (auto simp: bij_betw_def card_image)
1.19 +  then show ?thesis by blast
1.20 +next
1.21 +  case False
1.22 +  with \<open>n \<le> card A\<close> show ?thesis by force
1.23 +qed
1.24 +
1.25 +lemma subspace_substandard: "subspace {x::'a::euclidean_space. (\<forall>i\<in>Basis. P i \<longrightarrow> x\<bullet>i = 0)}"
1.26 +  by (auto simp: subspace_def inner_add_left)
1.27 +
1.28 +lemma dim_substandard:
1.29 +  assumes d: "d \<subseteq> Basis"
1.30 +  shows "dim {x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0} = card d" (is "dim ?A = _")
1.31 +proof (rule dim_unique)
1.32 +  from d show "d \<subseteq> ?A"
1.33 +    by (auto simp: inner_Basis)
1.34 +  from d show "independent d"
1.35 +    by (rule independent_mono [OF independent_Basis])
1.36 +  have "x \<in> span d" if "\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0" for x
1.37 +  proof -
1.38 +    have "finite d"
1.39 +      by (rule finite_subset [OF d finite_Basis])
1.40 +    then have "(\<Sum>i\<in>d. (x \<bullet> i) *\<^sub>R i) \<in> span d"
1.41 +      by (simp add: span_sum span_clauses)
1.42 +    also have "(\<Sum>i\<in>d. (x \<bullet> i) *\<^sub>R i) = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i)"
1.43 +      by (rule sum.mono_neutral_cong_left [OF finite_Basis d]) (auto simp: that)
1.44 +    finally show "x \<in> span d"
1.45 +      by (simp only: euclidean_representation)
1.46 +  qed
1.47 +  then show "?A \<subseteq> span d" by auto
1.48 +qed simp
1.49 +
1.50
1.51  subsection \<open>Orthogonality\<close>
1.52
1.53 @@ -858,6 +901,7 @@
1.54    shows "f = g"
1.55    using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg by blast
1.56
1.57 +
1.58  subsection \<open>Infinity norm\<close>
1.59
1.60  definition%important "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
```