8300 qed |
8300 qed |
8301 ultimately show ?thesis |
8301 ultimately show ?thesis |
8302 using that by metis |
8302 using that by metis |
8303 qed |
8303 qed |
8304 |
8304 |
|
8305 |
|
8306 subsection{*Orthogonal complement*} |
|
8307 |
|
8308 definition orthogonal_comp ("_\<^sup>\<bottom>" [80] 80) |
|
8309 where "orthogonal_comp W \<equiv> {x. \<forall>y \<in> W. orthogonal y x}" |
|
8310 |
|
8311 lemma subspace_orthogonal_comp: "subspace (W\<^sup>\<bottom>)" |
|
8312 unfolding subspace_def orthogonal_comp_def orthogonal_def |
|
8313 by (auto simp: inner_right_distrib) |
|
8314 |
|
8315 lemma orthogonal_comp_anti_mono: |
|
8316 assumes "A \<subseteq> B" |
|
8317 shows "B\<^sup>\<bottom> \<subseteq> A\<^sup>\<bottom>" |
|
8318 proof |
|
8319 fix x assume x: "x \<in> B\<^sup>\<bottom>" |
|
8320 show "x \<in> orthogonal_comp A" using x unfolding orthogonal_comp_def |
|
8321 by (simp add: orthogonal_def, metis assms in_mono) |
|
8322 qed |
|
8323 |
|
8324 lemma orthogonal_comp_null [simp]: "{0}\<^sup>\<bottom> = UNIV" |
|
8325 by (auto simp: orthogonal_comp_def orthogonal_def) |
|
8326 |
|
8327 lemma orthogonal_comp_UNIV [simp]: "UNIV\<^sup>\<bottom> = {0}" |
|
8328 unfolding orthogonal_comp_def orthogonal_def |
|
8329 by auto (use inner_eq_zero_iff in blast) |
|
8330 |
|
8331 lemma orthogonal_comp_subset: "U \<subseteq> U\<^sup>\<bottom>\<^sup>\<bottom>" |
|
8332 by (auto simp: orthogonal_comp_def orthogonal_def inner_commute) |
|
8333 |
|
8334 lemma subspace_sum_minimal: |
|
8335 assumes "S \<subseteq> U" "T \<subseteq> U" "subspace U" |
|
8336 shows "S + T \<subseteq> U" |
|
8337 proof |
|
8338 fix x |
|
8339 assume "x \<in> S + T" |
|
8340 then obtain xs xt where "xs \<in> S" "xt \<in> T" "x = xs+xt" |
|
8341 by (meson set_plus_elim) |
|
8342 then show "x \<in> U" |
|
8343 by (meson assms subsetCE subspace_add) |
|
8344 qed |
|
8345 |
|
8346 lemma subspace_sum_orthogonal_comp: |
|
8347 fixes U :: "'a :: euclidean_space set" |
|
8348 assumes "subspace U" |
|
8349 shows "U + U\<^sup>\<bottom> = UNIV" |
|
8350 proof - |
|
8351 obtain B where "B \<subseteq> U" |
|
8352 and ortho: "pairwise orthogonal B" "\<And>x. x \<in> B \<Longrightarrow> norm x = 1" |
|
8353 and "independent B" "card B = dim U" "span B = U" |
|
8354 using orthonormal_basis_subspace [OF assms] by metis |
|
8355 then have "finite B" |
|
8356 by (simp add: indep_card_eq_dim_span) |
|
8357 have *: "\<forall>x\<in>B. \<forall>y\<in>B. x \<bullet> y = (if x=y then 1 else 0)" |
|
8358 using ortho norm_eq_1 by (auto simp: orthogonal_def pairwise_def) |
|
8359 { fix v |
|
8360 let ?u = "\<Sum>b\<in>B. (v \<bullet> b) *\<^sub>R b" |
|
8361 have "v = ?u + (v - ?u)" |
|
8362 by simp |
|
8363 moreover have "?u \<in> U" |
|
8364 by (metis (no_types, lifting) \<open>span B = U\<close> assms real_vector_class.subspace_sum span_clauses(1) span_mul) |
|
8365 moreover have "(v - ?u) \<in> U\<^sup>\<bottom>" |
|
8366 proof (clarsimp simp: orthogonal_comp_def orthogonal_def) |
|
8367 fix y |
|
8368 assume "y \<in> U" |
|
8369 with \<open>span B = U\<close> span_finite [OF \<open>finite B\<close>] |
|
8370 obtain u where u: "y = (\<Sum>b\<in>B. u b *\<^sub>R b)" |
|
8371 by auto |
|
8372 have "b \<bullet> (v - ?u) = 0" if "b \<in> B" for b |
|
8373 using that \<open>finite B\<close> |
|
8374 by (simp add: * algebra_simps inner_sum_right if_distrib [of "( *)v" for v] inner_commute cong: if_cong) |
|
8375 then show "y \<bullet> (v - ?u) = 0" |
|
8376 by (simp add: u inner_sum_left) |
|
8377 qed |
|
8378 ultimately have "v \<in> U + U\<^sup>\<bottom>" |
|
8379 using set_plus_intro by fastforce |
|
8380 } then show ?thesis |
|
8381 by auto |
|
8382 qed |
|
8383 |
|
8384 lemma orthogonal_Int_0: |
|
8385 assumes "subspace U" |
|
8386 shows "U \<inter> U\<^sup>\<bottom> = {0}" |
|
8387 using orthogonal_comp_def orthogonal_self |
|
8388 by (force simp: assms subspace_0 subspace_orthogonal_comp) |
|
8389 |
|
8390 lemma orthogonal_comp_self: |
|
8391 fixes U :: "'a :: euclidean_space set" |
|
8392 assumes "subspace U" |
|
8393 shows "U\<^sup>\<bottom>\<^sup>\<bottom> = U" |
|
8394 proof |
|
8395 have ssU': "subspace (U\<^sup>\<bottom>)" |
|
8396 by (simp add: subspace_orthogonal_comp) |
|
8397 have "u \<in> U" if "u \<in> U\<^sup>\<bottom>\<^sup>\<bottom>" for u |
|
8398 proof - |
|
8399 obtain v w where "u = v+w" "v \<in> U" "w \<in> U\<^sup>\<bottom>" |
|
8400 using subspace_sum_orthogonal_comp [OF assms] set_plus_elim by blast |
|
8401 then have "u-v \<in> U\<^sup>\<bottom>" |
|
8402 by simp |
|
8403 moreover have "v \<in> U\<^sup>\<bottom>\<^sup>\<bottom>" |
|
8404 using \<open>v \<in> U\<close> orthogonal_comp_subset by blast |
|
8405 then have "u-v \<in> U\<^sup>\<bottom>\<^sup>\<bottom>" |
|
8406 by (simp add: subspace_diff subspace_orthogonal_comp that) |
|
8407 ultimately have "u-v = 0" |
|
8408 using orthogonal_Int_0 ssU' by blast |
|
8409 with \<open>v \<in> U\<close> show ?thesis |
|
8410 by auto |
|
8411 qed |
|
8412 then show "U\<^sup>\<bottom>\<^sup>\<bottom> \<subseteq> U" |
|
8413 by auto |
|
8414 qed (use orthogonal_comp_subset in auto) |
|
8415 |
|
8416 lemma ker_orthogonal_comp_adjoint: |
|
8417 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space" |
|
8418 assumes "linear f" |
|
8419 shows "f -` {0} = (range (adjoint f))\<^sup>\<bottom>" |
|
8420 apply (auto simp: orthogonal_comp_def orthogonal_def) |
|
8421 apply (simp add: adjoint_works assms(1) inner_commute) |
|
8422 by (metis adjoint_works all_zero_iff assms(1) inner_commute) |
|
8423 |
|
8424 |
8305 end |
8425 end |
8306 |
8426 |