src/HOL/Analysis/Linear_Algebra.thy
changeset 67982 7643b005b29a
parent 67962 0acdcd8f4ba1
child 68058 69715dfdc286
child 68072 493b818e8e10
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sat Apr 14 20:19:52 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Sun Apr 15 13:57:00 2018 +0100
     1.3 @@ -1962,15 +1962,43 @@
     1.4  lemma linear_bounded_pos:
     1.5    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
     1.6    assumes lf: "linear f"
     1.7 -  shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
     1.8 + obtains B where "B > 0" "\<And>x. norm (f x) \<le> B * norm x"
     1.9  proof -
    1.10    have "\<exists>B > 0. \<forall>x. norm (f x) \<le> norm x * B"
    1.11      using lf unfolding linear_conv_bounded_linear
    1.12      by (rule bounded_linear.pos_bounded)
    1.13 -  then show ?thesis
    1.14 -    by (simp only: mult.commute)
    1.15 +  with that show ?thesis
    1.16 +    by (auto simp: mult.commute)
    1.17  qed
    1.18  
    1.19 +lemma linear_invertible_bounded_below_pos:
    1.20 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
    1.21 +  assumes "linear f" "linear g" "g \<circ> f = id"
    1.22 +  obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
    1.23 +proof -
    1.24 +  obtain B where "B > 0" and B: "\<And>x. norm (g x) \<le> B * norm x"
    1.25 +    using linear_bounded_pos [OF \<open>linear g\<close>] by blast
    1.26 +  show thesis
    1.27 +  proof
    1.28 +    show "0 < 1/B"
    1.29 +      by (simp add: \<open>B > 0\<close>)
    1.30 +    show "1/B * norm x \<le> norm (f x)" for x
    1.31 +    proof -
    1.32 +      have "1/B * norm x = 1/B * norm (g (f x))"
    1.33 +        using assms by (simp add: pointfree_idE)
    1.34 +      also have "\<dots> \<le> norm (f x)"
    1.35 +        using B [of "f x"] by (simp add: \<open>B > 0\<close> mult.commute pos_divide_le_eq)
    1.36 +      finally show ?thesis .
    1.37 +    qed
    1.38 +  qed
    1.39 +qed
    1.40 +
    1.41 +lemma linear_inj_bounded_below_pos:
    1.42 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
    1.43 +  assumes "linear f" "inj f"
    1.44 +  obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
    1.45 +  using linear_injective_left_inverse [OF assms] linear_invertible_bounded_below_pos assms by blast
    1.46 +
    1.47  lemma bounded_linearI':
    1.48    fixes f ::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
    1.49    assumes "\<And>x y. f (x + y) = f x + f y"