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}"