1564 |
1560 |
1565 lemma linear_bounded: |
1561 lemma linear_bounded: |
1566 fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
1562 fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
1567 assumes lf: "linear f" |
1563 assumes lf: "linear f" |
1568 shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x" |
1564 shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x" |
1569 proof - |
1565 proof |
1570 let ?B = "\<Sum>b\<in>Basis. norm (f b)" |
1566 let ?B = "\<Sum>b\<in>Basis. norm (f b)" |
1571 { |
1567 show "\<forall>x. norm (f x) \<le> ?B * norm x" |
|
1568 proof |
1572 fix x :: 'a |
1569 fix x :: 'a |
1573 let ?g = "\<lambda>b. (x \<bullet> b) *\<^sub>R f b" |
1570 let ?g = "\<lambda>b. (x \<bullet> b) *\<^sub>R f b" |
1574 have "norm (f x) = norm (f (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b))" |
1571 have "norm (f x) = norm (f (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b))" |
1575 unfolding euclidean_representation .. |
1572 unfolding euclidean_representation .. |
1576 also have "\<dots> = norm (setsum ?g Basis)" |
1573 also have "\<dots> = norm (setsum ?g Basis)" |
1577 using linear_setsum[OF lf finite_Basis, of "\<lambda>b. (x \<bullet> b) *\<^sub>R b", unfolded o_def] linear_cmul[OF lf] |
1574 by (simp add: linear_setsum [OF lf] linear_cmul [OF lf]) |
1578 by auto |
|
1579 finally have th0: "norm (f x) = norm (setsum ?g Basis)" . |
1575 finally have th0: "norm (f x) = norm (setsum ?g Basis)" . |
1580 { |
1576 have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x" |
|
1577 proof |
1581 fix i :: 'a |
1578 fix i :: 'a |
1582 assume i: "i \<in> Basis" |
1579 assume i: "i \<in> Basis" |
1583 from Basis_le_norm[OF i, of x] |
1580 from Basis_le_norm[OF i, of x] |
1584 have "norm (?g i) \<le> norm (f i) * norm x" |
1581 show "norm (?g i) \<le> norm (f i) * norm x" |
1585 unfolding norm_scaleR |
1582 unfolding norm_scaleR |
1586 apply (subst mult_commute) |
1583 apply (subst mult_commute) |
1587 apply (rule mult_mono) |
1584 apply (rule mult_mono) |
1588 apply (auto simp add: field_simps) |
1585 apply (auto simp add: field_simps) |
1589 done |
1586 done |
1590 } |
1587 qed |
1591 then have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x" |
|
1592 by metis |
|
1593 from setsum_norm_le[of _ ?g, OF th] |
1588 from setsum_norm_le[of _ ?g, OF th] |
1594 have "norm (f x) \<le> ?B * norm x" |
1589 show "norm (f x) \<le> ?B * norm x" |
1595 unfolding th0 setsum_left_distrib by metis |
1590 unfolding th0 setsum_left_distrib by metis |
1596 } |
1591 qed |
1597 then show ?thesis by blast |
|
1598 qed |
|
1599 |
|
1600 lemma linear_bounded_pos: |
|
1601 fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
|
1602 assumes lf: "linear f" |
|
1603 shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x" |
|
1604 proof - |
|
1605 from linear_bounded[OF lf] obtain B where |
|
1606 B: "\<forall>x. norm (f x) \<le> B * norm x" by blast |
|
1607 let ?K = "\<bar>B\<bar> + 1" |
|
1608 have Kp: "?K > 0" by arith |
|
1609 { |
|
1610 assume C: "B < 0" |
|
1611 def One \<equiv> "\<Sum>Basis ::'a" |
|
1612 then have "One \<noteq> 0" |
|
1613 unfolding euclidean_eq_iff[where 'a='a] |
|
1614 by (simp add: inner_setsum_left inner_Basis setsum_cases) |
|
1615 then have "norm One > 0" by auto |
|
1616 with C have "B * norm One < 0" |
|
1617 by (simp add: mult_less_0_iff) |
|
1618 with B[rule_format, of One] norm_ge_zero[of "f One"] |
|
1619 have False by simp |
|
1620 } |
|
1621 then have Bp: "B \<ge> 0" |
|
1622 by (metis not_leE) |
|
1623 { |
|
1624 fix x::"'a" |
|
1625 have "norm (f x) \<le> ?K * norm x" |
|
1626 using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp |
|
1627 apply (auto simp add: field_simps split add: abs_split) |
|
1628 apply (erule order_trans, simp) |
|
1629 done |
|
1630 } |
|
1631 then show ?thesis |
|
1632 using Kp by blast |
|
1633 qed |
1592 qed |
1634 |
1593 |
1635 lemma linear_conv_bounded_linear: |
1594 lemma linear_conv_bounded_linear: |
1636 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
1595 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
1637 shows "linear f \<longleftrightarrow> bounded_linear f" |
1596 shows "linear f \<longleftrightarrow> bounded_linear f" |
1638 proof |
1597 proof |
1639 assume "linear f" |
1598 assume "linear f" |
|
1599 then interpret f: linear f . |
1640 show "bounded_linear f" |
1600 show "bounded_linear f" |
1641 proof |
1601 proof |
1642 fix x y |
|
1643 show "f (x + y) = f x + f y" |
|
1644 using `linear f` unfolding linear_iff by simp |
|
1645 next |
|
1646 fix r x |
|
1647 show "f (scaleR r x) = scaleR r (f x)" |
|
1648 using `linear f` unfolding linear_iff by simp |
|
1649 next |
|
1650 have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x" |
1602 have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x" |
1651 using `linear f` by (rule linear_bounded) |
1603 using `linear f` by (rule linear_bounded) |
1652 then show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K" |
1604 then show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K" |
1653 by (simp add: mult_commute) |
1605 by (simp add: mult_commute) |
1654 qed |
1606 qed |
1655 next |
1607 next |
1656 assume "bounded_linear f" |
1608 assume "bounded_linear f" |
1657 then interpret f: bounded_linear f . |
1609 then interpret f: bounded_linear f . |
1658 show "linear f" by (simp add: f.add f.scaleR linear_iff) |
1610 show "linear f" .. |
|
1611 qed |
|
1612 |
|
1613 lemma linear_bounded_pos: |
|
1614 fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
|
1615 assumes lf: "linear f" |
|
1616 shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x" |
|
1617 proof - |
|
1618 have "\<exists>B > 0. \<forall>x. norm (f x) \<le> norm x * B" |
|
1619 using lf unfolding linear_conv_bounded_linear |
|
1620 by (rule bounded_linear.pos_bounded) |
|
1621 then show ?thesis |
|
1622 by (simp only: mult_commute) |
1659 qed |
1623 qed |
1660 |
1624 |
1661 lemma bounded_linearI': |
1625 lemma bounded_linearI': |
1662 fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
1626 fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
1663 assumes "\<And>x y. f (x + y) = f x + f y" |
1627 assumes "\<And>x y. f (x + y) = f x + f y" |
1690 apply (rule mult_mono) |
1654 apply (rule mult_mono) |
1691 apply (auto simp add: zero_le_mult_iff Basis_le_norm) |
1655 apply (auto simp add: zero_le_mult_iff Basis_le_norm) |
1692 apply (rule mult_mono) |
1656 apply (rule mult_mono) |
1693 apply (auto simp add: zero_le_mult_iff Basis_le_norm) |
1657 apply (auto simp add: zero_le_mult_iff Basis_le_norm) |
1694 done |
1658 done |
1695 qed |
|
1696 |
|
1697 lemma bilinear_bounded_pos: |
|
1698 fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector" |
|
1699 assumes bh: "bilinear h" |
|
1700 shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y" |
|
1701 proof - |
|
1702 from bilinear_bounded[OF bh] obtain B where |
|
1703 B: "\<forall>x y. norm (h x y) \<le> B * norm x * norm y" by blast |
|
1704 let ?K = "\<bar>B\<bar> + 1" |
|
1705 have Kp: "?K > 0" by arith |
|
1706 have KB: "B < ?K" by arith |
|
1707 { |
|
1708 fix x :: 'a |
|
1709 fix y :: 'b |
|
1710 from KB Kp have "B * norm x * norm y \<le> ?K * norm x * norm y" |
|
1711 apply - |
|
1712 apply (rule mult_right_mono, rule mult_right_mono) |
|
1713 apply auto |
|
1714 done |
|
1715 then have "norm (h x y) \<le> ?K * norm x * norm y" |
|
1716 using B[rule_format, of x y] by simp |
|
1717 } |
|
1718 with Kp show ?thesis by blast |
|
1719 qed |
1659 qed |
1720 |
1660 |
1721 lemma bilinear_conv_bounded_bilinear: |
1661 lemma bilinear_conv_bounded_bilinear: |
1722 fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector" |
1662 fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector" |
1723 shows "bilinear h \<longleftrightarrow> bounded_bilinear h" |
1663 shows "bilinear h \<longleftrightarrow> bounded_bilinear h" |