1208 with False show "\<bar>x \<bullet> y\<bar> = norm x * norm y" |
1341 with False show "\<bar>x \<bullet> y\<bar> = norm x * norm y" |
1209 unfolding norm_cauchy_schwarz_abs_eq collinear_lemma by (auto simp: abs_if) |
1342 unfolding norm_cauchy_schwarz_abs_eq collinear_lemma by (auto simp: abs_if) |
1210 qed |
1343 qed |
1211 qed |
1344 qed |
1212 |
1345 |
|
1346 |
|
1347 subsection\<open>Properties of special hyperplanes\<close> |
|
1348 |
|
1349 lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}" |
|
1350 by (simp add: subspace_def inner_right_distrib) |
|
1351 |
|
1352 lemma subspace_hyperplane2: "subspace {x. x \<bullet> a = 0}" |
|
1353 by (simp add: inner_commute inner_right_distrib subspace_def) |
|
1354 |
|
1355 lemma special_hyperplane_span: |
|
1356 fixes S :: "'n::euclidean_space set" |
|
1357 assumes "k \<in> Basis" |
|
1358 shows "{x. k \<bullet> x = 0} = span (Basis - {k})" |
|
1359 proof - |
|
1360 have *: "x \<in> span (Basis - {k})" if "k \<bullet> x = 0" for x |
|
1361 proof - |
|
1362 have "x = (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b)" |
|
1363 by (simp add: euclidean_representation) |
|
1364 also have "... = (\<Sum>b \<in> Basis - {k}. (x \<bullet> b) *\<^sub>R b)" |
|
1365 by (auto simp: sum.remove [of _ k] inner_commute assms that) |
|
1366 finally have "x = (\<Sum>b\<in>Basis - {k}. (x \<bullet> b) *\<^sub>R b)" . |
|
1367 then show ?thesis |
|
1368 by (simp add: span_finite) |
|
1369 qed |
|
1370 show ?thesis |
|
1371 apply (rule span_subspace [symmetric]) |
|
1372 using assms |
|
1373 apply (auto simp: inner_not_same_Basis intro: * subspace_hyperplane) |
|
1374 done |
|
1375 qed |
|
1376 |
|
1377 lemma dim_special_hyperplane: |
|
1378 fixes k :: "'n::euclidean_space" |
|
1379 shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1" |
|
1380 apply (simp add: special_hyperplane_span) |
|
1381 apply (rule dim_unique [OF subset_refl]) |
|
1382 apply (auto simp: independent_substdbasis) |
|
1383 apply (metis member_remove remove_def span_base) |
|
1384 done |
|
1385 |
|
1386 proposition dim_hyperplane: |
|
1387 fixes a :: "'a::euclidean_space" |
|
1388 assumes "a \<noteq> 0" |
|
1389 shows "dim {x. a \<bullet> x = 0} = DIM('a) - 1" |
|
1390 proof - |
|
1391 have span0: "span {x. a \<bullet> x = 0} = {x. a \<bullet> x = 0}" |
|
1392 by (rule span_unique) (auto simp: subspace_hyperplane) |
|
1393 then obtain B where "independent B" |
|
1394 and Bsub: "B \<subseteq> {x. a \<bullet> x = 0}" |
|
1395 and subspB: "{x. a \<bullet> x = 0} \<subseteq> span B" |
|
1396 and card0: "(card B = dim {x. a \<bullet> x = 0})" |
|
1397 and ortho: "pairwise orthogonal B" |
|
1398 using orthogonal_basis_exists by metis |
|
1399 with assms have "a \<notin> span B" |
|
1400 by (metis (mono_tags, lifting) span_eq inner_eq_zero_iff mem_Collect_eq span0) |
|
1401 then have ind: "independent (insert a B)" |
|
1402 by (simp add: \<open>independent B\<close> independent_insert) |
|
1403 have "finite B" |
|
1404 using \<open>independent B\<close> independent_bound by blast |
|
1405 have "UNIV \<subseteq> span (insert a B)" |
|
1406 proof fix y::'a |
|
1407 obtain r z where z: "y = r *\<^sub>R a + z" "a \<bullet> z = 0" |
|
1408 apply (rule_tac r="(a \<bullet> y) / (a \<bullet> a)" and z = "y - ((a \<bullet> y) / (a \<bullet> a)) *\<^sub>R a" in that) |
|
1409 using assms |
|
1410 by (auto simp: algebra_simps) |
|
1411 show "y \<in> span (insert a B)" |
|
1412 by (metis (mono_tags, lifting) z Bsub span_eq_iff |
|
1413 add_diff_cancel_left' mem_Collect_eq span0 span_breakdown_eq span_subspace subspB) |
|
1414 qed |
|
1415 then have dima: "DIM('a) = dim(insert a B)" |
|
1416 by (metis independent_Basis span_Basis dim_eq_card top.extremum_uniqueI) |
|
1417 then show ?thesis |
|
1418 by (metis (mono_tags, lifting) Bsub Diff_insert_absorb \<open>a \<notin> span B\<close> ind card0 |
|
1419 card_Diff_singleton dim_span indep_card_eq_dim_span insertI1 subsetCE |
|
1420 subspB) |
|
1421 qed |
|
1422 |
|
1423 lemma lowdim_eq_hyperplane: |
|
1424 fixes S :: "'a::euclidean_space set" |
|
1425 assumes "dim S = DIM('a) - 1" |
|
1426 obtains a where "a \<noteq> 0" and "span S = {x. a \<bullet> x = 0}" |
|
1427 proof - |
|
1428 have dimS: "dim S < DIM('a)" |
|
1429 by (simp add: assms) |
|
1430 then obtain b where b: "b \<noteq> 0" "span S \<subseteq> {a. b \<bullet> a = 0}" |
|
1431 using lowdim_subset_hyperplane [of S] by fastforce |
|
1432 show ?thesis |
|
1433 apply (rule that[OF b(1)]) |
|
1434 apply (rule subspace_dim_equal) |
|
1435 by (auto simp: assms b dim_hyperplane dim_span subspace_hyperplane |
|
1436 subspace_span) |
|
1437 qed |
|
1438 |
|
1439 lemma dim_eq_hyperplane: |
|
1440 fixes S :: "'n::euclidean_space set" |
|
1441 shows "dim S = DIM('n) - 1 \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> span S = {x. a \<bullet> x = 0})" |
|
1442 by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane) |
|
1443 |
|
1444 |
|
1445 subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close> |
|
1446 |
|
1447 lemma pairwise_orthogonal_independent: |
|
1448 assumes "pairwise orthogonal S" and "0 \<notin> S" |
|
1449 shows "independent S" |
|
1450 proof - |
|
1451 have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0" |
|
1452 using assms by (simp add: pairwise_def orthogonal_def) |
|
1453 have "False" if "a \<in> S" and a: "a \<in> span (S - {a})" for a |
|
1454 proof - |
|
1455 obtain T U where "T \<subseteq> S - {a}" "a = (\<Sum>v\<in>T. U v *\<^sub>R v)" |
|
1456 using a by (force simp: span_explicit) |
|
1457 then have "a \<bullet> a = a \<bullet> (\<Sum>v\<in>T. U v *\<^sub>R v)" |
|
1458 by simp |
|
1459 also have "... = 0" |
|
1460 apply (simp add: inner_sum_right) |
|
1461 apply (rule comm_monoid_add_class.sum.neutral) |
|
1462 by (metis "0" DiffE \<open>T \<subseteq> S - {a}\<close> mult_not_zero singletonI subsetCE \<open>a \<in> S\<close>) |
|
1463 finally show ?thesis |
|
1464 using \<open>0 \<notin> S\<close> \<open>a \<in> S\<close> by auto |
|
1465 qed |
|
1466 then show ?thesis |
|
1467 by (force simp: dependent_def) |
|
1468 qed |
|
1469 |
|
1470 lemma pairwise_orthogonal_imp_finite: |
|
1471 fixes S :: "'a::euclidean_space set" |
|
1472 assumes "pairwise orthogonal S" |
|
1473 shows "finite S" |
|
1474 proof - |
|
1475 have "independent (S - {0})" |
|
1476 apply (rule pairwise_orthogonal_independent) |
|
1477 apply (metis Diff_iff assms pairwise_def) |
|
1478 by blast |
|
1479 then show ?thesis |
|
1480 by (meson independent_imp_finite infinite_remove) |
|
1481 qed |
|
1482 |
|
1483 lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}" |
|
1484 by (simp add: subspace_def orthogonal_clauses) |
|
1485 |
|
1486 lemma subspace_orthogonal_to_vectors: "subspace {y. \<forall>x \<in> S. orthogonal x y}" |
|
1487 by (simp add: subspace_def orthogonal_clauses) |
|
1488 |
|
1489 lemma orthogonal_to_span: |
|
1490 assumes a: "a \<in> span S" and x: "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y" |
|
1491 shows "orthogonal x a" |
|
1492 by (metis a orthogonal_clauses(1,2,4) |
|
1493 span_induct_alt x) |
|
1494 |
|
1495 proposition Gram_Schmidt_step: |
|
1496 fixes S :: "'a::euclidean_space set" |
|
1497 assumes S: "pairwise orthogonal S" and x: "x \<in> span S" |
|
1498 shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))" |
|
1499 proof - |
|
1500 have "finite S" |
|
1501 by (simp add: S pairwise_orthogonal_imp_finite) |
|
1502 have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x" |
|
1503 if "x \<in> S" for x |
|
1504 proof - |
|
1505 have "a \<bullet> x = (\<Sum>y\<in>S. if y = x then y \<bullet> a else 0)" |
|
1506 by (simp add: \<open>finite S\<close> inner_commute sum.delta that) |
|
1507 also have "... = (\<Sum>b\<in>S. b \<bullet> a * (b \<bullet> x) / (b \<bullet> b))" |
|
1508 apply (rule sum.cong [OF refl], simp) |
|
1509 by (meson S orthogonal_def pairwise_def that) |
|
1510 finally show ?thesis |
|
1511 by (simp add: orthogonal_def algebra_simps inner_sum_left) |
|
1512 qed |
|
1513 then show ?thesis |
|
1514 using orthogonal_to_span orthogonal_commute x by blast |
|
1515 qed |
|
1516 |
|
1517 |
|
1518 lemma orthogonal_extension_aux: |
|
1519 fixes S :: "'a::euclidean_space set" |
|
1520 assumes "finite T" "finite S" "pairwise orthogonal S" |
|
1521 shows "\<exists>U. pairwise orthogonal (S \<union> U) \<and> span (S \<union> U) = span (S \<union> T)" |
|
1522 using assms |
|
1523 proof (induction arbitrary: S) |
|
1524 case empty then show ?case |
|
1525 by simp (metis sup_bot_right) |
|
1526 next |
|
1527 case (insert a T) |
|
1528 have 0: "\<And>x y. \<lbrakk>x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<bullet> y = 0" |
|
1529 using insert by (simp add: pairwise_def orthogonal_def) |
|
1530 define a' where "a' = a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)" |
|
1531 obtain U where orthU: "pairwise orthogonal (S \<union> insert a' U)" |
|
1532 and spanU: "span (insert a' S \<union> U) = span (insert a' S \<union> T)" |
|
1533 by (rule exE [OF insert.IH [of "insert a' S"]]) |
|
1534 (auto simp: Gram_Schmidt_step a'_def insert.prems orthogonal_commute |
|
1535 pairwise_orthogonal_insert span_clauses) |
|
1536 have orthS: "\<And>x. x \<in> S \<Longrightarrow> a' \<bullet> x = 0" |
|
1537 apply (simp add: a'_def) |
|
1538 using Gram_Schmidt_step [OF \<open>pairwise orthogonal S\<close>] |
|
1539 apply (force simp: orthogonal_def inner_commute span_superset [THEN subsetD]) |
|
1540 done |
|
1541 have "span (S \<union> insert a' U) = span (insert a' (S \<union> T))" |
|
1542 using spanU by simp |
|
1543 also have "... = span (insert a (S \<union> T))" |
|
1544 apply (rule eq_span_insert_eq) |
|
1545 apply (simp add: a'_def span_neg span_sum span_base span_mul) |
|
1546 done |
|
1547 also have "... = span (S \<union> insert a T)" |
|
1548 by simp |
|
1549 finally show ?case |
|
1550 by (rule_tac x="insert a' U" in exI) (use orthU in auto) |
|
1551 qed |
|
1552 |
|
1553 |
|
1554 proposition orthogonal_extension: |
|
1555 fixes S :: "'a::euclidean_space set" |
|
1556 assumes S: "pairwise orthogonal S" |
|
1557 obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)" |
|
1558 proof - |
|
1559 obtain B where "finite B" "span B = span T" |
|
1560 using basis_subspace_exists [of "span T"] subspace_span by metis |
|
1561 with orthogonal_extension_aux [of B S] |
|
1562 obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> B)" |
|
1563 using assms pairwise_orthogonal_imp_finite by auto |
|
1564 with \<open>span B = span T\<close> show ?thesis |
|
1565 by (rule_tac U=U in that) (auto simp: span_Un) |
|
1566 qed |
|
1567 |
|
1568 corollary%unimportant orthogonal_extension_strong: |
|
1569 fixes S :: "'a::euclidean_space set" |
|
1570 assumes S: "pairwise orthogonal S" |
|
1571 obtains U where "U \<inter> (insert 0 S) = {}" "pairwise orthogonal (S \<union> U)" |
|
1572 "span (S \<union> U) = span (S \<union> T)" |
|
1573 proof - |
|
1574 obtain U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)" |
|
1575 using orthogonal_extension assms by blast |
|
1576 then show ?thesis |
|
1577 apply (rule_tac U = "U - (insert 0 S)" in that) |
|
1578 apply blast |
|
1579 apply (force simp: pairwise_def) |
|
1580 apply (metis Un_Diff_cancel Un_insert_left span_redundant span_zero) |
|
1581 done |
|
1582 qed |
|
1583 |
|
1584 subsection\<open>Decomposing a vector into parts in orthogonal subspaces\<close> |
|
1585 |
|
1586 text\<open>existence of orthonormal basis for a subspace.\<close> |
|
1587 |
|
1588 lemma orthogonal_spanningset_subspace: |
|
1589 fixes S :: "'a :: euclidean_space set" |
|
1590 assumes "subspace S" |
|
1591 obtains B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S" |
|
1592 proof - |
|
1593 obtain B where "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" |
|
1594 using basis_exists by blast |
|
1595 with orthogonal_extension [of "{}" B] |
|
1596 show ?thesis |
|
1597 by (metis Un_empty_left assms pairwise_empty span_superset span_subspace that) |
|
1598 qed |
|
1599 |
|
1600 lemma orthogonal_basis_subspace: |
|
1601 fixes S :: "'a :: euclidean_space set" |
|
1602 assumes "subspace S" |
|
1603 obtains B where "0 \<notin> B" "B \<subseteq> S" "pairwise orthogonal B" "independent B" |
|
1604 "card B = dim S" "span B = S" |
|
1605 proof - |
|
1606 obtain B where "B \<subseteq> S" "pairwise orthogonal B" "span B = S" |
|
1607 using assms orthogonal_spanningset_subspace by blast |
|
1608 then show ?thesis |
|
1609 apply (rule_tac B = "B - {0}" in that) |
|
1610 apply (auto simp: indep_card_eq_dim_span pairwise_subset pairwise_orthogonal_independent elim: pairwise_subset) |
|
1611 done |
|
1612 qed |
|
1613 |
|
1614 proposition orthonormal_basis_subspace: |
|
1615 fixes S :: "'a :: euclidean_space set" |
|
1616 assumes "subspace S" |
|
1617 obtains B where "B \<subseteq> S" "pairwise orthogonal B" |
|
1618 and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1" |
|
1619 and "independent B" "card B = dim S" "span B = S" |
|
1620 proof - |
|
1621 obtain B where "0 \<notin> B" "B \<subseteq> S" |
|
1622 and orth: "pairwise orthogonal B" |
|
1623 and "independent B" "card B = dim S" "span B = S" |
|
1624 by (blast intro: orthogonal_basis_subspace [OF assms]) |
|
1625 have 1: "(\<lambda>x. x /\<^sub>R norm x) ` B \<subseteq> S" |
|
1626 using \<open>span B = S\<close> span_superset span_mul by fastforce |
|
1627 have 2: "pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` B)" |
|
1628 using orth by (force simp: pairwise_def orthogonal_clauses) |
|
1629 have 3: "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` B \<Longrightarrow> norm x = 1" |
|
1630 by (metis (no_types, lifting) \<open>0 \<notin> B\<close> image_iff norm_sgn sgn_div_norm) |
|
1631 have 4: "independent ((\<lambda>x. x /\<^sub>R norm x) ` B)" |
|
1632 by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one) |
|
1633 have "inj_on (\<lambda>x. x /\<^sub>R norm x) B" |
|
1634 proof |
|
1635 fix x y |
|
1636 assume "x \<in> B" "y \<in> B" "x /\<^sub>R norm x = y /\<^sub>R norm y" |
|
1637 moreover have "\<And>i. i \<in> B \<Longrightarrow> norm (i /\<^sub>R norm i) = 1" |
|
1638 using 3 by blast |
|
1639 ultimately show "x = y" |
|
1640 by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one) |
|
1641 qed |
|
1642 then have 5: "card ((\<lambda>x. x /\<^sub>R norm x) ` B) = dim S" |
|
1643 by (metis \<open>card B = dim S\<close> card_image) |
|
1644 have 6: "span ((\<lambda>x. x /\<^sub>R norm x) ` B) = S" |
|
1645 by (metis "1" "4" "5" assms card_eq_dim independent_imp_finite span_subspace) |
|
1646 show ?thesis |
|
1647 by (rule that [OF 1 2 3 4 5 6]) |
|
1648 qed |
|
1649 |
|
1650 |
|
1651 proposition%unimportant orthogonal_to_subspace_exists_gen: |
|
1652 fixes S :: "'a :: euclidean_space set" |
|
1653 assumes "span S \<subset> span T" |
|
1654 obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y" |
|
1655 proof - |
|
1656 obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B" |
|
1657 and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1" |
|
1658 and "independent B" "card B = dim S" "span B = span S" |
|
1659 by (rule orthonormal_basis_subspace [of "span S", OF subspace_span]) |
|
1660 (auto simp: dim_span) |
|
1661 with assms obtain u where spanBT: "span B \<subseteq> span T" and "u \<notin> span B" "u \<in> span T" |
|
1662 by auto |
|
1663 obtain C where orthBC: "pairwise orthogonal (B \<union> C)" and spanBC: "span (B \<union> C) = span (B \<union> {u})" |
|
1664 by (blast intro: orthogonal_extension [OF orthB]) |
|
1665 show thesis |
|
1666 proof (cases "C \<subseteq> insert 0 B") |
|
1667 case True |
|
1668 then have "C \<subseteq> span B" |
|
1669 using span_eq |
|
1670 by (metis span_insert_0 subset_trans) |
|
1671 moreover have "u \<in> span (B \<union> C)" |
|
1672 using \<open>span (B \<union> C) = span (B \<union> {u})\<close> span_superset by force |
|
1673 ultimately show ?thesis |
|
1674 using True \<open>u \<notin> span B\<close> |
|
1675 by (metis Un_insert_left span_insert_0 sup.orderE) |
|
1676 next |
|
1677 case False |
|
1678 then obtain x where "x \<in> C" "x \<noteq> 0" "x \<notin> B" |
|
1679 by blast |
|
1680 then have "x \<in> span T" |
|
1681 by (metis (no_types, lifting) Un_insert_right Un_upper2 \<open>u \<in> span T\<close> spanBT spanBC |
|
1682 \<open>u \<in> span T\<close> insert_subset span_superset span_mono |
|
1683 span_span subsetCE subset_trans sup_bot.comm_neutral) |
|
1684 moreover have "orthogonal x y" if "y \<in> span B" for y |
|
1685 using that |
|
1686 proof (rule span_induct) |
|
1687 show "subspace {a. orthogonal x a}" |
|
1688 by (simp add: subspace_orthogonal_to_vector) |
|
1689 show "\<And>b. b \<in> B \<Longrightarrow> orthogonal x b" |
|
1690 by (metis Un_iff \<open>x \<in> C\<close> \<open>x \<notin> B\<close> orthBC pairwise_def) |
|
1691 qed |
|
1692 ultimately show ?thesis |
|
1693 using \<open>x \<noteq> 0\<close> that \<open>span B = span S\<close> by auto |
|
1694 qed |
|
1695 qed |
|
1696 |
|
1697 corollary%unimportant orthogonal_to_subspace_exists: |
|
1698 fixes S :: "'a :: euclidean_space set" |
|
1699 assumes "dim S < DIM('a)" |
|
1700 obtains x where "x \<noteq> 0" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y" |
|
1701 proof - |
|
1702 have "span S \<subset> UNIV" |
|
1703 by (metis (mono_tags) UNIV_I assms inner_eq_zero_iff less_le lowdim_subset_hyperplane |
|
1704 mem_Collect_eq top.extremum_strict top.not_eq_extremum) |
|
1705 with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis |
|
1706 by (auto simp: span_UNIV) |
|
1707 qed |
|
1708 |
|
1709 corollary%unimportant orthogonal_to_vector_exists: |
|
1710 fixes x :: "'a :: euclidean_space" |
|
1711 assumes "2 \<le> DIM('a)" |
|
1712 obtains y where "y \<noteq> 0" "orthogonal x y" |
|
1713 proof - |
|
1714 have "dim {x} < DIM('a)" |
|
1715 using assms by auto |
|
1716 then show thesis |
|
1717 by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that) |
|
1718 qed |
|
1719 |
|
1720 proposition%unimportant orthogonal_subspace_decomp_exists: |
|
1721 fixes S :: "'a :: euclidean_space set" |
|
1722 obtains y z |
|
1723 where "y \<in> span S" |
|
1724 and "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" |
|
1725 and "x = y + z" |
|
1726 proof - |
|
1727 obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T" |
|
1728 "card T = dim (span S)" "span T = span S" |
|
1729 using orthogonal_basis_subspace subspace_span by blast |
|
1730 let ?a = "\<Sum>b\<in>T. (b \<bullet> x / (b \<bullet> b)) *\<^sub>R b" |
|
1731 have orth: "orthogonal (x - ?a) w" if "w \<in> span S" for w |
|
1732 by (simp add: Gram_Schmidt_step \<open>pairwise orthogonal T\<close> \<open>span T = span S\<close> |
|
1733 orthogonal_commute that) |
|
1734 show ?thesis |
|
1735 apply (rule_tac y = "?a" and z = "x - ?a" in that) |
|
1736 apply (meson \<open>T \<subseteq> span S\<close> span_scale span_sum subsetCE) |
|
1737 apply (fact orth, simp) |
|
1738 done |
|
1739 qed |
|
1740 |
|
1741 lemma orthogonal_subspace_decomp_unique: |
|
1742 fixes S :: "'a :: euclidean_space set" |
|
1743 assumes "x + y = x' + y'" |
|
1744 and ST: "x \<in> span S" "x' \<in> span S" "y \<in> span T" "y' \<in> span T" |
|
1745 and orth: "\<And>a b. \<lbrakk>a \<in> S; b \<in> T\<rbrakk> \<Longrightarrow> orthogonal a b" |
|
1746 shows "x = x' \<and> y = y'" |
|
1747 proof - |
|
1748 have "x + y - y' = x'" |
|
1749 by (simp add: assms) |
|
1750 moreover have "\<And>a b. \<lbrakk>a \<in> span S; b \<in> span T\<rbrakk> \<Longrightarrow> orthogonal a b" |
|
1751 by (meson orth orthogonal_commute orthogonal_to_span) |
|
1752 ultimately have "0 = x' - x" |
|
1753 by (metis (full_types) add_diff_cancel_left' ST diff_right_commute orthogonal_clauses(10) orthogonal_clauses(5) orthogonal_self) |
|
1754 with assms show ?thesis by auto |
|
1755 qed |
|
1756 |
|
1757 lemma vector_in_orthogonal_spanningset: |
|
1758 fixes a :: "'a::euclidean_space" |
|
1759 obtains S where "a \<in> S" "pairwise orthogonal S" "span S = UNIV" |
|
1760 by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def |
|
1761 pairwise_orthogonal_insert span_UNIV subsetI subset_antisym) |
|
1762 |
|
1763 lemma vector_in_orthogonal_basis: |
|
1764 fixes a :: "'a::euclidean_space" |
|
1765 assumes "a \<noteq> 0" |
|
1766 obtains S where "a \<in> S" "0 \<notin> S" "pairwise orthogonal S" "independent S" "finite S" |
|
1767 "span S = UNIV" "card S = DIM('a)" |
|
1768 proof - |
|
1769 obtain S where S: "a \<in> S" "pairwise orthogonal S" "span S = UNIV" |
|
1770 using vector_in_orthogonal_spanningset . |
|
1771 show thesis |
|
1772 proof |
|
1773 show "pairwise orthogonal (S - {0})" |
|
1774 using pairwise_mono S(2) by blast |
|
1775 show "independent (S - {0})" |
|
1776 by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent) |
|
1777 show "finite (S - {0})" |
|
1778 using \<open>independent (S - {0})\<close> independent_imp_finite by blast |
|
1779 show "card (S - {0}) = DIM('a)" |
|
1780 using span_delete_0 [of S] S |
|
1781 by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span dim_UNIV) |
|
1782 qed (use S \<open>a \<noteq> 0\<close> in auto) |
|
1783 qed |
|
1784 |
|
1785 lemma vector_in_orthonormal_basis: |
|
1786 fixes a :: "'a::euclidean_space" |
|
1787 assumes "norm a = 1" |
|
1788 obtains S where "a \<in> S" "pairwise orthogonal S" "\<And>x. x \<in> S \<Longrightarrow> norm x = 1" |
|
1789 "independent S" "card S = DIM('a)" "span S = UNIV" |
|
1790 proof - |
|
1791 have "a \<noteq> 0" |
|
1792 using assms by auto |
|
1793 then obtain S where "a \<in> S" "0 \<notin> S" "finite S" |
|
1794 and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)" |
|
1795 by (metis vector_in_orthogonal_basis) |
|
1796 let ?S = "(\<lambda>x. x /\<^sub>R norm x) ` S" |
|
1797 show thesis |
|
1798 proof |
|
1799 show "a \<in> ?S" |
|
1800 using \<open>a \<in> S\<close> assms image_iff by fastforce |
|
1801 next |
|
1802 show "pairwise orthogonal ?S" |
|
1803 using \<open>pairwise orthogonal S\<close> by (auto simp: pairwise_def orthogonal_def) |
|
1804 show "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` S \<Longrightarrow> norm x = 1" |
|
1805 using \<open>0 \<notin> S\<close> by (auto simp: divide_simps) |
|
1806 then show "independent ?S" |
|
1807 by (metis \<open>pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` S)\<close> norm_zero pairwise_orthogonal_independent zero_neq_one) |
|
1808 have "inj_on (\<lambda>x. x /\<^sub>R norm x) S" |
|
1809 unfolding inj_on_def |
|
1810 by (metis (full_types) S(1) \<open>0 \<notin> S\<close> inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def) |
|
1811 then show "card ?S = DIM('a)" |
|
1812 by (simp add: card_image S) |
|
1813 show "span ?S = UNIV" |
|
1814 by (metis (no_types) \<open>0 \<notin> S\<close> \<open>finite S\<close> \<open>span S = UNIV\<close> |
|
1815 field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale |
|
1816 zero_less_norm_iff) |
|
1817 qed |
|
1818 qed |
|
1819 |
|
1820 proposition dim_orthogonal_sum: |
|
1821 fixes A :: "'a::euclidean_space set" |
|
1822 assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0" |
|
1823 shows "dim(A \<union> B) = dim A + dim B" |
|
1824 proof - |
|
1825 have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0" |
|
1826 by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms) |
|
1827 have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0" |
|
1828 using 1 by (simp add: span_induct [OF _ subspace_hyperplane]) |
|
1829 then have 0: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0" |
|
1830 by simp |
|
1831 have "dim(A \<union> B) = dim (span (A \<union> B))" |
|
1832 by (simp add: dim_span) |
|
1833 also have "span (A \<union> B) = ((\<lambda>(a, b). a + b) ` (span A \<times> span B))" |
|
1834 by (auto simp add: span_Un image_def) |
|
1835 also have "dim \<dots> = dim {x + y |x y. x \<in> span A \<and> y \<in> span B}" |
|
1836 by (auto intro!: arg_cong [where f=dim]) |
|
1837 also have "... = dim {x + y |x y. x \<in> span A \<and> y \<in> span B} + dim(span A \<inter> span B)" |
|
1838 by (auto simp: dest: 0) |
|
1839 also have "... = dim (span A) + dim (span B)" |
|
1840 by (rule dim_sums_Int) (auto simp: subspace_span) |
|
1841 also have "... = dim A + dim B" |
|
1842 by (simp add: dim_span) |
|
1843 finally show ?thesis . |
|
1844 qed |
|
1845 |
|
1846 lemma dim_subspace_orthogonal_to_vectors: |
|
1847 fixes A :: "'a::euclidean_space set" |
|
1848 assumes "subspace A" "subspace B" "A \<subseteq> B" |
|
1849 shows "dim {y \<in> B. \<forall>x \<in> A. orthogonal x y} + dim A = dim B" |
|
1850 proof - |
|
1851 have "dim (span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)) = dim (span B)" |
|
1852 proof (rule arg_cong [where f=dim, OF subset_antisym]) |
|
1853 show "span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A) \<subseteq> span B" |
|
1854 by (simp add: \<open>A \<subseteq> B\<close> Collect_restrict span_mono) |
|
1855 next |
|
1856 have *: "x \<in> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)" |
|
1857 if "x \<in> B" for x |
|
1858 proof - |
|
1859 obtain y z where "x = y + z" "y \<in> span A" and orth: "\<And>w. w \<in> span A \<Longrightarrow> orthogonal z w" |
|
1860 using orthogonal_subspace_decomp_exists [of A x] that by auto |
|
1861 have "y \<in> span B" |
|
1862 using \<open>y \<in> span A\<close> assms(3) span_mono by blast |
|
1863 then have "z \<in> {a \<in> B. \<forall>x. x \<in> A \<longrightarrow> orthogonal x a}" |
|
1864 apply simp |
|
1865 using \<open>x = y + z\<close> assms(1) assms(2) orth orthogonal_commute span_add_eq |
|
1866 span_eq_iff that by blast |
|
1867 then have z: "z \<in> span {y \<in> B. \<forall>x\<in>A. orthogonal x y}" |
|
1868 by (meson span_superset subset_iff) |
|
1869 then show ?thesis |
|
1870 apply (auto simp: span_Un image_def \<open>x = y + z\<close> \<open>y \<in> span A\<close>) |
|
1871 using \<open>y \<in> span A\<close> add.commute by blast |
|
1872 qed |
|
1873 show "span B \<subseteq> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)" |
|
1874 by (rule span_minimal) |
|
1875 (auto intro: * span_minimal simp: subspace_span) |
|
1876 qed |
|
1877 then show ?thesis |
|
1878 by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq |
|
1879 orthogonal_commute orthogonal_def) |
|
1880 qed |
|
1881 |
1213 end |
1882 end |