src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
 author huffman Thu Aug 11 09:11:15 2011 -0700 (2011-08-11) changeset 44165 d26a45f3c835 parent 44140 2c10c35dd4be child 44166 d12d89a66742 permissions -rw-r--r--
remove lemma stupid_ext
```     1
```
```     2 header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}
```
```     3
```
```     4 theory Cartesian_Euclidean_Space
```
```     5 imports Finite_Cartesian_Product Integration
```
```     6 begin
```
```     7
```
```     8 lemma delta_mult_idempotent:
```
```     9   "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto)
```
```    10
```
```    11 lemma setsum_Plus:
```
```    12   "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow>
```
```    13     (\<Sum>x\<in>A <+> B. g x) = (\<Sum>x\<in>A. g (Inl x)) + (\<Sum>x\<in>B. g (Inr x))"
```
```    14   unfolding Plus_def
```
```    15   by (subst setsum_Un_disjoint, auto simp add: setsum_reindex)
```
```    16
```
```    17 lemma setsum_UNIV_sum:
```
```    18   fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
```
```    19   shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))"
```
```    20   apply (subst UNIV_Plus_UNIV [symmetric])
```
```    21   apply (rule setsum_Plus [OF finite finite])
```
```    22   done
```
```    23
```
```    24 lemma setsum_mult_product:
```
```    25   "setsum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"
```
```    26   unfolding sumr_group[of h B A, unfolded atLeast0LessThan, symmetric]
```
```    27 proof (rule setsum_cong, simp, rule setsum_reindex_cong)
```
```    28   fix i show "inj_on (\<lambda>j. j + i * B) {..<B}" by (auto intro!: inj_onI)
```
```    29   show "{i * B..<i * B + B} = (\<lambda>j. j + i * B) ` {..<B}"
```
```    30   proof safe
```
```    31     fix j assume "j \<in> {i * B..<i * B + B}"
```
```    32     thus "j \<in> (\<lambda>j. j + i * B) ` {..<B}"
```
```    33       by (auto intro!: image_eqI[of _ _ "j - i * B"])
```
```    34   qed simp
```
```    35 qed simp
```
```    36
```
```    37 subsection{* Basic componentwise operations on vectors. *}
```
```    38
```
```    39 instantiation vec :: (times, finite) times
```
```    40 begin
```
```    41   definition "op * \<equiv> (\<lambda> x y.  (\<chi> i. (x\$i) * (y\$i)))"
```
```    42   instance ..
```
```    43 end
```
```    44
```
```    45 instantiation vec :: (one, finite) one
```
```    46 begin
```
```    47   definition "1 \<equiv> (\<chi> i. 1)"
```
```    48   instance ..
```
```    49 end
```
```    50
```
```    51 instantiation vec :: (ord, finite) ord
```
```    52 begin
```
```    53   definition "x \<le> y \<longleftrightarrow> (\<forall>i. x\$i \<le> y\$i)"
```
```    54   definition "x < y \<longleftrightarrow> (\<forall>i. x\$i < y\$i)"
```
```    55   instance ..
```
```    56 end
```
```    57
```
```    58 text{* The ordering on one-dimensional vectors is linear. *}
```
```    59
```
```    60 class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
```
```    61 begin
```
```    62   subclass finite
```
```    63   proof from UNIV_one show "finite (UNIV :: 'a set)"
```
```    64       by (auto intro!: card_ge_0_finite) qed
```
```    65 end
```
```    66
```
```    67 instantiation vec :: (linorder,cart_one) linorder begin
```
```    68 instance proof
```
```    69   guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+
```
```    70   hence *:"UNIV = {a}" by auto
```
```    71   have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P a" unfolding * by auto hence all:"\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a" by auto
```
```    72   fix x y z::"'a^'b::cart_one" note * = less_eq_vec_def less_vec_def all vec_eq_iff
```
```    73   show "x\<le>x" "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" "x\<le>y \<or> y\<le>x" unfolding * by(auto simp only:field_simps)
```
```    74   { assume "x\<le>y" "y\<le>z" thus "x\<le>z" unfolding * by(auto simp only:field_simps) }
```
```    75   { assume "x\<le>y" "y\<le>x" thus "x=y" unfolding * by(auto simp only:field_simps) }
```
```    76 qed end
```
```    77
```
```    78 text{* Constant Vectors *}
```
```    79
```
```    80 definition "vec x = (\<chi> i. x)"
```
```    81
```
```    82 text{* Also the scalar-vector multiplication. *}
```
```    83
```
```    84 definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
```
```    85   where "c *s x = (\<chi> i. c * (x\$i))"
```
```    86
```
```    87 subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}
```
```    88
```
```    89 method_setup vector = {*
```
```    90 let
```
```    91   val ss1 = HOL_basic_ss addsimps [@{thm setsum_addf} RS sym,
```
```    92   @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib},
```
```    93   @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]
```
```    94   val ss2 = @{simpset} addsimps
```
```    95              [@{thm plus_vec_def}, @{thm times_vec_def},
```
```    96               @{thm minus_vec_def}, @{thm uminus_vec_def},
```
```    97               @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def},
```
```    98               @{thm scaleR_vec_def},
```
```    99               @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}]
```
```   100  fun vector_arith_tac ths =
```
```   101    simp_tac ss1
```
```   102    THEN' (fn i => rtac @{thm setsum_cong2} i
```
```   103          ORELSE rtac @{thm setsum_0'} i
```
```   104          ORELSE simp_tac (HOL_basic_ss addsimps [@{thm vec_eq_iff}]) i)
```
```   105    (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
```
```   106    THEN' asm_full_simp_tac (ss2 addsimps ths)
```
```   107  in
```
```   108   Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))
```
```   109  end
```
```   110 *} "lift trivial vector statements to real arith statements"
```
```   111
```
```   112 lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def)
```
```   113 lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def)
```
```   114
```
```   115 lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
```
```   116
```
```   117 lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
```
```   118
```
```   119 lemma vec_add: "vec(x + y) = vec x + vec y"  by (vector vec_def)
```
```   120 lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)
```
```   121 lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def)
```
```   122 lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
```
```   123
```
```   124 lemma vec_setsum: assumes fS: "finite S"
```
```   125   shows "vec(setsum f S) = setsum (vec o f) S"
```
```   126   apply (induct rule: finite_induct[OF fS])
```
```   127   apply (simp)
```
```   128   apply (auto simp add: vec_add)
```
```   129   done
```
```   130
```
```   131 text{* Obvious "component-pushing". *}
```
```   132
```
```   133 lemma vec_component [simp]: "vec x \$ i = x"
```
```   134   by (vector vec_def)
```
```   135
```
```   136 lemma vector_mult_component [simp]: "(x * y)\$i = x\$i * y\$i"
```
```   137   by vector
```
```   138
```
```   139 lemma vector_smult_component [simp]: "(c *s y)\$i = c * (y\$i)"
```
```   140   by vector
```
```   141
```
```   142 lemma cond_component: "(if b then x else y)\$i = (if b then x\$i else y\$i)" by vector
```
```   143
```
```   144 lemmas vector_component =
```
```   145   vec_component vector_add_component vector_mult_component
```
```   146   vector_smult_component vector_minus_component vector_uminus_component
```
```   147   vector_scaleR_component cond_component
```
```   148
```
```   149 subsection {* Some frequently useful arithmetic lemmas over vectors. *}
```
```   150
```
```   151 instance vec :: (semigroup_mult, finite) semigroup_mult
```
```   152   by default (vector mult_assoc)
```
```   153
```
```   154 instance vec :: (monoid_mult, finite) monoid_mult
```
```   155   by default vector+
```
```   156
```
```   157 instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult
```
```   158   by default (vector mult_commute)
```
```   159
```
```   160 instance vec :: (ab_semigroup_idem_mult, finite) ab_semigroup_idem_mult
```
```   161   by default (vector mult_idem)
```
```   162
```
```   163 instance vec :: (comm_monoid_mult, finite) comm_monoid_mult
```
```   164   by default vector
```
```   165
```
```   166 instance vec :: (semiring, finite) semiring
```
```   167   by default (vector field_simps)+
```
```   168
```
```   169 instance vec :: (semiring_0, finite) semiring_0
```
```   170   by default (vector field_simps)+
```
```   171 instance vec :: (semiring_1, finite) semiring_1
```
```   172   by default vector
```
```   173 instance vec :: (comm_semiring, finite) comm_semiring
```
```   174   by default (vector field_simps)+
```
```   175
```
```   176 instance vec :: (comm_semiring_0, finite) comm_semiring_0 ..
```
```   177 instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
```
```   178 instance vec :: (semiring_0_cancel, finite) semiring_0_cancel ..
```
```   179 instance vec :: (comm_semiring_0_cancel, finite) comm_semiring_0_cancel ..
```
```   180 instance vec :: (ring, finite) ring ..
```
```   181 instance vec :: (semiring_1_cancel, finite) semiring_1_cancel ..
```
```   182 instance vec :: (comm_semiring_1, finite) comm_semiring_1 ..
```
```   183
```
```   184 instance vec :: (ring_1, finite) ring_1 ..
```
```   185
```
```   186 instance vec :: (real_algebra, finite) real_algebra
```
```   187   apply intro_classes
```
```   188   apply (simp_all add: vec_eq_iff)
```
```   189   done
```
```   190
```
```   191 instance vec :: (real_algebra_1, finite) real_algebra_1 ..
```
```   192
```
```   193 lemma of_nat_index:
```
```   194   "(of_nat n :: 'a::semiring_1 ^'n)\$i = of_nat n"
```
```   195   apply (induct n)
```
```   196   apply vector
```
```   197   apply vector
```
```   198   done
```
```   199
```
```   200 lemma one_index[simp]:
```
```   201   "(1 :: 'a::one ^'n)\$i = 1" by vector
```
```   202
```
```   203 instance vec :: (semiring_char_0, finite) semiring_char_0
```
```   204 proof
```
```   205   fix m n :: nat
```
```   206   show "inj (of_nat :: nat \<Rightarrow> 'a ^ 'b)"
```
```   207     by (auto intro!: injI simp add: vec_eq_iff of_nat_index)
```
```   208 qed
```
```   209
```
```   210 instance vec :: (comm_ring_1, finite) comm_ring_1 ..
```
```   211 instance vec :: (ring_char_0, finite) ring_char_0 ..
```
```   212
```
```   213 lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
```
```   214   by (vector mult_assoc)
```
```   215 lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x"
```
```   216   by (vector field_simps)
```
```   217 lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y"
```
```   218   by (vector field_simps)
```
```   219 lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector
```
```   220 lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector
```
```   221 lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y"
```
```   222   by (vector field_simps)
```
```   223 lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector
```
```   224 lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector
```
```   225 lemma vector_sneg_minus1: "-x = (- (1::'a::ring_1)) *s x" by vector
```
```   226 lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector
```
```   227 lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x"
```
```   228   by (vector field_simps)
```
```   229
```
```   230 lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
```
```   231   by (simp add: vec_eq_iff)
```
```   232
```
```   233 lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
```
```   234 lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
```
```   235   by vector
```
```   236 lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
```
```   237   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)
```
```   238 lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
```
```   239   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
```
```   240 lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"
```
```   241   by (metis vector_mul_lcancel)
```
```   242 lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
```
```   243   by (metis vector_mul_rcancel)
```
```   244
```
```   245 lemma component_le_norm_cart: "\<bar>x\$i\<bar> <= norm x"
```
```   246   apply (simp add: norm_vec_def)
```
```   247   apply (rule member_le_setL2, simp_all)
```
```   248   done
```
```   249
```
```   250 lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x\$i\<bar> <= e"
```
```   251   by (metis component_le_norm_cart order_trans)
```
```   252
```
```   253 lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x\$i\<bar> < e"
```
```   254   by (metis component_le_norm_cart basic_trans_rules(21))
```
```   255
```
```   256 lemma norm_le_l1_cart: "norm x <= setsum(\<lambda>i. \<bar>x\$i\<bar>) UNIV"
```
```   257   by (simp add: norm_vec_def setL2_le_setsum)
```
```   258
```
```   259 lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"
```
```   260   unfolding scaleR_vec_def vector_scalar_mult_def by simp
```
```   261
```
```   262 lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
```
```   263   unfolding dist_norm scalar_mult_eq_scaleR
```
```   264   unfolding scaleR_right_diff_distrib[symmetric] by simp
```
```   265
```
```   266 lemma setsum_component [simp]:
```
```   267   fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"
```
```   268   shows "(setsum f S)\$i = setsum (\<lambda>x. (f x)\$i) S"
```
```   269   by (cases "finite S", induct S set: finite, simp_all)
```
```   270
```
```   271 lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)\$i ) S)"
```
```   272   by (simp add: vec_eq_iff)
```
```   273
```
```   274 lemma setsum_cmul:
```
```   275   fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n"
```
```   276   shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"
```
```   277   by (simp add: vec_eq_iff setsum_right_distrib)
```
```   278
```
```   279 (* TODO: use setsum_norm_allsubsets_bound *)
```
```   280 lemma setsum_norm_allsubsets_bound_cart:
```
```   281   fixes f:: "'a \<Rightarrow> real ^'n"
```
```   282   assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
```
```   283   shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"
```
```   284 proof-
```
```   285   let ?d = "real CARD('n)"
```
```   286   let ?nf = "\<lambda>x. norm (f x)"
```
```   287   let ?U = "UNIV :: 'n set"
```
```   288   have th0: "setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x \$ i\<bar>) ?U) P = setsum (\<lambda>i. setsum (\<lambda>x. \<bar>f x \$ i\<bar>) P) ?U"
```
```   289     by (rule setsum_commute)
```
```   290   have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def)
```
```   291   have "setsum ?nf P \<le> setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x \$ i\<bar>) ?U) P"
```
```   292     apply (rule setsum_mono)    by (rule norm_le_l1_cart)
```
```   293   also have "\<dots> \<le> 2 * ?d * e"
```
```   294     unfolding th0 th1
```
```   295   proof(rule setsum_bounded)
```
```   296     fix i assume i: "i \<in> ?U"
```
```   297     let ?Pp = "{x. x\<in> P \<and> f x \$ i \<ge> 0}"
```
```   298     let ?Pn = "{x. x \<in> P \<and> f x \$ i < 0}"
```
```   299     have thp: "P = ?Pp \<union> ?Pn" by auto
```
```   300     have thp0: "?Pp \<inter> ?Pn ={}" by auto
```
```   301     have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
```
```   302     have Ppe:"setsum (\<lambda>x. \<bar>f x \$ i\<bar>) ?Pp \<le> e"
```
```   303       using component_le_norm_cart[of "setsum (\<lambda>x. f x) ?Pp" i]  fPs[OF PpP]
```
```   304       by (auto intro: abs_le_D1)
```
```   305     have Pne: "setsum (\<lambda>x. \<bar>f x \$ i\<bar>) ?Pn \<le> e"
```
```   306       using component_le_norm_cart[of "setsum (\<lambda>x. - f x) ?Pn" i]  fPs[OF PnP]
```
```   307       by (auto simp add: setsum_negf intro: abs_le_D1)
```
```   308     have "setsum (\<lambda>x. \<bar>f x \$ i\<bar>) P = setsum (\<lambda>x. \<bar>f x \$ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x \$ i\<bar>) ?Pn"
```
```   309       apply (subst thp)
```
```   310       apply (rule setsum_Un_zero)
```
```   311       using fP thp0 by auto
```
```   312     also have "\<dots> \<le> 2*e" using Pne Ppe by arith
```
```   313     finally show "setsum (\<lambda>x. \<bar>f x \$ i\<bar>) P \<le> 2*e" .
```
```   314   qed
```
```   315   finally show ?thesis .
```
```   316 qed
```
```   317
```
```   318 lemma if_distr: "(if P then f else g) \$ i = (if P then f \$ i else g \$ i)" by simp
```
```   319
```
```   320 lemma split_dimensions'[consumes 1]:
```
```   321   assumes "k < DIM('a::euclidean_space^'b)"
```
```   322   obtains i j where "i < CARD('b::finite)" and "j < DIM('a::euclidean_space)" and "k = j + i * DIM('a::euclidean_space)"
```
```   323 using split_times_into_modulo[OF assms[simplified]] .
```
```   324
```
```   325 lemma cart_euclidean_bound[intro]:
```
```   326   assumes j:"j < DIM('a::euclidean_space)"
```
```   327   shows "j + \<pi>' (i::'b::finite) * DIM('a) < CARD('b) * DIM('a::euclidean_space)"
```
```   328   using linear_less_than_times[OF pi'_range j, of i] .
```
```   329
```
```   330 lemma (in euclidean_space) forall_CARD_DIM:
```
```   331   "(\<forall>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<forall>(i::'b::finite) j. j<DIM('a) \<longrightarrow> P (j + \<pi>' i * DIM('a)))"
```
```   332    (is "?l \<longleftrightarrow> ?r")
```
```   333 proof (safe elim!: split_times_into_modulo)
```
```   334   fix i :: 'b and j assume "j < DIM('a)"
```
```   335   note linear_less_than_times[OF pi'_range[of i] this]
```
```   336   moreover assume "?l"
```
```   337   ultimately show "P (j + \<pi>' i * DIM('a))" by auto
```
```   338 next
```
```   339   fix i j assume "i < CARD('b)" "j < DIM('a)" and "?r"
```
```   340   from `?r`[rule_format, OF `j < DIM('a)`, of "\<pi> i"] `i < CARD('b)`
```
```   341   show "P (j + i * DIM('a))" by simp
```
```   342 qed
```
```   343
```
```   344 lemma (in euclidean_space) exists_CARD_DIM:
```
```   345   "(\<exists>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<exists>i::'b::finite. \<exists>j<DIM('a). P (j + \<pi>' i * DIM('a)))"
```
```   346   using forall_CARD_DIM[where 'b='b, of "\<lambda>x. \<not> P x"] by blast
```
```   347
```
```   348 lemma forall_CARD:
```
```   349   "(\<forall>i<CARD('b). P i) \<longleftrightarrow> (\<forall>i::'b::finite. P (\<pi>' i))"
```
```   350   using forall_CARD_DIM[where 'a=real, of P] by simp
```
```   351
```
```   352 lemma exists_CARD:
```
```   353   "(\<exists>i<CARD('b). P i) \<longleftrightarrow> (\<exists>i::'b::finite. P (\<pi>' i))"
```
```   354   using exists_CARD_DIM[where 'a=real, of P] by simp
```
```   355
```
```   356 lemmas cart_simps = forall_CARD_DIM exists_CARD_DIM forall_CARD exists_CARD
```
```   357
```
```   358 lemma cart_euclidean_nth[simp]:
```
```   359   fixes x :: "('a::euclidean_space, 'b::finite) vec"
```
```   360   assumes j:"j < DIM('a)"
```
```   361   shows "x \$\$ (j + \<pi>' i * DIM('a)) = x \$ i \$\$ j"
```
```   362   unfolding euclidean_component_def inner_vec_def basis_eq_pi'[OF j] if_distrib cond_application_beta
```
```   363   by (simp add: setsum_cases)
```
```   364
```
```   365 lemma real_euclidean_nth:
```
```   366   fixes x :: "real^'n"
```
```   367   shows "x \$\$ \<pi>' i = (x \$ i :: real)"
```
```   368   using cart_euclidean_nth[where 'a=real, of 0 x i] by simp
```
```   369
```
```   370 lemmas nth_conv_component = real_euclidean_nth[symmetric]
```
```   371
```
```   372 lemma mult_split_eq:
```
```   373   fixes A :: nat assumes "x < A" "y < A"
```
```   374   shows "x + i * A = y + j * A \<longleftrightarrow> x = y \<and> i = j"
```
```   375 proof
```
```   376   assume *: "x + i * A = y + j * A"
```
```   377   { fix x y i j assume "i < j" "x < A" and *: "x + i * A = y + j * A"
```
```   378     hence "x + i * A < Suc i * A" using `x < A` by simp
```
```   379     also have "\<dots> \<le> j * A" using `i < j` unfolding mult_le_cancel2 by simp
```
```   380     also have "\<dots> \<le> y + j * A" by simp
```
```   381     finally have "i = j" using * by simp }
```
```   382   note eq = this
```
```   383
```
```   384   have "i = j"
```
```   385   proof (cases rule: linorder_cases)
```
```   386     assume "i < j" from eq[OF this `x < A` *] show "i = j" by simp
```
```   387   next
```
```   388     assume "j < i" from eq[OF this `y < A` *[symmetric]] show "i = j" by simp
```
```   389   qed simp
```
```   390   thus "x = y \<and> i = j" using * by simp
```
```   391 qed simp
```
```   392
```
```   393 instance vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
```
```   394 proof
```
```   395   fix x y::"'a^'b"
```
```   396   show "(x \<le> y) = (\<forall>i<DIM(('a, 'b) vec). x \$\$ i \<le> y \$\$ i)"
```
```   397     unfolding less_eq_vec_def apply(subst eucl_le) by (simp add: cart_simps)
```
```   398   show"(x < y) = (\<forall>i<DIM(('a, 'b) vec). x \$\$ i < y \$\$ i)"
```
```   399     unfolding less_vec_def apply(subst eucl_less) by (simp add: cart_simps)
```
```   400 qed
```
```   401
```
```   402 subsection{* Basis vectors in coordinate directions. *}
```
```   403
```
```   404 definition "cart_basis k = (\<chi> i. if i = k then 1 else 0)"
```
```   405
```
```   406 lemma basis_component [simp]: "cart_basis k \$ i = (if k=i then 1 else 0)"
```
```   407   unfolding cart_basis_def by simp
```
```   408
```
```   409 lemma norm_basis[simp]:
```
```   410   shows "norm (cart_basis k :: real ^'n) = 1"
```
```   411   apply (simp add: cart_basis_def norm_eq_sqrt_inner) unfolding inner_vec_def
```
```   412   apply (vector delta_mult_idempotent)
```
```   413   using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"] by auto
```
```   414
```
```   415 lemma norm_basis_1: "norm(cart_basis 1 :: real ^'n::{finite,one}) = 1"
```
```   416   by (rule norm_basis)
```
```   417
```
```   418 lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n). norm x = c"
```
```   419   by (rule exI[where x="c *\<^sub>R cart_basis arbitrary"]) simp
```
```   420
```
```   421 lemma vector_choose_dist: assumes e: "0 <= e"
```
```   422   shows "\<exists>(y::real^'n). dist x y = e"
```
```   423 proof-
```
```   424   from vector_choose_size[OF e] obtain c:: "real ^'n"  where "norm c = e"
```
```   425     by blast
```
```   426   then have "dist x (x - c) = e" by (simp add: dist_norm)
```
```   427   then show ?thesis by blast
```
```   428 qed
```
```   429
```
```   430 lemma basis_inj[intro]: "inj (cart_basis :: 'n \<Rightarrow> real ^'n)"
```
```   431   by (simp add: inj_on_def vec_eq_iff)
```
```   432
```
```   433 lemma basis_expansion:
```
```   434   "setsum (\<lambda>i. (x\$i) *s cart_basis i) UNIV = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _")
```
```   435   by (auto simp add: vec_eq_iff if_distrib setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong)
```
```   436
```
```   437 lemma smult_conv_scaleR: "c *s x = scaleR c x"
```
```   438   unfolding vector_scalar_mult_def scaleR_vec_def by simp
```
```   439
```
```   440 lemma basis_expansion':
```
```   441   "setsum (\<lambda>i. (x\$i) *\<^sub>R cart_basis i) UNIV = x"
```
```   442   by (rule basis_expansion [where 'a=real, unfolded smult_conv_scaleR])
```
```   443
```
```   444 lemma basis_expansion_unique:
```
```   445   "setsum (\<lambda>i. f i *s cart_basis i) UNIV = (x::('a::comm_ring_1) ^'n) \<longleftrightarrow> (\<forall>i. f i = x\$i)"
```
```   446   by (simp add: vec_eq_iff setsum_delta if_distrib cong del: if_weak_cong)
```
```   447
```
```   448 lemma dot_basis:
```
```   449   shows "cart_basis i \<bullet> x = x\$i" "x \<bullet> (cart_basis i) = (x\$i)"
```
```   450   by (auto simp add: inner_vec_def cart_basis_def cond_application_beta if_distrib setsum_delta
```
```   451            cong del: if_weak_cong)
```
```   452
```
```   453 lemma inner_basis:
```
```   454   fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n"
```
```   455   shows "inner (cart_basis i) x = inner 1 (x \$ i)"
```
```   456     and "inner x (cart_basis i) = inner (x \$ i) 1"
```
```   457   unfolding inner_vec_def cart_basis_def
```
```   458   by (auto simp add: cond_application_beta if_distrib setsum_delta cong del: if_weak_cong)
```
```   459
```
```   460 lemma basis_eq_0: "cart_basis i = (0::'a::semiring_1^'n) \<longleftrightarrow> False"
```
```   461   by (auto simp add: vec_eq_iff)
```
```   462
```
```   463 lemma basis_nonzero:
```
```   464   shows "cart_basis k \<noteq> (0:: 'a::semiring_1 ^'n)"
```
```   465   by (simp add: basis_eq_0)
```
```   466
```
```   467 text {* some lemmas to map between Eucl and Cart *}
```
```   468 lemma basis_real_n[simp]:"(basis (\<pi>' i)::real^'a) = cart_basis i"
```
```   469   unfolding basis_vec_def using pi'_range[where 'n='a]
```
```   470   by (auto simp: vec_eq_iff)
```
```   471
```
```   472 subsection {* Orthogonality on cartesian products *}
```
```   473
```
```   474 lemma orthogonal_basis:
```
```   475   shows "orthogonal (cart_basis i) x \<longleftrightarrow> x\$i = (0::real)"
```
```   476   by (auto simp add: orthogonal_def inner_vec_def cart_basis_def if_distrib
```
```   477                      cond_application_beta setsum_delta cong del: if_weak_cong)
```
```   478
```
```   479 lemma orthogonal_basis_basis:
```
```   480   shows "orthogonal (cart_basis i :: real^'n) (cart_basis j) \<longleftrightarrow> i \<noteq> j"
```
```   481   unfolding orthogonal_basis[of i] basis_component[of j] by simp
```
```   482
```
```   483 subsection {* Linearity on cartesian products *}
```
```   484
```
```   485 lemma linear_vmul_component:
```
```   486   assumes lf: "linear f"
```
```   487   shows "linear (\<lambda>x. f x \$ k *\<^sub>R v)"
```
```   488   using lf
```
```   489   by (auto simp add: linear_def algebra_simps)
```
```   490
```
```   491
```
```   492 subsection{* Adjoints on cartesian products *}
```
```   493
```
```   494 text {* TODO: The following lemmas about adjoints should hold for any
```
```   495 Hilbert space (i.e. complete inner product space).
```
```   496 (see \url{http://en.wikipedia.org/wiki/Hermitian_adjoint})
```
```   497 *}
```
```   498
```
```   499 lemma adjoint_works_lemma:
```
```   500   fixes f:: "real ^'n \<Rightarrow> real ^'m"
```
```   501   assumes lf: "linear f"
```
```   502   shows "\<forall>x y. f x \<bullet> y = x \<bullet> adjoint f y"
```
```   503 proof-
```
```   504   let ?N = "UNIV :: 'n set"
```
```   505   let ?M = "UNIV :: 'm set"
```
```   506   have fN: "finite ?N" by simp
```
```   507   have fM: "finite ?M" by simp
```
```   508   {fix y:: "real ^ 'm"
```
```   509     let ?w = "(\<chi> i. (f (cart_basis i) \<bullet> y)) :: real ^ 'n"
```
```   510     {fix x
```
```   511       have "f x \<bullet> y = f (setsum (\<lambda>i. (x\$i) *\<^sub>R cart_basis i) ?N) \<bullet> y"
```
```   512         by (simp only: basis_expansion')
```
```   513       also have "\<dots> = (setsum (\<lambda>i. (x\$i) *\<^sub>R f (cart_basis i)) ?N) \<bullet> y"
```
```   514         unfolding linear_setsum[OF lf fN]
```
```   515         by (simp add: linear_cmul[OF lf])
```
```   516       finally have "f x \<bullet> y = x \<bullet> ?w"
```
```   517         apply (simp only: )
```
```   518         apply (simp add: inner_vec_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] field_simps)
```
```   519         done}
```
```   520   }
```
```   521   then show ?thesis unfolding adjoint_def
```
```   522     some_eq_ex[of "\<lambda>f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y"]
```
```   523     using choice_iff[of "\<lambda>a b. \<forall>x. f x \<bullet> a = x \<bullet> b "]
```
```   524     by metis
```
```   525 qed
```
```   526
```
```   527 lemma adjoint_works:
```
```   528   fixes f:: "real ^'n \<Rightarrow> real ^'m"
```
```   529   assumes lf: "linear f"
```
```   530   shows "x \<bullet> adjoint f y = f x \<bullet> y"
```
```   531   using adjoint_works_lemma[OF lf] by metis
```
```   532
```
```   533 lemma adjoint_linear:
```
```   534   fixes f:: "real ^'n \<Rightarrow> real ^'m"
```
```   535   assumes lf: "linear f"
```
```   536   shows "linear (adjoint f)"
```
```   537   unfolding linear_def vector_eq_ldot[where 'a="real^'n", symmetric] apply safe
```
```   538   unfolding inner_simps smult_conv_scaleR adjoint_works[OF lf] by auto
```
```   539
```
```   540 lemma adjoint_clauses:
```
```   541   fixes f:: "real ^'n \<Rightarrow> real ^'m"
```
```   542   assumes lf: "linear f"
```
```   543   shows "x \<bullet> adjoint f y = f x \<bullet> y"
```
```   544   and "adjoint f y \<bullet> x = y \<bullet> f x"
```
```   545   by (simp_all add: adjoint_works[OF lf] inner_commute)
```
```   546
```
```   547 lemma adjoint_adjoint:
```
```   548   fixes f:: "real ^'n \<Rightarrow> real ^'m"
```
```   549   assumes lf: "linear f"
```
```   550   shows "adjoint (adjoint f) = f"
```
```   551   by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
```
```   552
```
```   553
```
```   554 subsection {* Matrix operations *}
```
```   555
```
```   556 text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *}
```
```   557
```
```   558 definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"  (infixl "**" 70)
```
```   559   where "m ** m' == (\<chi> i j. setsum (\<lambda>k. ((m\$i)\$k) * ((m'\$k)\$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
```
```   560
```
```   561 definition matrix_vector_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"  (infixl "*v" 70)
```
```   562   where "m *v x \<equiv> (\<chi> i. setsum (\<lambda>j. ((m\$i)\$j) * (x\$j)) (UNIV ::'n set)) :: 'a^'m"
```
```   563
```
```   564 definition vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "  (infixl "v*" 70)
```
```   565   where "v v* m == (\<chi> j. setsum (\<lambda>i. ((m\$i)\$j) * (v\$i)) (UNIV :: 'm set)) :: 'a^'n"
```
```   566
```
```   567 definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
```
```   568 definition transpose where
```
```   569   "(transpose::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A\$j)\$i))"
```
```   570 definition "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A\$i)\$j))"
```
```   571 definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A\$i)\$j))"
```
```   572 definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
```
```   573 definition "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"
```
```   574
```
```   575 lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)
```
```   576 lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
```
```   577   by (vector matrix_matrix_mult_def setsum_addf[symmetric] field_simps)
```
```   578
```
```   579 lemma matrix_mul_lid:
```
```   580   fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
```
```   581   shows "mat 1 ** A = A"
```
```   582   apply (simp add: matrix_matrix_mult_def mat_def)
```
```   583   apply vector
```
```   584   by (auto simp only: if_distrib cond_application_beta setsum_delta'[OF finite]  mult_1_left mult_zero_left if_True UNIV_I)
```
```   585
```
```   586
```
```   587 lemma matrix_mul_rid:
```
```   588   fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
```
```   589   shows "A ** mat 1 = A"
```
```   590   apply (simp add: matrix_matrix_mult_def mat_def)
```
```   591   apply vector
```
```   592   by (auto simp only: if_distrib cond_application_beta setsum_delta[OF finite]  mult_1_right mult_zero_right if_True UNIV_I cong: if_cong)
```
```   593
```
```   594 lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
```
```   595   apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)
```
```   596   apply (subst setsum_commute)
```
```   597   apply simp
```
```   598   done
```
```   599
```
```   600 lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
```
```   601   apply (vector matrix_matrix_mult_def matrix_vector_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)
```
```   602   apply (subst setsum_commute)
```
```   603   apply simp
```
```   604   done
```
```   605
```
```   606 lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
```
```   607   apply (vector matrix_vector_mult_def mat_def)
```
```   608   by (simp add: if_distrib cond_application_beta
```
```   609     setsum_delta' cong del: if_weak_cong)
```
```   610
```
```   611 lemma matrix_transpose_mul: "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
```
```   612   by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult_commute)
```
```   613
```
```   614 lemma matrix_eq:
```
```   615   fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
```
```   616   shows "A = B \<longleftrightarrow>  (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")
```
```   617   apply auto
```
```   618   apply (subst vec_eq_iff)
```
```   619   apply clarify
```
```   620   apply (clarsimp simp add: matrix_vector_mult_def cart_basis_def if_distrib cond_application_beta vec_eq_iff cong del: if_weak_cong)
```
```   621   apply (erule_tac x="cart_basis ia" in allE)
```
```   622   apply (erule_tac x="i" in allE)
```
```   623   by (auto simp add: cart_basis_def if_distrib cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong)
```
```   624
```
```   625 lemma matrix_vector_mul_component:
```
```   626   shows "((A::real^_^_) *v x)\$k = (A\$k) \<bullet> x"
```
```   627   by (simp add: matrix_vector_mult_def inner_vec_def)
```
```   628
```
```   629 lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
```
```   630   apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
```
```   631   apply (subst setsum_commute)
```
```   632   by simp
```
```   633
```
```   634 lemma transpose_mat: "transpose (mat n) = mat n"
```
```   635   by (vector transpose_def mat_def)
```
```   636
```
```   637 lemma transpose_transpose: "transpose(transpose A) = A"
```
```   638   by (vector transpose_def)
```
```   639
```
```   640 lemma row_transpose:
```
```   641   fixes A:: "'a::semiring_1^_^_"
```
```   642   shows "row i (transpose A) = column i A"
```
```   643   by (simp add: row_def column_def transpose_def vec_eq_iff)
```
```   644
```
```   645 lemma column_transpose:
```
```   646   fixes A:: "'a::semiring_1^_^_"
```
```   647   shows "column i (transpose A) = row i A"
```
```   648   by (simp add: row_def column_def transpose_def vec_eq_iff)
```
```   649
```
```   650 lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
```
```   651 by (auto simp add: rows_def columns_def row_transpose intro: set_eqI)
```
```   652
```
```   653 lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" by (metis transpose_transpose rows_transpose)
```
```   654
```
```   655 text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *}
```
```   656
```
```   657 lemma matrix_mult_dot: "A *v x = (\<chi> i. A\$i \<bullet> x)"
```
```   658   by (simp add: matrix_vector_mult_def inner_vec_def)
```
```   659
```
```   660 lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x\$i) *s column i A) (UNIV:: 'n set)"
```
```   661   by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult_commute)
```
```   662
```
```   663 lemma vector_componentwise:
```
```   664   "(x::'a::ring_1^'n) = (\<chi> j. setsum (\<lambda>i. (x\$i) * (cart_basis i :: 'a^'n)\$j) (UNIV :: 'n set))"
```
```   665   apply (subst basis_expansion[symmetric])
```
```   666   by (vector vec_eq_iff setsum_component)
```
```   667
```
```   668 lemma linear_componentwise:
```
```   669   fixes f:: "real ^'m \<Rightarrow> real ^ _"
```
```   670   assumes lf: "linear f"
```
```   671   shows "(f x)\$j = setsum (\<lambda>i. (x\$i) * (f (cart_basis i)\$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
```
```   672 proof-
```
```   673   let ?M = "(UNIV :: 'm set)"
```
```   674   let ?N = "(UNIV :: 'n set)"
```
```   675   have fM: "finite ?M" by simp
```
```   676   have "?rhs = (setsum (\<lambda>i.(x\$i) *\<^sub>R f (cart_basis i) ) ?M)\$j"
```
```   677     unfolding vector_smult_component[symmetric] smult_conv_scaleR
```
```   678     unfolding setsum_component[of "(\<lambda>i.(x\$i) *\<^sub>R f (cart_basis i :: real^'m))" ?M]
```
```   679     ..
```
```   680   then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion' ..
```
```   681 qed
```
```   682
```
```   683 text{* Inverse matrices  (not necessarily square) *}
```
```   684
```
```   685 definition "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
```
```   686
```
```   687 definition "matrix_inv(A:: 'a::semiring_1^'n^'m) =
```
```   688         (SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
```
```   689
```
```   690 text{* Correspondence between matrices and linear operators. *}
```
```   691
```
```   692 definition matrix:: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
```
```   693 where "matrix f = (\<chi> i j. (f(cart_basis j))\$i)"
```
```   694
```
```   695 lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
```
```   696   by (simp add: linear_def matrix_vector_mult_def vec_eq_iff field_simps setsum_right_distrib setsum_addf)
```
```   697
```
```   698 lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::real ^ 'n)"
```
```   699 apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult_commute)
```
```   700 apply clarify
```
```   701 apply (rule linear_componentwise[OF lf, symmetric])
```
```   702 done
```
```   703
```
```   704 lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))" by (simp add: ext matrix_works)
```
```   705
```
```   706 lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"
```
```   707   by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)
```
```   708
```
```   709 lemma matrix_compose:
```
```   710   assumes lf: "linear (f::real^'n \<Rightarrow> real^'m)"
```
```   711   and lg: "linear (g::real^'m \<Rightarrow> real^_)"
```
```   712   shows "matrix (g o f) = matrix g ** matrix f"
```
```   713   using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]]
```
```   714   by (simp  add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
```
```   715
```
```   716 lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x\$i) *s ((transpose A)\$i)) (UNIV:: 'n set)"
```
```   717   by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult_commute)
```
```   718
```
```   719 lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
```
```   720   apply (rule adjoint_unique)
```
```   721   apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)
```
```   722   apply (subst setsum_commute)
```
```   723   apply (auto simp add: mult_ac)
```
```   724   done
```
```   725
```
```   726 lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
```
```   727   shows "matrix(adjoint f) = transpose(matrix f)"
```
```   728   apply (subst matrix_vector_mul[OF lf])
```
```   729   unfolding adjoint_matrix matrix_of_matrix_vector_mul ..
```
```   730
```
```   731 section {* lambda skolemization on cartesian products *}
```
```   732
```
```   733 (* FIXME: rename do choice_cart *)
```
```   734
```
```   735 lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
```
```   736    (\<exists>x::'a ^ 'n. \<forall>i. P i (x \$ i))" (is "?lhs \<longleftrightarrow> ?rhs")
```
```   737 proof-
```
```   738   let ?S = "(UNIV :: 'n set)"
```
```   739   {assume H: "?rhs"
```
```   740     then have ?lhs by auto}
```
```   741   moreover
```
```   742   {assume H: "?lhs"
```
```   743     then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
```
```   744     let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
```
```   745     {fix i
```
```   746       from f have "P i (f i)" by metis
```
```   747       then have "P i (?x \$ i)" by auto
```
```   748     }
```
```   749     hence "\<forall>i. P i (?x\$i)" by metis
```
```   750     hence ?rhs by metis }
```
```   751   ultimately show ?thesis by metis
```
```   752 qed
```
```   753
```
```   754 subsection {* Standard bases are a spanning set, and obviously finite. *}
```
```   755
```
```   756 lemma span_stdbasis:"span {cart_basis i :: real^'n | i. i \<in> (UNIV :: 'n set)} = UNIV"
```
```   757 apply (rule set_eqI)
```
```   758 apply auto
```
```   759 apply (subst basis_expansion'[symmetric])
```
```   760 apply (rule span_setsum)
```
```   761 apply simp
```
```   762 apply auto
```
```   763 apply (rule span_mul)
```
```   764 apply (rule span_superset)
```
```   765 apply (auto simp add: Collect_def mem_def)
```
```   766 done
```
```   767
```
```   768 lemma finite_stdbasis: "finite {cart_basis i ::real^'n |i. i\<in> (UNIV:: 'n set)}" (is "finite ?S")
```
```   769 proof-
```
```   770   have eq: "?S = cart_basis ` UNIV" by blast
```
```   771   show ?thesis unfolding eq by auto
```
```   772 qed
```
```   773
```
```   774 lemma card_stdbasis: "card {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)} = CARD('n)" (is "card ?S = _")
```
```   775 proof-
```
```   776   have eq: "?S = cart_basis ` UNIV" by blast
```
```   777   show ?thesis unfolding eq using card_image[OF basis_inj] by simp
```
```   778 qed
```
```   779
```
```   780
```
```   781 lemma independent_stdbasis_lemma:
```
```   782   assumes x: "(x::real ^ 'n) \<in> span (cart_basis ` S)"
```
```   783   and iS: "i \<notin> S"
```
```   784   shows "(x\$i) = 0"
```
```   785 proof-
```
```   786   let ?U = "UNIV :: 'n set"
```
```   787   let ?B = "cart_basis ` S"
```
```   788   let ?P = "\<lambda>(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x\$i =0"
```
```   789  {fix x::"real^_" assume xS: "x\<in> ?B"
```
```   790    from xS have "?P x" by auto}
```
```   791  moreover
```
```   792  have "subspace ?P"
```
```   793    by (auto simp add: subspace_def Collect_def mem_def)
```
```   794  ultimately show ?thesis
```
```   795    using x span_induct[of ?B ?P x] iS by blast
```
```   796 qed
```
```   797
```
```   798 lemma independent_stdbasis: "independent {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)}"
```
```   799 proof-
```
```   800   let ?I = "UNIV :: 'n set"
```
```   801   let ?b = "cart_basis :: _ \<Rightarrow> real ^'n"
```
```   802   let ?B = "?b ` ?I"
```
```   803   have eq: "{?b i|i. i \<in> ?I} = ?B"
```
```   804     by auto
```
```   805   {assume d: "dependent ?B"
```
```   806     then obtain k where k: "k \<in> ?I" "?b k \<in> span (?B - {?b k})"
```
```   807       unfolding dependent_def by auto
```
```   808     have eq1: "?B - {?b k} = ?B - ?b ` {k}"  by simp
```
```   809     have eq2: "?B - {?b k} = ?b ` (?I - {k})"
```
```   810       unfolding eq1
```
```   811       apply (rule inj_on_image_set_diff[symmetric])
```
```   812       apply (rule basis_inj) using k(1) by auto
```
```   813     from k(2) have th0: "?b k \<in> span (?b ` (?I - {k}))" unfolding eq2 .
```
```   814     from independent_stdbasis_lemma[OF th0, of k, simplified]
```
```   815     have False by simp}
```
```   816   then show ?thesis unfolding eq dependent_def ..
```
```   817 qed
```
```   818
```
```   819 lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
```
```   820   unfolding inner_simps smult_conv_scaleR by auto
```
```   821
```
```   822 lemma linear_eq_stdbasis_cart:
```
```   823   assumes lf: "linear (f::real^'m \<Rightarrow> _)" and lg: "linear g"
```
```   824   and fg: "\<forall>i. f (cart_basis i) = g(cart_basis i)"
```
```   825   shows "f = g"
```
```   826 proof-
```
```   827   let ?U = "UNIV :: 'm set"
```
```   828   let ?I = "{cart_basis i:: real^'m|i. i \<in> ?U}"
```
```   829   {fix x assume x: "x \<in> (UNIV :: (real^'m) set)"
```
```   830     from equalityD2[OF span_stdbasis]
```
```   831     have IU: " (UNIV :: (real^'m) set) \<subseteq> span ?I" by blast
```
```   832     from linear_eq[OF lf lg IU] fg x
```
```   833     have "f x = g x" unfolding Collect_def  Ball_def mem_def by metis}
```
```   834   then show ?thesis by (auto intro: ext)
```
```   835 qed
```
```   836
```
```   837 lemma bilinear_eq_stdbasis_cart:
```
```   838   assumes bf: "bilinear (f:: real^'m \<Rightarrow> real^'n \<Rightarrow> _)"
```
```   839   and bg: "bilinear g"
```
```   840   and fg: "\<forall>i j. f (cart_basis i) (cart_basis j) = g (cart_basis i) (cart_basis j)"
```
```   841   shows "f = g"
```
```   842 proof-
```
```   843   from fg have th: "\<forall>x \<in> {cart_basis i| i. i\<in> (UNIV :: 'm set)}. \<forall>y\<in>  {cart_basis j |j. j \<in> (UNIV :: 'n set)}. f x y = g x y" by blast
```
```   844   from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by (blast intro: ext)
```
```   845 qed
```
```   846
```
```   847 lemma left_invertible_transpose:
```
```   848   "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
```
```   849   by (metis matrix_transpose_mul transpose_mat transpose_transpose)
```
```   850
```
```   851 lemma right_invertible_transpose:
```
```   852   "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
```
```   853   by (metis matrix_transpose_mul transpose_mat transpose_transpose)
```
```   854
```
```   855 lemma matrix_left_invertible_injective:
```
```   856 "(\<exists>B. (B::real^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x y. A *v x = A *v y \<longrightarrow> x = y)"
```
```   857 proof-
```
```   858   {fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y"
```
```   859     from xy have "B*v (A *v x) = B *v (A*v y)" by simp
```
```   860     hence "x = y"
```
```   861       unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid .}
```
```   862   moreover
```
```   863   {assume A: "\<forall>x y. A *v x = A *v y \<longrightarrow> x = y"
```
```   864     hence i: "inj (op *v A)" unfolding inj_on_def by auto
```
```   865     from linear_injective_left_inverse[OF matrix_vector_mul_linear i]
```
```   866     obtain g where g: "linear g" "g o op *v A = id" by blast
```
```   867     have "matrix g ** A = mat 1"
```
```   868       unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
```
```   869       using g(2) by (simp add: fun_eq_iff)
```
```   870     then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast}
```
```   871   ultimately show ?thesis by blast
```
```   872 qed
```
```   873
```
```   874 lemma matrix_left_invertible_ker:
```
```   875   "(\<exists>B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"
```
```   876   unfolding matrix_left_invertible_injective
```
```   877   using linear_injective_0[OF matrix_vector_mul_linear, of A]
```
```   878   by (simp add: inj_on_def)
```
```   879
```
```   880 lemma matrix_right_invertible_surjective:
```
```   881 "(\<exists>B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
```
```   882 proof-
```
```   883   {fix B :: "real ^'m^'n"  assume AB: "A ** B = mat 1"
```
```   884     {fix x :: "real ^ 'm"
```
```   885       have "A *v (B *v x) = x"
```
```   886         by (simp add: matrix_vector_mul_lid matrix_vector_mul_assoc AB)}
```
```   887     hence "surj (op *v A)" unfolding surj_def by metis }
```
```   888   moreover
```
```   889   {assume sf: "surj (op *v A)"
```
```   890     from linear_surjective_right_inverse[OF matrix_vector_mul_linear sf]
```
```   891     obtain g:: "real ^'m \<Rightarrow> real ^'n" where g: "linear g" "op *v A o g = id"
```
```   892       by blast
```
```   893
```
```   894     have "A ** (matrix g) = mat 1"
```
```   895       unfolding matrix_eq  matrix_vector_mul_lid
```
```   896         matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
```
```   897       using g(2) unfolding o_def fun_eq_iff id_def
```
```   898       .
```
```   899     hence "\<exists>B. A ** (B::real^'m^'n) = mat 1" by blast
```
```   900   }
```
```   901   ultimately show ?thesis unfolding surj_def by blast
```
```   902 qed
```
```   903
```
```   904 lemma matrix_left_invertible_independent_columns:
```
```   905   fixes A :: "real^'n^'m"
```
```   906   shows "(\<exists>(B::real ^'m^'n). B ** A = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
```
```   907    (is "?lhs \<longleftrightarrow> ?rhs")
```
```   908 proof-
```
```   909   let ?U = "UNIV :: 'n set"
```
```   910   {assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0"
```
```   911     {fix c i assume c: "setsum (\<lambda>i. c i *s column i A) ?U = 0"
```
```   912       and i: "i \<in> ?U"
```
```   913       let ?x = "\<chi> i. c i"
```
```   914       have th0:"A *v ?x = 0"
```
```   915         using c
```
```   916         unfolding matrix_mult_vsum vec_eq_iff
```
```   917         by auto
```
```   918       from k[rule_format, OF th0] i
```
```   919       have "c i = 0" by (vector vec_eq_iff)}
```
```   920     hence ?rhs by blast}
```
```   921   moreover
```
```   922   {assume H: ?rhs
```
```   923     {fix x assume x: "A *v x = 0"
```
```   924       let ?c = "\<lambda>i. ((x\$i ):: real)"
```
```   925       from H[rule_format, of ?c, unfolded matrix_mult_vsum[symmetric], OF x]
```
```   926       have "x = 0" by vector}}
```
```   927   ultimately show ?thesis unfolding matrix_left_invertible_ker by blast
```
```   928 qed
```
```   929
```
```   930 lemma matrix_right_invertible_independent_rows:
```
```   931   fixes A :: "real^'n^'m"
```
```   932   shows "(\<exists>(B::real^'m^'n). A ** B = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
```
```   933   unfolding left_invertible_transpose[symmetric]
```
```   934     matrix_left_invertible_independent_columns
```
```   935   by (simp add: column_transpose)
```
```   936
```
```   937 lemma matrix_right_invertible_span_columns:
```
```   938   "(\<exists>(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \<longleftrightarrow> span (columns A) = UNIV" (is "?lhs = ?rhs")
```
```   939 proof-
```
```   940   let ?U = "UNIV :: 'm set"
```
```   941   have fU: "finite ?U" by simp
```
```   942   have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::real^'m). setsum (\<lambda>i. (x\$i) *s column i A) ?U = y)"
```
```   943     unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def
```
```   944     apply (subst eq_commute) ..
```
```   945   have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> span (columns A))" by blast
```
```   946   {assume h: ?lhs
```
```   947     {fix x:: "real ^'n"
```
```   948         from h[unfolded lhseq, rule_format, of x] obtain y:: "real ^'m"
```
```   949           where y: "setsum (\<lambda>i. (y\$i) *s column i A) ?U = x" by blast
```
```   950         have "x \<in> span (columns A)"
```
```   951           unfolding y[symmetric]
```
```   952           apply (rule span_setsum[OF fU])
```
```   953           apply clarify
```
```   954           unfolding smult_conv_scaleR
```
```   955           apply (rule span_mul)
```
```   956           apply (rule span_superset)
```
```   957           unfolding columns_def
```
```   958           by blast}
```
```   959     then have ?rhs unfolding rhseq by blast}
```
```   960   moreover
```
```   961   {assume h:?rhs
```
```   962     let ?P = "\<lambda>(y::real ^'n). \<exists>(x::real^'m). setsum (\<lambda>i. (x\$i) *s column i A) ?U = y"
```
```   963     {fix y have "?P y"
```
```   964       proof(rule span_induct_alt[of ?P "columns A", folded smult_conv_scaleR])
```
```   965         show "\<exists>x\<Colon>real ^ 'm. setsum (\<lambda>i. (x\$i) *s column i A) ?U = 0"
```
```   966           by (rule exI[where x=0], simp)
```
```   967       next
```
```   968         fix c y1 y2 assume y1: "y1 \<in> columns A" and y2: "?P y2"
```
```   969         from y1 obtain i where i: "i \<in> ?U" "y1 = column i A"
```
```   970           unfolding columns_def by blast
```
```   971         from y2 obtain x:: "real ^'m" where
```
```   972           x: "setsum (\<lambda>i. (x\$i) *s column i A) ?U = y2" by blast
```
```   973         let ?x = "(\<chi> j. if j = i then c + (x\$i) else (x\$j))::real^'m"
```
```   974         show "?P (c*s y1 + y2)"
```
```   975           proof(rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib right_distrib cond_application_beta cong del: if_weak_cong)
```
```   976             fix j
```
```   977             have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x\$i)) * ((column xa A)\$j)
```
```   978            else (x\$xa) * ((column xa A\$j))) = (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))" using i(1)
```
```   979               by (simp add: field_simps)
```
```   980             have "setsum (\<lambda>xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j)
```
```   981            else (x\$xa) * ((column xa A\$j))) ?U = setsum (\<lambda>xa. (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))) ?U"
```
```   982               apply (rule setsum_cong[OF refl])
```
```   983               using th by blast
```
```   984             also have "\<dots> = setsum (\<lambda>xa. if xa = i then c * ((column i A)\$j) else 0) ?U + setsum (\<lambda>xa. ((x\$xa) * ((column xa A)\$j))) ?U"
```
```   985               by (simp add: setsum_addf)
```
```   986             also have "\<dots> = c * ((column i A)\$j) + setsum (\<lambda>xa. ((x\$xa) * ((column xa A)\$j))) ?U"
```
```   987               unfolding setsum_delta[OF fU]
```
```   988               using i(1) by simp
```
```   989             finally show "setsum (\<lambda>xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j)
```
```   990            else (x\$xa) * ((column xa A\$j))) ?U = c * ((column i A)\$j) + setsum (\<lambda>xa. ((x\$xa) * ((column xa A)\$j))) ?U" .
```
```   991           qed
```
```   992         next
```
```   993           show "y \<in> span (columns A)" unfolding h by blast
```
```   994         qed}
```
```   995     then have ?lhs unfolding lhseq ..}
```
```   996   ultimately show ?thesis by blast
```
```   997 qed
```
```   998
```
```   999 lemma matrix_left_invertible_span_rows:
```
```  1000   "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
```
```  1001   unfolding right_invertible_transpose[symmetric]
```
```  1002   unfolding columns_transpose[symmetric]
```
```  1003   unfolding matrix_right_invertible_span_columns
```
```  1004  ..
```
```  1005
```
```  1006 text {* The same result in terms of square matrices. *}
```
```  1007
```
```  1008 lemma matrix_left_right_inverse:
```
```  1009   fixes A A' :: "real ^'n^'n"
```
```  1010   shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1"
```
```  1011 proof-
```
```  1012   {fix A A' :: "real ^'n^'n" assume AA': "A ** A' = mat 1"
```
```  1013     have sA: "surj (op *v A)"
```
```  1014       unfolding surj_def
```
```  1015       apply clarify
```
```  1016       apply (rule_tac x="(A' *v y)" in exI)
```
```  1017       by (simp add: matrix_vector_mul_assoc AA' matrix_vector_mul_lid)
```
```  1018     from linear_surjective_isomorphism[OF matrix_vector_mul_linear sA]
```
```  1019     obtain f' :: "real ^'n \<Rightarrow> real ^'n"
```
```  1020       where f': "linear f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
```
```  1021     have th: "matrix f' ** A = mat 1"
```
```  1022       by (simp add: matrix_eq matrix_works[OF f'(1)] matrix_vector_mul_assoc[symmetric] matrix_vector_mul_lid f'(2)[rule_format])
```
```  1023     hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp
```
```  1024     hence "matrix f' = A'" by (simp add: matrix_mul_assoc[symmetric] AA' matrix_mul_rid matrix_mul_lid)
```
```  1025     hence "matrix f' ** A = A' ** A" by simp
```
```  1026     hence "A' ** A = mat 1" by (simp add: th)}
```
```  1027   then show ?thesis by blast
```
```  1028 qed
```
```  1029
```
```  1030 text {* Considering an n-element vector as an n-by-1 or 1-by-n matrix. *}
```
```  1031
```
```  1032 definition "rowvector v = (\<chi> i j. (v\$j))"
```
```  1033
```
```  1034 definition "columnvector v = (\<chi> i j. (v\$i))"
```
```  1035
```
```  1036 lemma transpose_columnvector:
```
```  1037  "transpose(columnvector v) = rowvector v"
```
```  1038   by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff)
```
```  1039
```
```  1040 lemma transpose_rowvector: "transpose(rowvector v) = columnvector v"
```
```  1041   by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff)
```
```  1042
```
```  1043 lemma dot_rowvector_columnvector:
```
```  1044   "columnvector (A *v v) = A ** columnvector v"
```
```  1045   by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
```
```  1046
```
```  1047 lemma dot_matrix_product: "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))\$1)\$1"
```
```  1048   by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def)
```
```  1049
```
```  1050 lemma dot_matrix_vector_mul:
```
```  1051   fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
```
```  1052   shows "(A *v x) \<bullet> (B *v y) =
```
```  1053       (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))\$1)\$1"
```
```  1054 unfolding dot_matrix_product transpose_columnvector[symmetric]
```
```  1055   dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
```
```  1056
```
```  1057
```
```  1058 lemma infnorm_cart:"infnorm (x::real^'n) = Sup {abs(x\$i) |i. i\<in> (UNIV :: 'n set)}"
```
```  1059   unfolding infnorm_def apply(rule arg_cong[where f=Sup]) apply safe
```
```  1060   apply(rule_tac x="\<pi> i" in exI) defer
```
```  1061   apply(rule_tac x="\<pi>' i" in exI) unfolding nth_conv_component using pi'_range by auto
```
```  1062
```
```  1063 lemma infnorm_set_image_cart:
```
```  1064   "{abs(x\$i) |i. i\<in> (UNIV :: _ set)} =
```
```  1065   (\<lambda>i. abs(x\$i)) ` (UNIV)" by blast
```
```  1066
```
```  1067 lemma infnorm_set_lemma_cart:
```
```  1068   shows "finite {abs((x::'a::abs ^'n)\$i) |i. i\<in> (UNIV :: 'n set)}"
```
```  1069   and "{abs(x\$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}"
```
```  1070   unfolding  infnorm_set_image_cart
```
```  1071   by auto
```
```  1072
```
```  1073 lemma component_le_infnorm_cart:
```
```  1074   shows "\<bar>x\$i\<bar> \<le> infnorm (x::real^'n)"
```
```  1075   unfolding nth_conv_component
```
```  1076   using component_le_infnorm[of x] .
```
```  1077
```
```  1078 instance vec :: (perfect_space, finite) perfect_space
```
```  1079 proof
```
```  1080   fix x :: "'a ^ 'b"
```
```  1081   show "x islimpt UNIV"
```
```  1082     apply (rule islimptI)
```
```  1083     apply (unfold open_vec_def)
```
```  1084     apply (drule (1) bspec)
```
```  1085     apply clarsimp
```
```  1086     apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>y. y \<in> A i \<and> y \<noteq> x \$ i")
```
```  1087      apply (drule finite_choice [OF finite_UNIV], erule exE)
```
```  1088      apply (rule_tac x="vec_lambda f" in exI)
```
```  1089      apply (simp add: vec_eq_iff)
```
```  1090     apply (rule ballI, drule_tac x=i in spec, clarify)
```
```  1091     apply (cut_tac x="x \$ i" in islimpt_UNIV)
```
```  1092     apply (simp add: islimpt_def)
```
```  1093     done
```
```  1094 qed
```
```  1095
```
```  1096 lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x\$i}"
```
```  1097 proof-
```
```  1098   let ?U = "UNIV :: 'n set"
```
```  1099   let ?O = "{x::real^'n. \<forall>i. x\$i\<ge>0}"
```
```  1100   {fix x:: "real^'n" and i::'n assume H: "\<forall>e>0. \<exists>x'\<in>?O. x' \<noteq> x \<and> dist x' x < e"
```
```  1101     and xi: "x\$i < 0"
```
```  1102     from xi have th0: "-x\$i > 0" by arith
```
```  1103     from H[rule_format, OF th0] obtain x' where x': "x' \<in>?O" "x' \<noteq> x" "dist x' x < -x \$ i" by blast
```
```  1104       have th:" \<And>b a (x::real). abs x <= b \<Longrightarrow> b <= a ==> ~(a + x < 0)" by arith
```
```  1105       have th': "\<And>x (y::real). x < 0 \<Longrightarrow> 0 <= y ==> abs x <= abs (y - x)" by arith
```
```  1106       have th1: "\<bar>x\$i\<bar> \<le> \<bar>(x' - x)\$i\<bar>" using x'(1) xi
```
```  1107         apply (simp only: vector_component)
```
```  1108         by (rule th') auto
```
```  1109       have th2: "\<bar>dist x x'\<bar> \<ge> \<bar>(x' - x)\$i\<bar>" using  component_le_norm_cart[of "x'-x" i]
```
```  1110         apply (simp add: dist_norm) by norm
```
```  1111       from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) }
```
```  1112   then show ?thesis unfolding closed_limpt islimpt_approachable
```
```  1113     unfolding not_le[symmetric] by blast
```
```  1114 qed
```
```  1115 lemma Lim_component_cart:
```
```  1116   fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
```
```  1117   shows "(f ---> l) net \<Longrightarrow> ((\<lambda>a. f a \$i) ---> l\$i) net"
```
```  1118   unfolding tendsto_iff
```
```  1119   apply (clarify)
```
```  1120   apply (drule spec, drule (1) mp)
```
```  1121   apply (erule eventually_elim1)
```
```  1122   apply (erule le_less_trans [OF dist_vec_nth_le])
```
```  1123   done
```
```  1124
```
```  1125 lemma bounded_component_cart: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x \$ i) ` s)"
```
```  1126 unfolding bounded_def
```
```  1127 apply clarify
```
```  1128 apply (rule_tac x="x \$ i" in exI)
```
```  1129 apply (rule_tac x="e" in exI)
```
```  1130 apply clarify
```
```  1131 apply (rule order_trans [OF dist_vec_nth_le], simp)
```
```  1132 done
```
```  1133
```
```  1134 lemma compact_lemma_cart:
```
```  1135   fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
```
```  1136   assumes "bounded s" and "\<forall>n. f n \<in> s"
```
```  1137   shows "\<forall>d.
```
```  1138         \<exists>l r. subseq r \<and>
```
```  1139         (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)"
```
```  1140 proof
```
```  1141   fix d::"'n set" have "finite d" by simp
```
```  1142   thus "\<exists>l::'a ^ 'n. \<exists>r. subseq r \<and>
```
```  1143       (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)"
```
```  1144   proof(induct d) case empty thus ?case unfolding subseq_def by auto
```
```  1145   next case (insert k d)
```
```  1146     have s': "bounded ((\<lambda>x. x \$ k) ` s)" using `bounded s` by (rule bounded_component_cart)
```
```  1147     obtain l1::"'a^'n" and r1 where r1:"subseq r1" and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \$ i) (l1 \$ i) < e) sequentially"
```
```  1148       using insert(3) by auto
```
```  1149     have f': "\<forall>n. f (r1 n) \$ k \<in> (\<lambda>x. x \$ k) ` s" using `\<forall>n. f n \<in> s` by simp
```
```  1150     obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \$ k) ---> l2) sequentially"
```
```  1151       using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
```
```  1152     def r \<equiv> "r1 \<circ> r2" have r:"subseq r"
```
```  1153       using r1 and r2 unfolding r_def o_def subseq_def by auto
```
```  1154     moreover
```
```  1155     def l \<equiv> "(\<chi> i. if i = k then l2 else l1\$i)::'a^'n"
```
```  1156     { fix e::real assume "e>0"
```
```  1157       from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \$ i) (l1 \$ i) < e) sequentially" by blast
```
```  1158       from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) \$ k) l2 < e) sequentially" by (rule tendstoD)
```
```  1159       from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) \$ i) (l1 \$ i) < e) sequentially"
```
```  1160         by (rule eventually_subseq)
```
```  1161       have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) \$ i) (l \$ i) < e) sequentially"
```
```  1162         using N1' N2 by (rule eventually_elim2, simp add: l_def r_def)
```
```  1163     }
```
```  1164     ultimately show ?case by auto
```
```  1165   qed
```
```  1166 qed
```
```  1167
```
```  1168 instance vec :: (heine_borel, finite) heine_borel
```
```  1169 proof
```
```  1170   fix s :: "('a ^ 'b) set" and f :: "nat \<Rightarrow> 'a ^ 'b"
```
```  1171   assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
```
```  1172   then obtain l r where r: "subseq r"
```
```  1173     and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) \$ i) (l \$ i) < e) sequentially"
```
```  1174     using compact_lemma_cart [OF s f] by blast
```
```  1175   let ?d = "UNIV::'b set"
```
```  1176   { fix e::real assume "e>0"
```
```  1177     hence "0 < e / (real_of_nat (card ?d))"
```
```  1178       using zero_less_card_finite using divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto
```
```  1179     with l have "eventually (\<lambda>n. \<forall>i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))) sequentially"
```
```  1180       by simp
```
```  1181     moreover
```
```  1182     { fix n assume n: "\<forall>i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))"
```
```  1183       have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) \$ i) (l \$ i))"
```
```  1184         unfolding dist_vec_def using zero_le_dist by (rule setL2_le_setsum)
```
```  1185       also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
```
```  1186         by (rule setsum_strict_mono) (simp_all add: n)
```
```  1187       finally have "dist (f (r n)) l < e" by simp
```
```  1188     }
```
```  1189     ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
```
```  1190       by (rule eventually_elim1)
```
```  1191   }
```
```  1192   hence *:"((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp
```
```  1193   with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto
```
```  1194 qed
```
```  1195
```
```  1196 lemma continuous_at_component: "continuous (at a) (\<lambda>x. x \$ i)"
```
```  1197 unfolding continuous_at by (intro tendsto_intros)
```
```  1198
```
```  1199 lemma continuous_on_component: "continuous_on s (\<lambda>x. x \$ i)"
```
```  1200 unfolding continuous_on_def by (intro ballI tendsto_intros)
```
```  1201
```
```  1202 lemma interval_cart: fixes a :: "'a::ord^'n" shows
```
```  1203   "{a <..< b} = {x::'a^'n. \<forall>i. a\$i < x\$i \<and> x\$i < b\$i}" and
```
```  1204   "{a .. b} = {x::'a^'n. \<forall>i. a\$i \<le> x\$i \<and> x\$i \<le> b\$i}"
```
```  1205   by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def)
```
```  1206
```
```  1207 lemma mem_interval_cart: fixes a :: "'a::ord^'n" shows
```
```  1208   "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a\$i < x\$i \<and> x\$i < b\$i)"
```
```  1209   "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a\$i \<le> x\$i \<and> x\$i \<le> b\$i)"
```
```  1210   using interval_cart[of a b] by(auto simp add: set_eq_iff less_vec_def less_eq_vec_def)
```
```  1211
```
```  1212 lemma interval_eq_empty_cart: fixes a :: "real^'n" shows
```
```  1213  "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b\$i \<le> a\$i))" (is ?th1) and
```
```  1214  "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i. b\$i < a\$i))" (is ?th2)
```
```  1215 proof-
```
```  1216   { fix i x assume as:"b\$i \<le> a\$i" and x:"x\<in>{a <..< b}"
```
```  1217     hence "a \$ i < x \$ i \<and> x \$ i < b \$ i" unfolding mem_interval_cart by auto
```
```  1218     hence "a\$i < b\$i" by auto
```
```  1219     hence False using as by auto  }
```
```  1220   moreover
```
```  1221   { assume as:"\<forall>i. \<not> (b\$i \<le> a\$i)"
```
```  1222     let ?x = "(1/2) *\<^sub>R (a + b)"
```
```  1223     { fix i
```
```  1224       have "a\$i < b\$i" using as[THEN spec[where x=i]] by auto
```
```  1225       hence "a\$i < ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i < b\$i"
```
```  1226         unfolding vector_smult_component and vector_add_component
```
```  1227         by auto  }
```
```  1228     hence "{a <..< b} \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto  }
```
```  1229   ultimately show ?th1 by blast
```
```  1230
```
```  1231   { fix i x assume as:"b\$i < a\$i" and x:"x\<in>{a .. b}"
```
```  1232     hence "a \$ i \<le> x \$ i \<and> x \$ i \<le> b \$ i" unfolding mem_interval_cart by auto
```
```  1233     hence "a\$i \<le> b\$i" by auto
```
```  1234     hence False using as by auto  }
```
```  1235   moreover
```
```  1236   { assume as:"\<forall>i. \<not> (b\$i < a\$i)"
```
```  1237     let ?x = "(1/2) *\<^sub>R (a + b)"
```
```  1238     { fix i
```
```  1239       have "a\$i \<le> b\$i" using as[THEN spec[where x=i]] by auto
```
```  1240       hence "a\$i \<le> ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i \<le> b\$i"
```
```  1241         unfolding vector_smult_component and vector_add_component
```
```  1242         by auto  }
```
```  1243     hence "{a .. b} \<noteq> {}" using mem_interval_cart(2)[of "?x" a b] by auto  }
```
```  1244   ultimately show ?th2 by blast
```
```  1245 qed
```
```  1246
```
```  1247 lemma interval_ne_empty_cart: fixes a :: "real^'n" shows
```
```  1248   "{a  ..  b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a\$i \<le> b\$i)" and
```
```  1249   "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a\$i < b\$i)"
```
```  1250   unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le)
```
```  1251     (* BH: Why doesn't just "auto" work here? *)
```
```  1252
```
```  1253 lemma subset_interval_imp_cart: fixes a :: "real^'n" shows
```
```  1254  "(\<forall>i. a\$i \<le> c\$i \<and> d\$i \<le> b\$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}" and
```
```  1255  "(\<forall>i. a\$i < c\$i \<and> d\$i < b\$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}" and
```
```  1256  "(\<forall>i. a\$i \<le> c\$i \<and> d\$i \<le> b\$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}" and
```
```  1257  "(\<forall>i. a\$i \<le> c\$i \<and> d\$i \<le> b\$i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
```
```  1258   unfolding subset_eq[unfolded Ball_def] unfolding mem_interval_cart
```
```  1259   by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
```
```  1260
```
```  1261 lemma interval_sing: fixes a :: "'a::linorder^'n" shows
```
```  1262  "{a .. a} = {a} \<and> {a<..<a} = {}"
```
```  1263 apply(auto simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
```
```  1264 apply (simp add: order_eq_iff)
```
```  1265 apply (auto simp add: not_less less_imp_le)
```
```  1266 done
```
```  1267
```
```  1268 lemma interval_open_subset_closed_cart:  fixes a :: "'a::preorder^'n" shows
```
```  1269  "{a<..<b} \<subseteq> {a .. b}"
```
```  1270 proof(simp add: subset_eq, rule)
```
```  1271   fix x
```
```  1272   assume x:"x \<in>{a<..<b}"
```
```  1273   { fix i
```
```  1274     have "a \$ i \<le> x \$ i"
```
```  1275       using x order_less_imp_le[of "a\$i" "x\$i"]
```
```  1276       by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
```
```  1277   }
```
```  1278   moreover
```
```  1279   { fix i
```
```  1280     have "x \$ i \<le> b \$ i"
```
```  1281       using x order_less_imp_le[of "x\$i" "b\$i"]
```
```  1282       by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
```
```  1283   }
```
```  1284   ultimately
```
```  1285   show "a \<le> x \<and> x \<le> b"
```
```  1286     by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
```
```  1287 qed
```
```  1288
```
```  1289 lemma subset_interval_cart: fixes a :: "real^'n" shows
```
```  1290  "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c\$i \<le> d\$i) --> (\<forall>i. a\$i \<le> c\$i \<and> d\$i \<le> b\$i)" (is ?th1) and
```
```  1291  "{c .. d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i. c\$i \<le> d\$i) --> (\<forall>i. a\$i < c\$i \<and> d\$i < b\$i)" (is ?th2) and
```
```  1292  "{c<..<d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c\$i < d\$i) --> (\<forall>i. a\$i \<le> c\$i \<and> d\$i \<le> b\$i)" (is ?th3) and
```
```  1293  "{c<..<d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i. c\$i < d\$i) --> (\<forall>i. a\$i \<le> c\$i \<and> d\$i \<le> b\$i)" (is ?th4)
```
```  1294   using subset_interval[of c d a b] by (simp_all add: cart_simps real_euclidean_nth)
```
```  1295
```
```  1296 lemma disjoint_interval_cart: fixes a::"real^'n" shows
```
```  1297   "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b\$i < a\$i \<or> d\$i < c\$i \<or> b\$i < c\$i \<or> d\$i < a\$i))" (is ?th1) and
```
```  1298   "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i. (b\$i < a\$i \<or> d\$i \<le> c\$i \<or> b\$i \<le> c\$i \<or> d\$i \<le> a\$i))" (is ?th2) and
```
```  1299   "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b\$i \<le> a\$i \<or> d\$i < c\$i \<or> b\$i \<le> c\$i \<or> d\$i \<le> a\$i))" (is ?th3) and
```
```  1300   "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i. (b\$i \<le> a\$i \<or> d\$i \<le> c\$i \<or> b\$i \<le> c\$i \<or> d\$i \<le> a\$i))" (is ?th4)
```
```  1301   using disjoint_interval[of a b c d] by (simp_all add: cart_simps real_euclidean_nth)
```
```  1302
```
```  1303 lemma inter_interval_cart: fixes a :: "'a::linorder^'n" shows
```
```  1304  "{a .. b} \<inter> {c .. d} =  {(\<chi> i. max (a\$i) (c\$i)) .. (\<chi> i. min (b\$i) (d\$i))}"
```
```  1305   unfolding set_eq_iff and Int_iff and mem_interval_cart
```
```  1306   by auto
```
```  1307
```
```  1308 lemma closed_interval_left_cart: fixes b::"real^'n"
```
```  1309   shows "closed {x::real^'n. \<forall>i. x\$i \<le> b\$i}"
```
```  1310 proof-
```
```  1311   { fix i
```
```  1312     fix x::"real^'n" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i. x \$ i \<le> b \$ i}. x' \<noteq> x \<and> dist x' x < e"
```
```  1313     { assume "x\$i > b\$i"
```
```  1314       then obtain y where "y \$ i \<le> b \$ i"  "y \<noteq> x"  "dist y x < x\$i - b\$i" using x[THEN spec[where x="x\$i - b\$i"]] by auto
```
```  1315       hence False using component_le_norm_cart[of "y - x" i] unfolding dist_norm and vector_minus_component by auto   }
```
```  1316     hence "x\$i \<le> b\$i" by(rule ccontr)auto  }
```
```  1317   thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
```
```  1318 qed
```
```  1319
```
```  1320 lemma closed_interval_right_cart: fixes a::"real^'n"
```
```  1321   shows "closed {x::real^'n. \<forall>i. a\$i \<le> x\$i}"
```
```  1322 proof-
```
```  1323   { fix i
```
```  1324     fix x::"real^'n" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i. a \$ i \<le> x \$ i}. x' \<noteq> x \<and> dist x' x < e"
```
```  1325     { assume "a\$i > x\$i"
```
```  1326       then obtain y where "a \$ i \<le> y \$ i"  "y \<noteq> x"  "dist y x < a\$i - x\$i" using x[THEN spec[where x="a\$i - x\$i"]] by auto
```
```  1327       hence False using component_le_norm_cart[of "y - x" i] unfolding dist_norm and vector_minus_component by auto   }
```
```  1328     hence "a\$i \<le> x\$i" by(rule ccontr)auto  }
```
```  1329   thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
```
```  1330 qed
```
```  1331
```
```  1332 lemma is_interval_cart:"is_interval (s::(real^'n) set) \<longleftrightarrow>
```
```  1333   (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a\$i \<le> x\$i \<and> x\$i \<le> b\$i) \<or> (b\$i \<le> x\$i \<and> x\$i \<le> a\$i))) \<longrightarrow> x \<in> s)"
```
```  1334   unfolding is_interval_def Ball_def by (simp add: cart_simps real_euclidean_nth)
```
```  1335
```
```  1336 lemma closed_halfspace_component_le_cart:
```
```  1337   shows "closed {x::real^'n. x\$i \<le> a}"
```
```  1338   using closed_halfspace_le[of "(cart_basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto
```
```  1339
```
```  1340 lemma closed_halfspace_component_ge_cart:
```
```  1341   shows "closed {x::real^'n. x\$i \<ge> a}"
```
```  1342   using closed_halfspace_ge[of a "(cart_basis i)::real^'n"] unfolding inner_basis[OF assms] by auto
```
```  1343
```
```  1344 lemma open_halfspace_component_lt_cart:
```
```  1345   shows "open {x::real^'n. x\$i < a}"
```
```  1346   using open_halfspace_lt[of "(cart_basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto
```
```  1347
```
```  1348 lemma open_halfspace_component_gt_cart:
```
```  1349   shows "open {x::real^'n. x\$i  > a}"
```
```  1350   using open_halfspace_gt[of a "(cart_basis i)::real^'n"] unfolding inner_basis[OF assms] by auto
```
```  1351
```
```  1352 lemma Lim_component_le_cart: fixes f :: "'a \<Rightarrow> real^'n"
```
```  1353   assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)\$i \<le> b) net"
```
```  1354   shows "l\$i \<le> b"
```
```  1355 proof-
```
```  1356   { fix x have "x \<in> {x::real^'n. inner (cart_basis i) x \<le> b} \<longleftrightarrow> x\$i \<le> b" unfolding inner_basis by auto } note * = this
```
```  1357   show ?thesis using Lim_in_closed_set[of "{x. inner (cart_basis i) x \<le> b}" f net l] unfolding *
```
```  1358     using closed_halfspace_le[of "(cart_basis i)::real^'n" b] and assms(1,2,3) by auto
```
```  1359 qed
```
```  1360
```
```  1361 lemma Lim_component_ge_cart: fixes f :: "'a \<Rightarrow> real^'n"
```
```  1362   assumes "(f ---> l) net"  "\<not> (trivial_limit net)"  "eventually (\<lambda>x. b \<le> (f x)\$i) net"
```
```  1363   shows "b \<le> l\$i"
```
```  1364 proof-
```
```  1365   { fix x have "x \<in> {x::real^'n. inner (cart_basis i) x \<ge> b} \<longleftrightarrow> x\$i \<ge> b" unfolding inner_basis by auto } note * = this
```
```  1366   show ?thesis using Lim_in_closed_set[of "{x. inner (cart_basis i) x \<ge> b}" f net l] unfolding *
```
```  1367     using closed_halfspace_ge[of b "(cart_basis i)::real^'n"] and assms(1,2,3) by auto
```
```  1368 qed
```
```  1369
```
```  1370 lemma Lim_component_eq_cart: fixes f :: "'a \<Rightarrow> real^'n"
```
```  1371   assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)\$i = b) net"
```
```  1372   shows "l\$i = b"
```
```  1373   using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge_cart[OF net, of b i] and
```
```  1374     Lim_component_le_cart[OF net, of i b] by auto
```
```  1375
```
```  1376 lemma connected_ivt_component_cart: fixes x::"real^'n" shows
```
```  1377  "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x\$k \<le> a \<Longrightarrow> a \<le> y\$k \<Longrightarrow> (\<exists>z\<in>s.  z\$k = a)"
```
```  1378   using connected_ivt_hyperplane[of s x y "(cart_basis k)::real^'n" a] by (auto simp add: inner_basis)
```
```  1379
```
```  1380 lemma subspace_substandard_cart:
```
```  1381  "subspace {x::real^_. (\<forall>i. P i \<longrightarrow> x\$i = 0)}"
```
```  1382   unfolding subspace_def by auto
```
```  1383
```
```  1384 lemma closed_substandard_cart:
```
```  1385  "closed {x::real^'n. \<forall>i. P i --> x\$i = 0}" (is "closed ?A")
```
```  1386 proof-
```
```  1387   let ?D = "{i. P i}"
```
```  1388   let ?Bs = "{{x::real^'n. inner (cart_basis i) x = 0}| i. i \<in> ?D}"
```
```  1389   { fix x
```
```  1390     { assume "x\<in>?A"
```
```  1391       hence x:"\<forall>i\<in>?D. x \$ i = 0" by auto
```
```  1392       hence "x\<in> \<Inter> ?Bs" by(auto simp add: inner_basis x) }
```
```  1393     moreover
```
```  1394     { assume x:"x\<in>\<Inter>?Bs"
```
```  1395       { fix i assume i:"i \<in> ?D"
```
```  1396         then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::real^'n. inner (cart_basis i) x = 0}" by auto
```
```  1397         hence "x \$ i = 0" unfolding B using x unfolding inner_basis by auto  }
```
```  1398       hence "x\<in>?A" by auto }
```
```  1399     ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" .. }
```
```  1400   hence "?A = \<Inter> ?Bs" by auto
```
```  1401   thus ?thesis by(auto simp add: closed_Inter closed_hyperplane)
```
```  1402 qed
```
```  1403
```
```  1404 lemma dim_substandard_cart:
```
```  1405   shows "dim {x::real^'n. \<forall>i. i \<notin> d \<longrightarrow> x\$i = 0} = card d" (is "dim ?A = _")
```
```  1406 proof- have *:"{x. \<forall>i<DIM((real, 'n) vec). i \<notin> \<pi>' ` d \<longrightarrow> x \$\$ i = 0} =
```
```  1407     {x::real^'n. \<forall>i. i \<notin> d \<longrightarrow> x\$i = 0}"apply safe
```
```  1408     apply(erule_tac x="\<pi>' i" in allE) defer
```
```  1409     apply(erule_tac x="\<pi> i" in allE)
```
```  1410     unfolding image_iff real_euclidean_nth[symmetric] by (auto simp: pi'_inj[THEN inj_eq])
```
```  1411   have " \<pi>' ` d \<subseteq> {..<DIM((real, 'n) vec)}" using pi'_range[where 'n='n] by auto
```
```  1412   thus ?thesis using dim_substandard[of "\<pi>' ` d", where 'a="real^'n"]
```
```  1413     unfolding * using card_image[of "\<pi>'" d] using pi'_inj unfolding inj_on_def by auto
```
```  1414 qed
```
```  1415
```
```  1416 lemma affinity_inverses:
```
```  1417   assumes m0: "m \<noteq> (0::'a::field)"
```
```  1418   shows "(\<lambda>x. m *s x + c) o (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
```
```  1419   "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) o (\<lambda>x. m *s x + c) = id"
```
```  1420   using m0
```
```  1421 apply (auto simp add: fun_eq_iff vector_add_ldistrib)
```
```  1422 by (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric])
```
```  1423
```
```  1424 lemma vector_affinity_eq:
```
```  1425   assumes m0: "(m::'a::field) \<noteq> 0"
```
```  1426   shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)"
```
```  1427 proof
```
```  1428   assume h: "m *s x + c = y"
```
```  1429   hence "m *s x = y - c" by (simp add: field_simps)
```
```  1430   hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
```
```  1431   then show "x = inverse m *s y + - (inverse m *s c)"
```
```  1432     using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
```
```  1433 next
```
```  1434   assume h: "x = inverse m *s y + - (inverse m *s c)"
```
```  1435   show "m *s x + c = y" unfolding h diff_minus[symmetric]
```
```  1436     using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
```
```  1437 qed
```
```  1438
```
```  1439 lemma vector_eq_affinity:
```
```  1440  "(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)"
```
```  1441   using vector_affinity_eq[where m=m and x=x and y=y and c=c]
```
```  1442   by metis
```
```  1443
```
```  1444 lemma const_vector_cart:"((\<chi> i. d)::real^'n) = (\<chi>\<chi> i. d)"
```
```  1445   apply(subst euclidean_eq)
```
```  1446 proof safe case goal1
```
```  1447   hence *:"(basis i::real^'n) = cart_basis (\<pi> i)"
```
```  1448     unfolding basis_real_n[THEN sym] by auto
```
```  1449   have "((\<chi> i. d)::real^'n) \$\$ i = d" unfolding euclidean_component_def *
```
```  1450     unfolding dot_basis by auto
```
```  1451   thus ?case using goal1 by auto
```
```  1452 qed
```
```  1453
```
```  1454 section "Convex Euclidean Space"
```
```  1455
```
```  1456 lemma Cart_1:"(1::real^'n) = (\<chi>\<chi> i. 1)"
```
```  1457   apply(subst euclidean_eq)
```
```  1458 proof safe case goal1 thus ?case using nth_conv_component[THEN sym,where i1="\<pi> i" and x1="1::real^'n"] by auto
```
```  1459 qed
```
```  1460
```
```  1461 declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp]
```
```  1462 declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp]
```
```  1463
```
```  1464 lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component less_eq_vec_def vec_lambda_beta basis_component vector_uminus_component
```
```  1465
```
```  1466 lemma convex_box_cart:
```
```  1467   assumes "\<And>i. convex {x. P i x}"
```
```  1468   shows "convex {x. \<forall>i. P i (x\$i)}"
```
```  1469   using assms unfolding convex_def by auto
```
```  1470
```
```  1471 lemma convex_positive_orthant_cart: "convex {x::real^'n. (\<forall>i. 0 \<le> x\$i)}"
```
```  1472   by (rule convex_box_cart) (simp add: atLeast_def[symmetric] convex_real_interval)
```
```  1473
```
```  1474 lemma unit_interval_convex_hull_cart:
```
```  1475   "{0::real^'n .. 1} = convex hull {x. \<forall>i. (x\$i = 0) \<or> (x\$i = 1)}" (is "?int = convex hull ?points")
```
```  1476   unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"]
```
```  1477   apply(rule arg_cong[where f="\<lambda>x. convex hull x"]) apply(rule set_eqI) unfolding mem_Collect_eq
```
```  1478   apply safe apply(erule_tac x="\<pi>' i" in allE) unfolding nth_conv_component defer
```
```  1479   apply(erule_tac x="\<pi> i" in allE) by auto
```
```  1480
```
```  1481 lemma cube_convex_hull_cart:
```
```  1482   assumes "0 < d" obtains s::"(real^'n) set" where "finite s" "{x - (\<chi> i. d) .. x + (\<chi> i. d)} = convex hull s"
```
```  1483 proof- from cube_convex_hull[OF assms, where 'a="real^'n" and x=x] guess s . note s=this
```
```  1484   show thesis apply(rule that[OF s(1)]) unfolding s(2)[THEN sym] const_vector_cart ..
```
```  1485 qed
```
```  1486
```
```  1487 lemma std_simplex_cart:
```
```  1488   "(insert (0::real^'n) { cart_basis i | i. i\<in>UNIV}) =
```
```  1489   (insert 0 { basis i | i. i<DIM((real,'n) vec)})"
```
```  1490   apply(rule arg_cong[where f="\<lambda>s. (insert 0 s)"])
```
```  1491   unfolding basis_real_n[THEN sym] apply safe
```
```  1492   apply(rule_tac x="\<pi>' i" in exI) defer
```
```  1493   apply(rule_tac x="\<pi> i" in exI) using pi'_range[where 'n='n] by auto
```
```  1494
```
```  1495 subsection "Brouwer Fixpoint"
```
```  1496
```
```  1497 lemma kuhn_labelling_lemma_cart:
```
```  1498   assumes "(\<forall>x::real^_. P x \<longrightarrow> P (f x))"  "\<forall>x. P x \<longrightarrow> (\<forall>i. Q i \<longrightarrow> 0 \<le> x\$i \<and> x\$i \<le> 1)"
```
```  1499   shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and>
```
```  1500              (\<forall>x i. P x \<and> Q i \<and> (x\$i = 0) \<longrightarrow> (l x i = 0)) \<and>
```
```  1501              (\<forall>x i. P x \<and> Q i \<and> (x\$i = 1) \<longrightarrow> (l x i = 1)) \<and>
```
```  1502              (\<forall>x i. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x\$i \<le> f(x)\$i) \<and>
```
```  1503              (\<forall>x i. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x)\$i \<le> x\$i)" proof-
```
```  1504   have and_forall_thm:"\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)" by auto
```
```  1505   have *:"\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> (x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x)" by auto
```
```  1506   show ?thesis unfolding and_forall_thm apply(subst choice_iff[THEN sym])+ proof(rule,rule) case goal1
```
```  1507     let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x \$ xa = 0 \<longrightarrow> y = (0::nat)) \<and>
```
```  1508         (P x \<and> Q xa \<and> x \$ xa = 1 \<longrightarrow> y = 1) \<and> (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x \$ xa \<le> f x \$ xa) \<and> (P x \<and> Q xa \<and> y = 1 \<longrightarrow> f x \$ xa \<le> x \$ xa)"
```
```  1509     { assume "P x" "Q xa" hence "0 \<le> f x \$ xa \<and> f x \$ xa \<le> 1" using assms(2)[rule_format,of "f x" xa]
```
```  1510         apply(drule_tac assms(1)[rule_format]) by auto }
```
```  1511     hence "?R 0 \<or> ?R 1" by auto thus ?case by auto qed qed
```
```  1512
```
```  1513 lemma interval_bij_cart:"interval_bij = (\<lambda> (a,b) (u,v) (x::real^'n).
```
```  1514     (\<chi> i. u\$i + (x\$i - a\$i) / (b\$i - a\$i) * (v\$i - u\$i))::real^'n)"
```
```  1515   unfolding interval_bij_def apply(rule ext)+ apply safe
```
```  1516   unfolding vec_eq_iff vec_lambda_beta unfolding nth_conv_component
```
```  1517   apply rule apply(subst euclidean_lambda_beta) using pi'_range by auto
```
```  1518
```
```  1519 lemma interval_bij_affine_cart:
```
```  1520  "interval_bij (a,b) (u,v) = (\<lambda>x. (\<chi> i. (v\$i - u\$i) / (b\$i - a\$i) * x\$i) +
```
```  1521             (\<chi> i. u\$i - (v\$i - u\$i) / (b\$i - a\$i) * a\$i)::real^'n)"
```
```  1522   apply rule unfolding vec_eq_iff interval_bij_cart vector_component_simps
```
```  1523   by(auto simp add: field_simps add_divide_distrib[THEN sym])
```
```  1524
```
```  1525 subsection "Derivative"
```
```  1526
```
```  1527 lemma has_derivative_vmul_component_cart: fixes c::"real^'a \<Rightarrow> real^'b" and v::"real^'c"
```
```  1528   assumes "(c has_derivative c') net"
```
```  1529   shows "((\<lambda>x. c(x)\$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)\$k *\<^sub>R v)) net"
```
```  1530   unfolding nth_conv_component
```
```  1531   by (intro has_derivative_intros assms)
```
```  1532
```
```  1533 lemma differentiable_at_imp_differentiable_on: "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
```
```  1534   unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI)
```
```  1535
```
```  1536 definition "jacobian f net = matrix(frechet_derivative f net)"
```
```  1537
```
```  1538 lemma jacobian_works: "(f::(real^'a) \<Rightarrow> (real^'b)) differentiable net \<longleftrightarrow> (f has_derivative (\<lambda>h. (jacobian f net) *v h)) net"
```
```  1539   apply rule unfolding jacobian_def apply(simp only: matrix_works[OF linear_frechet_derivative]) defer
```
```  1540   apply(rule differentiableI) apply assumption unfolding frechet_derivative_works by assumption
```
```  1541
```
```  1542 subsection {* Component of the differential must be zero if it exists at a local        *)
```
```  1543 (* maximum or minimum for that corresponding component. *}
```
```  1544
```
```  1545 lemma differential_zero_maxmin_component: fixes f::"real^'a \<Rightarrow> real^'b"
```
```  1546   assumes "0 < e" "((\<forall>y \<in> ball x e. (f y)\$k \<le> (f x)\$k) \<or> (\<forall>y\<in>ball x e. (f x)\$k \<le> (f y)\$k))"
```
```  1547   "f differentiable (at x)" shows "jacobian f (at x) \$ k = 0"
```
```  1548 (* FIXME: reuse proof of generic differential_zero_maxmin_component*)
```
```  1549
```
```  1550 proof(rule ccontr)
```
```  1551   def D \<equiv> "jacobian f (at x)" assume "jacobian f (at x) \$ k \<noteq> 0"
```
```  1552   then obtain j where j:"D\$k\$j \<noteq> 0" unfolding vec_eq_iff D_def by auto
```
```  1553   hence *:"abs (jacobian f (at x) \$ k \$ j) / 2 > 0" unfolding D_def by auto
```
```  1554   note as = assms(3)[unfolded jacobian_works has_derivative_at_alt]
```
```  1555   guess e' using as[THEN conjunct2,rule_format,OF *] .. note e' = this
```
```  1556   guess d using real_lbound_gt_zero[OF assms(1) e'[THEN conjunct1]] .. note d = this
```
```  1557   { fix c assume "abs c \<le> d"
```
```  1558     hence *:"norm (x + c *\<^sub>R cart_basis j - x) < e'" using norm_basis[of j] d by auto
```
```  1559     have "\<bar>(f (x + c *\<^sub>R cart_basis j) - f x - D *v (c *\<^sub>R cart_basis j)) \$ k\<bar> \<le> norm (f (x + c *\<^sub>R cart_basis j) - f x - D *v (c *\<^sub>R cart_basis j))"
```
```  1560       by(rule component_le_norm_cart)
```
```  1561     also have "\<dots> \<le> \<bar>D \$ k \$ j\<bar> / 2 * \<bar>c\<bar>" using e'[THEN conjunct2,rule_format,OF *] and norm_basis[of j] unfolding D_def[symmetric] by auto
```
```  1562     finally have "\<bar>(f (x + c *\<^sub>R cart_basis j) - f x - D *v (c *\<^sub>R cart_basis j)) \$ k\<bar> \<le> \<bar>D \$ k \$ j\<bar> / 2 * \<bar>c\<bar>" by simp
```
```  1563     hence "\<bar>f (x + c *\<^sub>R cart_basis j) \$ k - f x \$ k - c * D \$ k \$ j\<bar> \<le> \<bar>D \$ k \$ j\<bar> / 2 * \<bar>c\<bar>"
```
```  1564       unfolding vector_component_simps matrix_vector_mul_component unfolding smult_conv_scaleR[symmetric]
```
```  1565       unfolding inner_simps dot_basis smult_conv_scaleR by simp  } note * = this
```
```  1566   have "x + d *\<^sub>R cart_basis j \<in> ball x e" "x - d *\<^sub>R cart_basis j \<in> ball x e"
```
```  1567     unfolding mem_ball dist_norm using norm_basis[of j] d by auto
```
```  1568   hence **:"((f (x - d *\<^sub>R cart_basis j))\$k \<le> (f x)\$k \<and> (f (x + d *\<^sub>R cart_basis j))\$k \<le> (f x)\$k) \<or>
```
```  1569          ((f (x - d *\<^sub>R cart_basis j))\$k \<ge> (f x)\$k \<and> (f (x + d *\<^sub>R cart_basis j))\$k \<ge> (f x)\$k)" using assms(2) by auto
```
```  1570   have ***:"\<And>y y1 y2 d dx::real. (y1\<le>y\<and>y2\<le>y) \<or> (y\<le>y1\<and>y\<le>y2) \<Longrightarrow> d < abs dx \<Longrightarrow> abs(y1 - y - - dx) \<le> d \<Longrightarrow> (abs (y2 - y - dx) \<le> d) \<Longrightarrow> False" by arith
```
```  1571   show False apply(rule ***[OF **, where dx="d * D \$ k \$ j" and d="\<bar>D \$ k \$ j\<bar> / 2 * \<bar>d\<bar>"])
```
```  1572     using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left
```
```  1573     unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
```
```  1574 qed
```
```  1575
```
```  1576 subsection {* Lemmas for working on @{typ "real^1"} *}
```
```  1577
```
```  1578 lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
```
```  1579   by (metis num1_eq_iff)
```
```  1580
```
```  1581 lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
```
```  1582   by auto (metis num1_eq_iff)
```
```  1583
```
```  1584 lemma exhaust_2:
```
```  1585   fixes x :: 2 shows "x = 1 \<or> x = 2"
```
```  1586 proof (induct x)
```
```  1587   case (of_int z)
```
```  1588   then have "0 <= z" and "z < 2" by simp_all
```
```  1589   then have "z = 0 | z = 1" by arith
```
```  1590   then show ?case by auto
```
```  1591 qed
```
```  1592
```
```  1593 lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
```
```  1594   by (metis exhaust_2)
```
```  1595
```
```  1596 lemma exhaust_3:
```
```  1597   fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3"
```
```  1598 proof (induct x)
```
```  1599   case (of_int z)
```
```  1600   then have "0 <= z" and "z < 3" by simp_all
```
```  1601   then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
```
```  1602   then show ?case by auto
```
```  1603 qed
```
```  1604
```
```  1605 lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
```
```  1606   by (metis exhaust_3)
```
```  1607
```
```  1608 lemma UNIV_1 [simp]: "UNIV = {1::1}"
```
```  1609   by (auto simp add: num1_eq_iff)
```
```  1610
```
```  1611 lemma UNIV_2: "UNIV = {1::2, 2::2}"
```
```  1612   using exhaust_2 by auto
```
```  1613
```
```  1614 lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
```
```  1615   using exhaust_3 by auto
```
```  1616
```
```  1617 lemma setsum_1: "setsum f (UNIV::1 set) = f 1"
```
```  1618   unfolding UNIV_1 by simp
```
```  1619
```
```  1620 lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"
```
```  1621   unfolding UNIV_2 by simp
```
```  1622
```
```  1623 lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
```
```  1624   unfolding UNIV_3 by (simp add: add_ac)
```
```  1625
```
```  1626 instantiation num1 :: cart_one begin
```
```  1627 instance proof
```
```  1628   show "CARD(1) = Suc 0" by auto
```
```  1629 qed end
```
```  1630
```
```  1631 (* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *)
```
```  1632
```
```  1633 abbreviation vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x \<equiv> vec x"
```
```  1634
```
```  1635 abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
```
```  1636   where "dest_vec1 x \<equiv> (x\$1)"
```
```  1637
```
```  1638 lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
```
```  1639   by (simp_all add:  vec_eq_iff)
```
```  1640
```
```  1641 lemma vec1_component[simp]: "(vec1 x)\$1 = x"
```
```  1642   by (simp_all add:  vec_eq_iff)
```
```  1643
```
```  1644 lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
```
```  1645   by (metis vec1_dest_vec1(1))
```
```  1646
```
```  1647 lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
```
```  1648   by (metis vec1_dest_vec1(1))
```
```  1649
```
```  1650 lemma vec1_eq[simp]:  "vec1 x = vec1 y \<longleftrightarrow> x = y"
```
```  1651   by (metis vec1_dest_vec1(2))
```
```  1652
```
```  1653 lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
```
```  1654   by (metis vec1_dest_vec1(1))
```
```  1655
```
```  1656 subsection{* The collapse of the general concepts to dimension one. *}
```
```  1657
```
```  1658 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x\$1))"
```
```  1659   by (simp add: vec_eq_iff)
```
```  1660
```
```  1661 lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
```
```  1662   apply auto
```
```  1663   apply (erule_tac x= "x\$1" in allE)
```
```  1664   apply (simp only: vector_one[symmetric])
```
```  1665   done
```
```  1666
```
```  1667 lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)"
```
```  1668   by (simp add: norm_vec_def)
```
```  1669
```
```  1670 lemma norm_real: "norm(x::real ^ 1) = abs(x\$1)"
```
```  1671   by (simp add: norm_vector_1)
```
```  1672
```
```  1673 lemma dist_real: "dist(x::real ^ 1) y = abs((x\$1) - (y\$1))"
```
```  1674   by (auto simp add: norm_real dist_norm)
```
```  1675
```
```  1676 subsection{* Explicit vector construction from lists. *}
```
```  1677
```
```  1678 definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
```
```  1679
```
```  1680 lemma vector_1: "(vector[x]) \$1 = x"
```
```  1681   unfolding vector_def by simp
```
```  1682
```
```  1683 lemma vector_2:
```
```  1684  "(vector[x,y]) \$1 = x"
```
```  1685  "(vector[x,y] :: 'a^2)\$2 = (y::'a::zero)"
```
```  1686   unfolding vector_def by simp_all
```
```  1687
```
```  1688 lemma vector_3:
```
```  1689  "(vector [x,y,z] ::('a::zero)^3)\$1 = x"
```
```  1690  "(vector [x,y,z] ::('a::zero)^3)\$2 = y"
```
```  1691  "(vector [x,y,z] ::('a::zero)^3)\$3 = z"
```
```  1692   unfolding vector_def by simp_all
```
```  1693
```
```  1694 lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
```
```  1695   apply auto
```
```  1696   apply (erule_tac x="v\$1" in allE)
```
```  1697   apply (subgoal_tac "vector [v\$1] = v")
```
```  1698   apply simp
```
```  1699   apply (vector vector_def)
```
```  1700   apply simp
```
```  1701   done
```
```  1702
```
```  1703 lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
```
```  1704   apply auto
```
```  1705   apply (erule_tac x="v\$1" in allE)
```
```  1706   apply (erule_tac x="v\$2" in allE)
```
```  1707   apply (subgoal_tac "vector [v\$1, v\$2] = v")
```
```  1708   apply simp
```
```  1709   apply (vector vector_def)
```
```  1710   apply (simp add: forall_2)
```
```  1711   done
```
```  1712
```
```  1713 lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
```
```  1714   apply auto
```
```  1715   apply (erule_tac x="v\$1" in allE)
```
```  1716   apply (erule_tac x="v\$2" in allE)
```
```  1717   apply (erule_tac x="v\$3" in allE)
```
```  1718   apply (subgoal_tac "vector [v\$1, v\$2, v\$3] = v")
```
```  1719   apply simp
```
```  1720   apply (vector vector_def)
```
```  1721   apply (simp add: forall_3)
```
```  1722   done
```
```  1723
```
```  1724 lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_eqI,rule) unfolding image_iff defer
```
```  1725   apply(rule_tac x="dest_vec1 x" in bexI) by auto
```
```  1726
```
```  1727 lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
```
```  1728   by (simp)
```
```  1729
```
```  1730 lemma dest_vec1_vec: "dest_vec1(vec x) = x"
```
```  1731   by (simp)
```
```  1732
```
```  1733 lemma dest_vec1_sum: assumes fS: "finite S"
```
```  1734   shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
```
```  1735   apply (induct rule: finite_induct[OF fS])
```
```  1736   apply simp
```
```  1737   apply auto
```
```  1738   done
```
```  1739
```
```  1740 lemma norm_vec1 [simp]: "norm(vec1 x) = abs(x)"
```
```  1741   by (simp add: vec_def norm_real)
```
```  1742
```
```  1743 lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
```
```  1744   by (simp only: dist_real vec1_component)
```
```  1745 lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
```
```  1746   by (metis vec1_dest_vec1(1) norm_vec1)
```
```  1747
```
```  1748 lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
```
```  1749    vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def real_norm_def
```
```  1750
```
```  1751 lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
```
```  1752   unfolding bounded_linear_def additive_def bounded_linear_axioms_def
```
```  1753   unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps
```
```  1754   apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto
```
```  1755
```
```  1756 lemma linear_vmul_dest_vec1:
```
```  1757   fixes f:: "real^_ \<Rightarrow> real^1"
```
```  1758   shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
```
```  1759   unfolding smult_conv_scaleR
```
```  1760   by (rule linear_vmul_component)
```
```  1761
```
```  1762 lemma linear_from_scalars:
```
```  1763   assumes lf: "linear (f::real^1 \<Rightarrow> real^_)"
```
```  1764   shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
```
```  1765   unfolding smult_conv_scaleR
```
```  1766   apply (rule ext)
```
```  1767   apply (subst matrix_works[OF lf, symmetric])
```
```  1768   apply (auto simp add: vec_eq_iff matrix_vector_mult_def column_def mult_commute)
```
```  1769   done
```
```  1770
```
```  1771 lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \<Rightarrow> real^1)"
```
```  1772   shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
```
```  1773   apply (rule ext)
```
```  1774   apply (subst matrix_works[OF lf, symmetric])
```
```  1775   apply (simp add: vec_eq_iff matrix_vector_mult_def row_def inner_vec_def mult_commute)
```
```  1776   done
```
```  1777
```
```  1778 lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
```
```  1779   by (simp add: dest_vec1_eq[symmetric])
```
```  1780
```
```  1781 lemma setsum_scalars: assumes fS: "finite S"
```
```  1782   shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)"
```
```  1783   unfolding vec_setsum[OF fS] by simp
```
```  1784
```
```  1785 lemma dest_vec1_wlog_le: "(\<And>(x::'a::linorder ^ 1) y. P x y \<longleftrightarrow> P y x)  \<Longrightarrow> (\<And>x y. dest_vec1 x <= dest_vec1 y ==> P x y) \<Longrightarrow> P x y"
```
```  1786   apply (cases "dest_vec1 x \<le> dest_vec1 y")
```
```  1787   apply simp
```
```  1788   apply (subgoal_tac "dest_vec1 y \<le> dest_vec1 x")
```
```  1789   apply (auto)
```
```  1790   done
```
```  1791
```
```  1792 text{* Lifting and dropping *}
```
```  1793
```
```  1794 lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
```
```  1795   assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)"
```
```  1796   using assms unfolding continuous_on_iff apply safe
```
```  1797   apply(erule_tac x="x\$1" in ballE,erule_tac x=e in allE) apply safe
```
```  1798   apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real
```
```  1799   apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:less_eq_vec_def)
```
```  1800
```
```  1801 lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
```
```  1802   assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)"
```
```  1803   using assms unfolding continuous_on_iff apply safe
```
```  1804   apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe
```
```  1805   apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real
```
```  1806   apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:less_eq_vec_def)
```
```  1807
```
```  1808 lemma continuous_on_vec1:"continuous_on A (vec1::real\<Rightarrow>real^1)"
```
```  1809   by(rule linear_continuous_on[OF bounded_linear_vec1])
```
```  1810
```
```  1811 lemma mem_interval_1: fixes x :: "real^1" shows
```
```  1812  "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
```
```  1813  "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
```
```  1814 by(simp_all add: vec_eq_iff less_vec_def less_eq_vec_def)
```
```  1815
```
```  1816 lemma vec1_interval:fixes a::"real" shows
```
```  1817   "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
```
```  1818   "vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
```
```  1819   apply(rule_tac[!] set_eqI) unfolding image_iff less_vec_def unfolding mem_interval_cart
```
```  1820   unfolding forall_1 unfolding vec1_dest_vec1_simps
```
```  1821   apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
```
```  1822   apply(rule_tac x="dest_vec1 x" in bexI) by auto
```
```  1823
```
```  1824 (* Some special cases for intervals in R^1.                                  *)
```
```  1825
```
```  1826 lemma interval_cases_1: fixes x :: "real^1" shows
```
```  1827  "x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
```
```  1828   unfolding vec_eq_iff less_vec_def less_eq_vec_def mem_interval_cart by(auto simp del:dest_vec1_eq)
```
```  1829
```
```  1830 lemma in_interval_1: fixes x :: "real^1" shows
```
```  1831  "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b) \<and>
```
```  1832   (x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
```
```  1833   unfolding vec_eq_iff less_vec_def less_eq_vec_def mem_interval_cart by(auto simp del:dest_vec1_eq)
```
```  1834
```
```  1835 lemma interval_eq_empty_1: fixes a :: "real^1" shows
```
```  1836   "{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
```
```  1837   "{a<..<b} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a"
```
```  1838   unfolding interval_eq_empty_cart and ex_1 by auto
```
```  1839
```
```  1840 lemma subset_interval_1: fixes a :: "real^1" shows
```
```  1841  "({a .. b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
```
```  1842                 dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
```
```  1843  "({a .. b} \<subseteq> {c<..<d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
```
```  1844                 dest_vec1 c < dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b < dest_vec1 d)"
```
```  1845  "({a<..<b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b \<le> dest_vec1 a \<or>
```
```  1846                 dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
```
```  1847  "({a<..<b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
```
```  1848                 dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
```
```  1849   unfolding subset_interval_cart[of a b c d] unfolding forall_1 by auto
```
```  1850
```
```  1851 lemma eq_interval_1: fixes a :: "real^1" shows
```
```  1852  "{a .. b} = {c .. d} \<longleftrightarrow>
```
```  1853           dest_vec1 b < dest_vec1 a \<and> dest_vec1 d < dest_vec1 c \<or>
```
```  1854           dest_vec1 a = dest_vec1 c \<and> dest_vec1 b = dest_vec1 d"
```
```  1855 unfolding set_eq_subset[of "{a .. b}" "{c .. d}"]
```
```  1856 unfolding subset_interval_1(1)[of a b c d]
```
```  1857 unfolding subset_interval_1(1)[of c d a b]
```
```  1858 by auto
```
```  1859
```
```  1860 lemma disjoint_interval_1: fixes a :: "real^1" shows
```
```  1861   "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d < dest_vec1 c  \<or>  dest_vec1 b < dest_vec1 c \<or> dest_vec1 d < dest_vec1 a"
```
```  1862   "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
```
```  1863   "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d < dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
```
```  1864   "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
```
```  1865   unfolding disjoint_interval_cart and ex_1 by auto
```
```  1866
```
```  1867 lemma open_closed_interval_1: fixes a :: "real^1" shows
```
```  1868  "{a<..<b} = {a .. b} - {a, b}"
```
```  1869   unfolding set_eq_iff apply simp unfolding less_vec_def and less_eq_vec_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
```
```  1870
```
```  1871 lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
```
```  1872   unfolding set_eq_iff apply simp unfolding less_vec_def and less_eq_vec_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
```
```  1873
```
```  1874 lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
```
```  1875   "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
```
```  1876   using Lim_component_le_cart[of f l net 1 b] by auto
```
```  1877
```
```  1878 lemma Lim_drop_ge: fixes f :: "'a \<Rightarrow> real^1" shows
```
```  1879  "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. b \<le> dest_vec1 (f x)) net ==> b \<le> dest_vec1 l"
```
```  1880   using Lim_component_ge_cart[of f l net b 1] by auto
```
```  1881
```
```  1882 text{* Also more convenient formulations of monotone convergence.                *}
```
```  1883
```
```  1884 lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real^1"
```
```  1885   assumes "bounded {s n| n::nat. True}"  "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
```
```  1886   shows "\<exists>l. (s ---> l) sequentially"
```
```  1887 proof-
```
```  1888   obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_iff abs_dest_vec1] by auto
```
```  1889   { fix m::nat
```
```  1890     have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
```
```  1891       apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq)  }
```
```  1892   hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
```
```  1893   then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] unfolding monoseq_def by auto
```
```  1894   thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
```
```  1895     unfolding dist_norm unfolding abs_dest_vec1  by auto
```
```  1896 qed
```
```  1897
```
```  1898 lemma dest_vec1_simps[simp]: fixes a::"real^1"
```
```  1899   shows "a\$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
```
```  1900   "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
```
```  1901   by(auto simp add: less_eq_vec_def vec_eq_iff)
```
```  1902
```
```  1903 lemma dest_vec1_inverval:
```
```  1904   "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"
```
```  1905   "dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}"
```
```  1906   "dest_vec1 ` {a ..<b} = {dest_vec1 a ..<dest_vec1 b}"
```
```  1907   "dest_vec1 ` {a<..<b} = {dest_vec1 a<..<dest_vec1 b}"
```
```  1908   apply(rule_tac [!] equalityI)
```
```  1909   unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff
```
```  1910   apply(rule_tac [!] allI)apply(rule_tac [!] impI)
```
```  1911   apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
```
```  1912   apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
```
```  1913   by (auto simp add: less_vec_def less_eq_vec_def)
```
```  1914
```
```  1915 lemma dest_vec1_setsum: assumes "finite S"
```
```  1916   shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
```
```  1917   using dest_vec1_sum[OF assms] by auto
```
```  1918
```
```  1919 lemma open_dest_vec1_vimage: "open S \<Longrightarrow> open (dest_vec1 -` S)"
```
```  1920 unfolding open_vec_def forall_1 by auto
```
```  1921
```
```  1922 lemma tendsto_dest_vec1 [tendsto_intros]:
```
```  1923   "(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
```
```  1924 by(rule tendsto_vec_nth)
```
```  1925
```
```  1926 lemma continuous_dest_vec1: "continuous net f \<Longrightarrow> continuous net (\<lambda>x. dest_vec1 (f x))"
```
```  1927   unfolding continuous_def by (rule tendsto_dest_vec1)
```
```  1928
```
```  1929 lemma forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))"
```
```  1930   apply safe defer apply(erule_tac x="vec1 x" in allE) by auto
```
```  1931
```
```  1932 lemma forall_of_dest_vec1: "(\<forall>v. P (\<lambda>x. dest_vec1 (v x))) \<longleftrightarrow> (\<forall>x. P x)"
```
```  1933   apply rule apply rule apply(erule_tac x="(vec1 \<circ> x)" in allE) unfolding o_def vec1_dest_vec1 by auto
```
```  1934
```
```  1935 lemma forall_of_dest_vec1': "(\<forall>v. P (dest_vec1 v)) \<longleftrightarrow> (\<forall>x. P x)"
```
```  1936   apply rule apply rule apply(erule_tac x="(vec1 x)" in allE) defer apply rule
```
```  1937   apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto
```
```  1938
```
```  1939 lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding dist_norm by auto
```
```  1940
```
```  1941 lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
```
```  1942   shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
```
```  1943   { assume ?l guess K using linear_bounded[OF `?l`] ..
```
```  1944     hence "\<exists>K. \<forall>x. \<bar>f x\<bar> \<le> \<bar>x\<bar> * K" apply(rule_tac x=K in exI)
```
```  1945       unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) }
```
```  1946   thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def
```
```  1947     unfolding vec1_dest_vec1_simps by auto qed
```
```  1948
```
```  1949 lemma vec1_le[simp]:fixes a::real shows "vec1 a \<le> vec1 b \<longleftrightarrow> a \<le> b"
```
```  1950   unfolding less_eq_vec_def by auto
```
```  1951 lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \<longleftrightarrow> a < b"
```
```  1952   unfolding less_vec_def by auto
```
```  1953
```
```  1954
```
```  1955 subsection {* Derivatives on real = Derivatives on @{typ "real^1"} *}
```
```  1956
```
```  1957 lemma has_derivative_within_vec1_dest_vec1: fixes f::"real\<Rightarrow>real" shows
```
```  1958   "((vec1 \<circ> f \<circ> dest_vec1) has_derivative (vec1 \<circ> f' \<circ> dest_vec1)) (at (vec1 x) within vec1 ` s)
```
```  1959   = (f has_derivative f') (at x within s)"
```
```  1960   unfolding has_derivative_within unfolding bounded_linear_vec1_dest_vec1[unfolded linear_conv_bounded_linear]
```
```  1961   unfolding o_def Lim_within Ball_def unfolding forall_vec1
```
```  1962   unfolding vec1_dest_vec1_simps dist_vec1_0 image_iff by auto
```
```  1963
```
```  1964 lemma has_derivative_at_vec1_dest_vec1: fixes f::"real\<Rightarrow>real" shows
```
```  1965   "((vec1 \<circ> f \<circ> dest_vec1) has_derivative (vec1 \<circ> f' \<circ> dest_vec1)) (at (vec1 x)) = (f has_derivative f') (at x)"
```
```  1966   using has_derivative_within_vec1_dest_vec1[where s=UNIV, unfolded range_vec1 within_UNIV] by auto
```
```  1967
```
```  1968 lemma bounded_linear_vec1': fixes f::"'a::real_normed_vector\<Rightarrow>real"
```
```  1969   shows "bounded_linear f = bounded_linear (vec1 \<circ> f)"
```
```  1970   unfolding bounded_linear_def additive_def bounded_linear_axioms_def o_def
```
```  1971   unfolding vec1_dest_vec1_simps by auto
```
```  1972
```
```  1973 lemma bounded_linear_dest_vec1: fixes f::"real\<Rightarrow>'a::real_normed_vector"
```
```  1974   shows "bounded_linear f = bounded_linear (f \<circ> dest_vec1)"
```
```  1975   unfolding bounded_linear_def additive_def bounded_linear_axioms_def o_def
```
```  1976   unfolding vec1_dest_vec1_simps by auto
```
```  1977
```
```  1978 lemma has_derivative_at_vec1: fixes f::"'a::real_normed_vector\<Rightarrow>real" shows
```
```  1979   "(f has_derivative f') (at x) = ((vec1 \<circ> f) has_derivative (vec1 \<circ> f')) (at x)"
```
```  1980   unfolding has_derivative_at unfolding bounded_linear_vec1'[unfolded linear_conv_bounded_linear]
```
```  1981   unfolding o_def Lim_at unfolding vec1_dest_vec1_simps dist_vec1_0 by auto
```
```  1982
```
```  1983 lemma has_derivative_within_dest_vec1:fixes f::"real\<Rightarrow>'a::real_normed_vector" shows
```
```  1984   "((f \<circ> dest_vec1) has_derivative (f' \<circ> dest_vec1)) (at (vec1 x) within vec1 ` s) = (f has_derivative f') (at x within s)"
```
```  1985   unfolding has_derivative_within bounded_linear_dest_vec1 unfolding o_def Lim_within Ball_def
```
```  1986   unfolding vec1_dest_vec1_simps dist_vec1_0 image_iff by auto
```
```  1987
```
```  1988 lemma has_derivative_at_dest_vec1:fixes f::"real\<Rightarrow>'a::real_normed_vector" shows
```
```  1989   "((f \<circ> dest_vec1) has_derivative (f' \<circ> dest_vec1)) (at (vec1 x)) = (f has_derivative f') (at x)"
```
```  1990   using has_derivative_within_dest_vec1[where s=UNIV] by(auto simp add:within_UNIV)
```
```  1991
```
```  1992 subsection {* In particular if we have a mapping into @{typ "real^1"}. *}
```
```  1993
```
```  1994 lemma onorm_vec1: fixes f::"real \<Rightarrow> real"
```
```  1995   shows "onorm (\<lambda>x. vec1 (f (dest_vec1 x))) = onorm f" proof-
```
```  1996   have "\<forall>x::real^1. norm x = 1 \<longleftrightarrow> x\<in>{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:vec_eq_iff)
```
```  1997   hence 1:"{x. norm x = 1} = {vec1 -1, vec1 (1::real)}" by auto
```
```  1998   have 2:"{norm (vec1 (f (dest_vec1 x))) |x. norm x = 1} = (\<lambda>x. norm (vec1 (f (dest_vec1 x)))) ` {x. norm x=1}" by auto
```
```  1999   have "\<forall>x::real. norm x = 1 \<longleftrightarrow> x\<in>{-1, 1}" by auto hence 3:"{x. norm x = 1} = {-1, (1::real)}" by auto
```
```  2000   have 4:"{norm (f x) |x. norm x = 1} = (\<lambda>x. norm (f x)) ` {x. norm x=1}" by auto
```
```  2001   show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max) qed
```
```  2002
```
```  2003 lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)"
```
```  2004   unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto
```
```  2005
```
```  2006 lemma bounded_linear_component_cart[intro]: "bounded_linear (\<lambda>x::real^'n. x \$ k)"
```
```  2007   apply(rule bounded_linearI[where K=1])
```
```  2008   using component_le_norm_cart[of _ k] unfolding real_norm_def by auto
```
```  2009
```
```  2010 lemma bounded_vec1[intro]:  "bounded s \<Longrightarrow> bounded (vec1 ` (s::real set))"
```
```  2011   unfolding bounded_def apply safe apply(rule_tac x="vec1 x" in exI,rule_tac x=e in exI)
```
```  2012   by(auto simp add: dist_real dist_real_def)
```
```  2013
```
```  2014 (*lemma content_closed_interval_cases_cart:
```
```  2015   "content {a..b::real^'n} =
```
```  2016   (if {a..b} = {} then 0 else setprod (\<lambda>i. b\$i - a\$i) UNIV)"
```
```  2017 proof(cases "{a..b} = {}")
```
```  2018   case True thus ?thesis unfolding content_def by auto
```
```  2019 next case Falsethus ?thesis unfolding content_def unfolding if_not_P[OF False]
```
```  2020   proof(cases "\<forall>i. a \$ i \<le> b \$ i")
```
```  2021     case False thus ?thesis unfolding content_def using t by auto
```
```  2022   next case True note interval_eq_empty
```
```  2023    apply auto
```
```  2024
```
```  2025   sorry*)
```
```  2026
```
```  2027 lemma integral_component_eq_cart[simp]: fixes f::"'n::ordered_euclidean_space \<Rightarrow> real^'m"
```
```  2028   assumes "f integrable_on s" shows "integral s (\<lambda>x. f x \$ k) = integral s f \$ k"
```
```  2029   using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] .
```
```  2030
```
```  2031 lemma interval_split_cart:
```
```  2032   "{a..b::real^'n} \<inter> {x. x\$k \<le> c} = {a .. (\<chi> i. if i = k then min (b\$k) c else b\$i)}"
```
```  2033   "{a..b} \<inter> {x. x\$k \<ge> c} = {(\<chi> i. if i = k then max (a\$k) c else a\$i) .. b}"
```
```  2034   apply(rule_tac[!] set_eqI) unfolding Int_iff mem_interval_cart mem_Collect_eq
```
```  2035   unfolding vec_lambda_beta by auto
```
```  2036
```
```  2037 (*lemma content_split_cart:
```
```  2038   "content {a..b::real^'n} = content({a..b} \<inter> {x. x\$k \<le> c}) + content({a..b} \<inter> {x. x\$k >= c})"
```
```  2039 proof- note simps = interval_split_cart content_closed_interval_cases_cart vec_lambda_beta less_eq_vec_def
```
```  2040   { presume "a\<le>b \<Longrightarrow> ?thesis" thus ?thesis apply(cases "a\<le>b") unfolding simps by auto }
```
```  2041   have *:"UNIV = insert k (UNIV - {k})" "\<And>x. finite (UNIV-{x::'n})" "\<And>x. x\<notin>UNIV-{x}" by auto
```
```  2042   have *:"\<And>X Y Z. (\<Prod>i\<in>UNIV. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>UNIV-{k}. Z i (Y i))"
```
```  2043     "(\<Prod>i\<in>UNIV. b\$i - a\$i) = (\<Prod>i\<in>UNIV-{k}. b\$i - a\$i) * (b\$k - a\$k)"
```
```  2044     apply(subst *(1)) defer apply(subst *(1)) unfolding setprod_insert[OF *(2-)] by auto
```
```  2045   assume as:"a\<le>b" moreover have "\<And>x. min (b \$ k) c = max (a \$ k) c
```
```  2046     \<Longrightarrow> x* (b\$k - a\$k) = x*(max (a \$ k) c - a \$ k) + x*(b \$ k - max (a \$ k) c)"
```
```  2047     by  (auto simp add:field_simps)
```
```  2048   moreover have "\<not> a \$ k \<le> c \<Longrightarrow> \<not> c \<le> b \$ k \<Longrightarrow> False"
```
```  2049     unfolding not_le using as[unfolded less_eq_vec_def,rule_format,of k] by auto
```
```  2050   ultimately show ?thesis
```
```  2051     unfolding simps unfolding *(1)[of "\<lambda>i x. b\$i - x"] *(1)[of "\<lambda>i x. x - a\$i"] *(2) by(auto)
```
```  2052 qed*)
```
```  2053
```
```  2054 lemma has_integral_vec1: assumes "(f has_integral k) {a..b}"
```
```  2055   shows "((\<lambda>x. vec1 (f x)) has_integral (vec1 k)) {a..b}"
```
```  2056 proof- have *:"\<And>p. (\<Sum>(x, k)\<in>p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k)"
```
```  2057     unfolding vec_sub vec_eq_iff by(auto simp add: split_beta)
```
```  2058   show ?thesis using assms unfolding has_integral apply safe
```
```  2059     apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
```
```  2060     apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
```
```  2061
```
```  2062 end
```