src/HOL/Analysis/Cartesian_Euclidean_Space.thy
 changeset 69064 5840724b1d71 parent 68833 fde093888c16 child 69272 15e9ed5b28fb
```     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Sep 23 21:49:31 2018 +0200
1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Sep 24 14:30:09 2018 +0200
1.3 @@ -203,7 +203,7 @@
1.4  lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
1.5    shows "matrix(adjoint f) = transpose(matrix f)"
1.6  proof%unimportant -
1.10    also have "\<dots> = transpose(matrix f)"
1.12 @@ -212,14 +212,14 @@
1.13    finally show ?thesis .
1.14  qed
1.15
1.16 -lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear (( *v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
1.17 +lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
1.18    using matrix_vector_mul_linear[of A]
1.19    by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq)
1.20
1.21  lemma%unimportant (* FIX ME needs name*)
1.22    fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
1.23 -  shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z"
1.24 -    and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)"
1.25 +  shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont ((*v) A) z"
1.26 +    and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S ((*v) A)"
1.27    by (simp_all add: linear_continuous_at linear_continuous_on)
1.28
1.29  lemma%unimportant scalar_invertible:
1.30 @@ -293,24 +293,24 @@
1.31
1.32  lemma%important norm_column_le_onorm:
1.33    fixes A :: "real^'n^'m"
1.34 -  shows "norm(column i A) \<le> onorm(( *v) A)"
1.35 +  shows "norm(column i A) \<le> onorm((*v) A)"
1.36  proof%unimportant -
1.37    have "norm (\<chi> j. A \$ j \$ i) \<le> norm (A *v axis i 1)"
1.38      by (simp add: matrix_mult_dot cart_eq_inner_axis)
1.39 -  also have "\<dots> \<le> onorm (( *v) A)"
1.40 +  also have "\<dots> \<le> onorm ((*v) A)"
1.41      using onorm [OF matrix_vector_mul_bounded_linear, of A "axis i 1"] by auto
1.42 -  finally have "norm (\<chi> j. A \$ j \$ i) \<le> onorm (( *v) A)" .
1.43 +  finally have "norm (\<chi> j. A \$ j \$ i) \<le> onorm ((*v) A)" .
1.44    then show ?thesis
1.45      unfolding column_def .
1.46  qed
1.47
1.48  lemma%important matrix_component_le_onorm:
1.49    fixes A :: "real^'n^'m"
1.50 -  shows "\<bar>A \$ i \$ j\<bar> \<le> onorm(( *v) A)"
1.51 +  shows "\<bar>A \$ i \$ j\<bar> \<le> onorm((*v) A)"
1.52  proof%unimportant -
1.53    have "\<bar>A \$ i \$ j\<bar> \<le> norm (\<chi> n. (A \$ n \$ j))"
1.54      by (metis (full_types, lifting) component_le_norm_cart vec_lambda_beta)
1.55 -  also have "\<dots> \<le> onorm (( *v) A)"
1.56 +  also have "\<dots> \<le> onorm ((*v) A)"
1.57      by (metis (no_types) column_def norm_column_le_onorm)
1.58    finally show ?thesis .
1.59  qed
1.60 @@ -322,7 +322,7 @@
1.61
1.62  lemma%important onorm_le_matrix_component_sum:
1.63    fixes A :: "real^'n^'m"
1.64 -  shows "onorm(( *v) A) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A \$ i \$ j\<bar>)"
1.65 +  shows "onorm((*v) A) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A \$ i \$ j\<bar>)"
1.66  proof%unimportant (rule onorm_le)
1.67    fix x
1.68    have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) \$ i\<bar>)"
1.69 @@ -345,7 +345,7 @@
1.70  lemma%important onorm_le_matrix_component:
1.71    fixes A :: "real^'n^'m"
1.72    assumes "\<And>i j. abs(A\$i\$j) \<le> B"
1.73 -  shows "onorm(( *v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
1.74 +  shows "onorm((*v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
1.75  proof%unimportant (rule onorm_le)
1.76    fix x :: "real^'n::_"
1.77    have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) \$ i\<bar>)"
1.78 @@ -403,13 +403,13 @@
1.79      by (auto simp: lambda_skolem Bex_def)
1.80    show ?thesis
1.81    proof
1.82 -    have "onorm (( *v) (A - B)) \<le> real CARD('m) * real CARD('n) *
1.83 +    have "onorm ((*v) (A - B)) \<le> real CARD('m) * real CARD('n) *
1.84      (e / (2 * real CARD('m) * real CARD('n)))"
1.85        apply (rule onorm_le_matrix_component)
1.86        using Bclo by (simp add: abs_minus_commute less_imp_le)
1.87      also have "\<dots> < e"
1.88        using \<open>0 < e\<close> by (simp add: divide_simps)
1.89 -    finally show "onorm (( *v) (A - B)) < e" .
1.90 +    finally show "onorm ((*v) (A - B)) < e" .
1.91    qed (use B in auto)
1.92  qed
1.93
1.94 @@ -778,7 +778,7 @@
1.95      where "finite s" "cbox (x - (\<chi> i. d)) (x + (\<chi> i. d)) = convex hull s"
1.96  proof%unimportant -
1.97    from assms obtain s where "finite s"
1.98 -    and "cbox (x - sum (( *\<^sub>R) d) Basis) (x + sum (( *\<^sub>R) d) Basis) = convex hull s"
1.99 +    and "cbox (x - sum ((*\<^sub>R) d) Basis) (x + sum ((*\<^sub>R) d) Basis) = convex hull s"
1.100      by (rule cube_convex_hull)
1.101    with that[of s] show thesis
1.103 @@ -982,11 +982,11 @@
1.104        using basis_exists [of "span(rows A)"] by metis
1.105      with span_subspace have eq: "span B = span(rows A)"
1.106        by auto
1.107 -    then have inj: "inj_on (( *v) A) (span B)"
1.108 +    then have inj: "inj_on ((*v) A) (span B)"
1.109        by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace)
1.110 -    then have ind: "independent (( *v) A ` B)"
1.111 +    then have ind: "independent ((*v) A ` B)"
1.112        by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>])
1.113 -    have "dim (span (rows A)) \<le> card (( *v) A ` B)"
1.114 +    have "dim (span (rows A)) \<le> card ((*v) A ` B)"
1.115        unfolding B(2)[symmetric]
1.116        using inj
1.117        by (auto simp: card_image inj_on_subset span_superset)
1.118 @@ -1017,7 +1017,7 @@
1.119
1.120  lemma%unimportant columns_image_basis:
1.121    fixes A :: "real^'n^'m"
1.122 -  shows "columns A = ( *v) A ` (range (\<lambda>i. axis i 1))"
1.123 +  shows "columns A = (*v) A ` (range (\<lambda>i. axis i 1))"
1.124    by (force simp: columns_def matrix_vector_mult_basis [symmetric])
1.125
1.126  lemma%important rank_dim_range:
1.127 @@ -1025,7 +1025,7 @@
1.128    shows "rank A = dim(range (\<lambda>x. A *v x))"
1.129    unfolding column_rank_def
1.130  proof%unimportant (rule span_eq_dim)
1.131 -  have "span (columns A) \<subseteq> span (range (( *v) A))" (is "?l \<subseteq> ?r")
1.132 +  have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r")
1.133      by (simp add: columns_image_basis image_subsetI span_mono)
1.134    then show "?l = ?r"
1.135      by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace
1.136 @@ -1040,13 +1040,13 @@
1.137
1.138  lemma%unimportant full_rank_injective:
1.139    fixes A :: "real^'n^'m"
1.140 -  shows "rank A = CARD('n) \<longleftrightarrow> inj (( *v) A)"
1.141 +  shows "rank A = CARD('n) \<longleftrightarrow> inj ((*v) A)"
1.142    by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def
1.143        dim_eq_full [symmetric] card_cart_basis vec.dimension_def)
1.144
1.145  lemma%unimportant full_rank_surjective:
1.146    fixes A :: "real^'n^'m"
1.147 -  shows "rank A = CARD('m) \<longleftrightarrow> surj (( *v) A)"
1.148 +  shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)"
1.149    by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
1.150                  matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
1.151
1.152 @@ -1055,7 +1055,7 @@
1.153
1.154  lemma%unimportant less_rank_noninjective:
1.155    fixes A :: "real^'n^'m"
1.156 -  shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj (( *v) A)"
1.157 +  shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)"
1.158  using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
1.159
1.160  lemma%unimportant matrix_nonfull_linear_equations_eq:
1.161 @@ -1071,7 +1071,7 @@
1.162    fixes A :: "real^'n^'m" and B :: "real^'p^'n"
1.163    shows "rank(A ** B) \<le> rank B"
1.164  proof%unimportant -
1.165 -  have "rank(A ** B) \<le> dim (( *v) A ` range (( *v) B))"
1.166 +  have "rank(A ** B) \<le> dim ((*v) A ` range ((*v) B))"
1.167      by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc)
1.168    also have "\<dots> \<le> rank B"
1.169      by (simp add: rank_dim_range dim_image_le)
1.170 @@ -1137,7 +1137,7 @@
1.171
1.172  lemma has_derivative_vector_1:
1.173    assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
1.174 -  shows "((\<lambda>x. vec (g (x \$ 1))) has_derivative ( *\<^sub>R) (g' a))
1.175 +  shows "((\<lambda>x. vec (g (x \$ 1))) has_derivative (*\<^sub>R) (g' a))
1.176           (at ((vec a)::real^1) within vec ` S)"
1.177      using der_g
1.178      apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
```