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