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.7 -  have "matrix(adjoint f) = matrix(adjoint (( *v) (matrix f)))"
     1.8 +  have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))"
     1.9      by (simp add: lf)
    1.10    also have "\<dots> = transpose(matrix f)"
    1.11      unfolding adjoint_matrix matrix_of_matrix_vector_mul
    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.102      by (simp add: const_vector_cart)
   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)