src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy

Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.

header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}

theory Cartesian_Euclidean_Space
imports Finite_Cartesian_Product Integration
begin

lemma delta_mult_idempotent:
  "(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)

lemma setsum_Plus:
  "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow>
    (\<Sum>x\<in>A <+> B. g x) = (\<Sum>x\<in>A. g (Inl x)) + (\<Sum>x\<in>B. g (Inr x))"
  unfolding Plus_def
  by (subst setsum_Un_disjoint, auto simp add: setsum_reindex)

lemma setsum_UNIV_sum:
  fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
  shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))"
  apply (subst UNIV_Plus_UNIV [symmetric])
  apply (rule setsum_Plus [OF finite finite])
  done

lemma setsum_mult_product:
  "setsum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"
  unfolding sumr_group[of h B A, unfolded atLeast0LessThan, symmetric]
proof (rule setsum_cong, simp, rule setsum_reindex_cong)
  fix i show "inj_on (\<lambda>j. j + i * B) {..<B}" by (auto intro!: inj_onI)
  show "{i * B..<i * B + B} = (\<lambda>j. j + i * B) ` {..<B}"
  proof safe
    fix j assume "j \<in> {i * B..<i * B + B}"
    thus "j \<in> (\<lambda>j. j + i * B) ` {..<B}"
      by (auto intro!: image_eqI[of _ _ "j - i * B"])
  qed simp
qed simp

subsection{* Basic componentwise operations on vectors. *}

instantiation cart :: (times,finite) times
begin
  definition vector_mult_def : "op * \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"
  instance ..
end

instantiation cart :: (one,finite) one
begin
  definition vector_one_def : "1 \<equiv> (\<chi> i. 1)"
  instance ..
end

instantiation cart :: (ord,finite) ord
begin
  definition vector_le_def:
    "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"
  definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)"
  instance by (intro_classes)
end

text{* The ordering on one-dimensional vectors is linear. *}

class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
begin
  subclass finite
  proof from UNIV_one show "finite (UNIV :: 'a set)"
      by (auto intro!: card_ge_0_finite) qed
end

instantiation cart :: (linorder,cart_one) linorder begin
instance proof
  guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+
  hence *:"UNIV = {a}" by auto
  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
  fix x y z::"'a^'b::cart_one" note * = vector_le_def vector_less_def all Cart_eq
  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)
  { assume "x\<le>y" "y\<le>z" thus "x\<le>z" unfolding * by(auto simp only:field_simps) }
  { assume "x\<le>y" "y\<le>x" thus "x=y" unfolding * by(auto simp only:field_simps) }
qed end

text{* Constant Vectors *} 

definition "vec x = (\<chi> i. x)"

text{* Also the scalar-vector multiplication. *}

definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
  where "c *s x = (\<chi> i. c * (x$i))"

subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}

method_setup vector = {*
let
  val ss1 = HOL_basic_ss addsimps [@{thm setsum_addf} RS sym,
  @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib},
  @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]
  val ss2 = @{simpset} addsimps
             [@{thm vector_add_def}, @{thm vector_mult_def},
              @{thm vector_minus_def}, @{thm vector_uminus_def},
              @{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def},
              @{thm vector_scaleR_def},
              @{thm Cart_lambda_beta}, @{thm vector_scalar_mult_def}]
 fun vector_arith_tac ths =
   simp_tac ss1
   THEN' (fn i => rtac @{thm setsum_cong2} i
         ORELSE rtac @{thm setsum_0'} i
         ORELSE simp_tac (HOL_basic_ss addsimps [@{thm "Cart_eq"}]) i)
   (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
   THEN' asm_full_simp_tac (ss2 addsimps ths)
 in
  Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))
 end
*} "Lifts trivial vector statements to real arith statements"

lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)
lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def)

lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector

lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto

lemma vec_add: "vec(x + y) = vec x + vec y"  by (vector vec_def)
lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)
lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def)
lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)

lemma vec_setsum: assumes fS: "finite S"
  shows "vec(setsum f S) = setsum (vec o f) S"
  apply (induct rule: finite_induct[OF fS])
  apply (simp)
  apply (auto simp add: vec_add)
  done

text{* Obvious "component-pushing". *}

lemma vec_component [simp]: "vec x $ i = x"
  by (vector vec_def)

lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
  by vector

lemma vector_smult_component [simp]: "(c *s y)$i = c * (y$i)"
  by vector

lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector

lemmas vector_component =
  vec_component vector_add_component vector_mult_component
  vector_smult_component vector_minus_component vector_uminus_component
  vector_scaleR_component cond_component

subsection {* Some frequently useful arithmetic lemmas over vectors. *}

instance cart :: (semigroup_mult,finite) semigroup_mult
  apply (intro_classes) by (vector mult_assoc)

instance cart :: (monoid_mult,finite) monoid_mult
  apply (intro_classes) by vector+

instance cart :: (ab_semigroup_mult,finite) ab_semigroup_mult
  apply (intro_classes) by (vector mult_commute)

instance cart :: (ab_semigroup_idem_mult,finite) ab_semigroup_idem_mult
  apply (intro_classes) by (vector mult_idem)

instance cart :: (comm_monoid_mult,finite) comm_monoid_mult
  apply (intro_classes) by vector

instance cart :: (semiring,finite) semiring
  apply (intro_classes) by (vector field_simps)+

instance cart :: (semiring_0,finite) semiring_0
  apply (intro_classes) by (vector field_simps)+
instance cart :: (semiring_1,finite) semiring_1
  apply (intro_classes) by vector
instance cart :: (comm_semiring,finite) comm_semiring
  apply (intro_classes) by (vector field_simps)+

instance cart :: (comm_semiring_0,finite) comm_semiring_0 by (intro_classes)
instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
instance cart :: (semiring_0_cancel,finite) semiring_0_cancel by (intro_classes)
instance cart :: (comm_semiring_0_cancel,finite) comm_semiring_0_cancel by (intro_classes)
instance cart :: (ring,finite) ring by (intro_classes)
instance cart :: (semiring_1_cancel,finite) semiring_1_cancel by (intro_classes)
instance cart :: (comm_semiring_1,finite) comm_semiring_1 by (intro_classes)

instance cart :: (ring_1,finite) ring_1 ..

instance cart :: (real_algebra,finite) real_algebra
  apply intro_classes
  apply (simp_all add: vector_scaleR_def field_simps)
  apply vector
  apply vector
  done

instance cart :: (real_algebra_1,finite) real_algebra_1 ..

lemma of_nat_index:
  "(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n"
  apply (induct n)
  apply vector
  apply vector
  done

lemma one_index[simp]:
  "(1 :: 'a::one ^'n)$i = 1" by vector

instance cart :: (semiring_char_0, finite) semiring_char_0
proof
  fix m n :: nat
  show "inj (of_nat :: nat \<Rightarrow> 'a ^ 'b)"
    by (auto intro!: injI simp add: Cart_eq of_nat_index)
qed

instance cart :: (comm_ring_1,finite) comm_ring_1 ..
instance cart :: (ring_char_0,finite) ring_char_0 ..

instance cart :: (real_vector,finite) real_vector ..

lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
  by (vector mult_assoc)
lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x"
  by (vector field_simps)
lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y"
  by (vector field_simps)
lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector
lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector
lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y"
  by (vector field_simps)
lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector
lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector
lemma vector_sneg_minus1: "-x = (- (1::'a::ring_1)) *s x" by vector
lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector
lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x"
  by (vector field_simps)

lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
  by (simp add: Cart_eq)

lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
  by vector
lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
  by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)
lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
  by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"
  by (metis vector_mul_lcancel)
lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
  by (metis vector_mul_rcancel)

lemma component_le_norm_cart: "\<bar>x$i\<bar> <= norm x"
  apply (simp add: norm_vector_def)
  apply (rule member_le_setL2, simp_all)
  done

lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x$i\<bar> <= e"
  by (metis component_le_norm_cart order_trans)

lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
  by (metis component_le_norm_cart basic_trans_rules(21))

lemma norm_le_l1_cart: "norm x <= setsum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
  by (simp add: norm_vector_def setL2_le_setsum)

lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"
  unfolding vector_scaleR_def vector_scalar_mult_def by simp

lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
  unfolding dist_norm scalar_mult_eq_scaleR
  unfolding scaleR_right_diff_distrib[symmetric] by simp

lemma setsum_component [simp]:
  fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"
  shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S"
  by (cases "finite S", induct S set: finite, simp_all)

lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)"
  by (simp add: Cart_eq)

lemma setsum_cmul:
  fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n"
  shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"
  by (simp add: Cart_eq setsum_right_distrib)

(* TODO: use setsum_norm_allsubsets_bound *)
lemma setsum_norm_allsubsets_bound_cart:
  fixes f:: "'a \<Rightarrow> real ^'n"
  assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
  shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"
proof-
  let ?d = "real CARD('n)"
  let ?nf = "\<lambda>x. norm (f x)"
  let ?U = "UNIV :: 'n set"
  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"
    by (rule setsum_commute)
  have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def)
  have "setsum ?nf P \<le> setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $ i\<bar>) ?U) P"
    apply (rule setsum_mono)    by (rule norm_le_l1_cart)
  also have "\<dots> \<le> 2 * ?d * e"
    unfolding th0 th1
  proof(rule setsum_bounded)
    fix i assume i: "i \<in> ?U"
    let ?Pp = "{x. x\<in> P \<and> f x $ i \<ge> 0}"
    let ?Pn = "{x. x \<in> P \<and> f x $ i < 0}"
    have thp: "P = ?Pp \<union> ?Pn" by auto
    have thp0: "?Pp \<inter> ?Pn ={}" by auto
    have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
    have Ppe:"setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp \<le> e"
      using component_le_norm_cart[of "setsum (\<lambda>x. f x) ?Pp" i]  fPs[OF PpP]
      by (auto intro: abs_le_D1)
    have Pne: "setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn \<le> e"
      using component_le_norm_cart[of "setsum (\<lambda>x. - f x) ?Pn" i]  fPs[OF PnP]
      by (auto simp add: setsum_negf intro: abs_le_D1)
    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"
      apply (subst thp)
      apply (rule setsum_Un_zero)
      using fP thp0 by auto
    also have "\<dots> \<le> 2*e" using Pne Ppe by arith
    finally show "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P \<le> 2*e" .
  qed
  finally show ?thesis .
qed

subsection {* A bijection between 'n::finite and {..<CARD('n)} *}

definition cart_bij_nat :: "nat \<Rightarrow> ('n::finite)" where
  "cart_bij_nat = (SOME p. bij_betw p {..<CARD('n)} (UNIV::'n set) )"

abbreviation "\<pi> \<equiv> cart_bij_nat"
definition "\<pi>' = inv_into {..<CARD('n)} (\<pi>::nat \<Rightarrow> ('n::finite))"

lemma bij_betw_pi:
  "bij_betw \<pi> {..<CARD('n::finite)} (UNIV::('n::finite) set)"
  using ex_bij_betw_nat_finite[of "UNIV::'n set"]
  by (auto simp: cart_bij_nat_def atLeast0LessThan
    intro!: someI_ex[of "\<lambda>x. bij_betw x {..<CARD('n)} (UNIV::'n set)"])

lemma bij_betw_pi'[intro]: "bij_betw \<pi>' (UNIV::'n set) {..<CARD('n::finite)}"
  using bij_betw_inv_into[OF bij_betw_pi] unfolding \<pi>'_def by auto

lemma pi'_inj[intro]: "inj \<pi>'"
  using bij_betw_pi' unfolding bij_betw_def by auto

lemma pi'_range[intro]: "\<And>i::'n. \<pi>' i < CARD('n::finite)"
  using bij_betw_pi' unfolding bij_betw_def by auto

lemma \<pi>\<pi>'[simp]: "\<And>i::'n::finite. \<pi> (\<pi>' i) = i"
  using bij_betw_pi by (auto intro!: f_inv_into_f simp: \<pi>'_def bij_betw_def)

lemma \<pi>'\<pi>[simp]: "\<And>i. i\<in>{..<CARD('n::finite)} \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"
  using bij_betw_pi by (auto intro!: inv_into_f_eq simp: \<pi>'_def bij_betw_def)

lemma \<pi>\<pi>'_alt[simp]: "\<And>i. i<CARD('n::finite) \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"
  by auto

lemma \<pi>_inj_on: "inj_on (\<pi>::nat\<Rightarrow>'n::finite) {..<CARD('n)}"
  using bij_betw_pi[where 'n='n] by (simp add: bij_betw_def)

instantiation cart :: (real_basis,finite) real_basis
begin

definition "(basis i::'a^'b) =
  (if i < (CARD('b) * DIM('a))
  then (\<chi> j::'b. if j = \<pi>(i div DIM('a)) then basis (i mod DIM('a)) else 0)
  else 0)"

lemma basis_eq:
  assumes "i < CARD('b)" and "j < DIM('a)"
  shows "basis (j + i * DIM('a)) = (\<chi> k. if k = \<pi> i then basis j else 0)"
proof -
  have "j + i * DIM('a) <  DIM('a) * (i + 1)" using assms by (auto simp: field_simps)
  also have "\<dots> \<le> DIM('a) * CARD('b)" using assms unfolding mult_le_cancel1 by auto
  finally show ?thesis
    unfolding basis_cart_def using assms by (auto simp: Cart_eq not_less field_simps)
qed

lemma basis_eq_pi':
  assumes "j < DIM('a)"
  shows "basis (j + \<pi>' i * DIM('a)) $ k = (if k = i then basis j else 0)"
  apply (subst basis_eq)
  using pi'_range assms by simp_all

lemma split_times_into_modulo[consumes 1]:
  fixes k :: nat
  assumes "k < A * B"
  obtains i j where "i < A" and "j < B" and "k = j + i * B"
proof
  have "A * B \<noteq> 0"
  proof assume "A * B = 0" with assms show False by simp qed
  hence "0 < B" by auto
  thus "k mod B < B" using `0 < B` by auto
next
  have "k div B * B \<le> k div B * B + k mod B" by (rule le_add1)
  also have "... < A * B" using assms by simp
  finally show "k div B < A" by auto
qed simp

lemma split_CARD_DIM[consumes 1]:
  fixes k :: nat
  assumes k: "k < CARD('b) * DIM('a)"
  obtains i and j::'b where "i < DIM('a)" "k = i + \<pi>' j * DIM('a)"
proof -
  from split_times_into_modulo[OF k] guess i j . note ij = this
  show thesis
  proof
    show "j < DIM('a)" using ij by simp
    show "k = j + \<pi>' (\<pi> i :: 'b) * DIM('a)"
      using ij by simp
  qed
qed

lemma linear_less_than_times:
  fixes i j A B :: nat assumes "i < B" "j < A"
  shows "j + i * A < B * A"
proof -
  have "i * A + j < (Suc i)*A" using `j < A` by simp
  also have "\<dots> \<le> B * A" using `i < B` unfolding mult_le_cancel2 by simp
  finally show ?thesis by simp
qed

instance
proof
  let ?b = "basis :: nat \<Rightarrow> 'a^'b"
  let ?b' = "basis :: nat \<Rightarrow> 'a"

  have setsum_basis:
    "\<And>f. (\<Sum>x\<in>range basis. f (x::'a)) = f 0 + (\<Sum>i<DIM('a). f (basis i))"
    unfolding range_basis apply (subst setsum.insert)
    by (auto simp: basis_eq_0_iff setsum.insert setsum_reindex[OF basis_inj])

  have inj: "inj_on ?b {..<CARD('b)*DIM('a)}"
    by (auto intro!: inj_onI elim!: split_CARD_DIM split: split_if_asm
             simp add: Cart_eq basis_eq_pi' all_conj_distrib basis_neq_0
                       inj_on_iff[OF basis_inj])
  moreover
  hence indep: "independent (?b ` {..<CARD('b) * DIM('a)})"
  proof (rule independent_eq_inj_on[THEN iffD2], safe elim!: split_CARD_DIM del: notI)
    fix j and i :: 'b and u :: "'a^'b \<Rightarrow> real" assume "j < DIM('a)"
    let ?x = "j + \<pi>' i * DIM('a)"
    show "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) \<noteq> ?b ?x"
      unfolding Cart_eq not_all
    proof
      have "(\<lambda>j. j + \<pi>' i*DIM('a))`({..<DIM('a)}-{j}) =
        {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)} - {?x}"(is "?S = ?I - _")
      proof safe
        fix y assume "y \<in> ?I"
        moreover def k \<equiv> "y - \<pi>' i*DIM('a)"
        ultimately have "k < DIM('a)" and "y = k + \<pi>' i * DIM('a)" by auto
        moreover assume "y \<notin> ?S"
        ultimately show "y = j + \<pi>' i * DIM('a)" by auto
      qed auto

      have "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) $ i =
          (\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k $ i)" by simp
      also have "\<dots> = (\<Sum>k\<in>?S. u(?b k) *\<^sub>R ?b k $ i)"
        unfolding `?S = ?I - {?x}`
      proof (safe intro!: setsum_mono_zero_cong_right)
        fix y assume "y \<in> {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)}"
        moreover have "Suc (\<pi>' i) * DIM('a) \<le> CARD('b) * DIM('a)"
          unfolding mult_le_cancel2 using pi'_range[of i] by simp
        ultimately show "y < CARD('b) * DIM('a)" by simp
      next
        fix y assume "y < CARD('b) * DIM('a)"
        with split_CARD_DIM guess l k . note y = this
        moreover assume "u (?b y) *\<^sub>R ?b y $ i \<noteq> 0"
        ultimately show "y \<in> {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)}"
          by (auto simp: basis_eq_pi' split: split_if_asm)
      qed simp
      also have "\<dots> = (\<Sum>k\<in>{..<DIM('a)} - {j}. u (?b (k + \<pi>' i*DIM('a))) *\<^sub>R (?b' k))"
        by (subst setsum_reindex) (auto simp: basis_eq_pi' intro!: inj_onI)
      also have "\<dots> \<noteq> ?b ?x $ i"
      proof -
        note independent_eq_inj_on[THEN iffD1, OF basis_inj independent_basis, rule_format]
        note this[of j "\<lambda>v. u (\<chi> ka::'b. if ka = i then v else (0\<Colon>'a))"]
        thus ?thesis by (simp add: `j < DIM('a)` basis_eq pi'_range)
      qed
      finally show "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) $ i \<noteq> ?b ?x $ i" .
    qed
  qed
  ultimately
  show "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}"
    by (auto intro!: exI[of _ "CARD('b) * DIM('a)"] simp: basis_cart_def)

  from indep have exclude_0: "0 \<notin> ?b ` {..<CARD('b) * DIM('a)}"
    using dependent_0[of "?b ` {..<CARD('b) * DIM('a)}"] by blast

  show "span (range ?b) = UNIV"
  proof -
    { fix x :: "'a^'b"
      let "?if i y" = "(\<chi> k::'b. if k = i then ?b' y else (0\<Colon>'a))"
      have The_if: "\<And>i j. j < DIM('a) \<Longrightarrow> (THE k. (?if i j) $ k \<noteq> 0) = i"
        by (rule the_equality) (simp_all split: split_if_asm add: basis_neq_0)
      { fix x :: 'a
        have "x \<in> span (range basis)"
          using span_basis by (auto simp: range_basis)
        hence "\<exists>u. (\<Sum>x<DIM('a). u (?b' x) *\<^sub>R ?b' x) = x"
          by (subst (asm) span_finite) (auto simp: setsum_basis) }
      hence "\<forall>i. \<exists>u. (\<Sum>x<DIM('a). u (?b' x) *\<^sub>R ?b' x) = i" by auto
      then obtain u where u: "\<forall>i. (\<Sum>x<DIM('a). u i (?b' x) *\<^sub>R ?b' x) = i"
        by (auto dest: choice)
      have "\<exists>u. \<forall>i. (\<Sum>j<DIM('a). u (?if i j) *\<^sub>R ?b' j) = x $ i"
        apply (rule exI[of _ "\<lambda>v. let i = (THE i. v$i \<noteq> 0) in u (x$i) (v$i)"])
        using The_if u by simp }
    moreover
    have "\<And>i::'b. {..<CARD('b)} \<inter> {x. i = \<pi> x} = {\<pi>' i}"
      using pi'_range[where 'n='b] by auto
    moreover
    have "range ?b = {0} \<union> ?b ` {..<CARD('b) * DIM('a)}"
      by (auto simp: image_def basis_cart_def)
    ultimately
    show ?thesis
      by (auto simp add: Cart_eq setsum_reindex[OF inj] range_basis
          setsum_mult_product basis_eq if_distrib setsum_cases span_finite
          setsum_reindex[OF basis_inj])
  qed
qed

end

lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a::real_basis)"
proof (safe intro!: dimension_eq elim!: split_times_into_modulo del: notI)
  fix i j assume *: "i < CARD('b)" "j < DIM('a)"
  hence A: "(i * DIM('a) + j) div DIM('a) = i"
    by (subst div_add1_eq) simp
  from * have B: "(i * DIM('a) + j) mod DIM('a) = j"
    unfolding mod_mult_self3 by simp
  show "basis (j + i * DIM('a)) \<noteq> (0::'a^'b)" unfolding basis_cart_def
    using * basis_finite[where 'a='a]
      linear_less_than_times[of i "CARD('b)" j "DIM('a)"]
    by (auto simp: A B field_simps Cart_eq basis_eq_0_iff)
qed (auto simp: basis_cart_def)

lemma if_distr: "(if P then f else g) $ i = (if P then f $ i else g $ i)" by simp

lemma split_dimensions'[consumes 1]:
  assumes "k < DIM('a::real_basis^'b)"
  obtains i j where "i < CARD('b::finite)" and "j < DIM('a::real_basis)" and "k = j + i * DIM('a::real_basis)"
using split_times_into_modulo[OF assms[simplified]] .

lemma cart_euclidean_bound[intro]:
  assumes j:"j < DIM('a::{real_basis})"
  shows "j + \<pi>' (i::'b::finite) * DIM('a) < CARD('b) * DIM('a::real_basis)"
  using linear_less_than_times[OF pi'_range j, of i] .

instance cart :: (real_basis_with_inner,finite) real_basis_with_inner ..

lemma (in real_basis) forall_CARD_DIM:
  "(\<forall>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<forall>(i::'b::finite) j. j<DIM('a) \<longrightarrow> P (j + \<pi>' i * DIM('a)))"
   (is "?l \<longleftrightarrow> ?r")
proof (safe elim!: split_times_into_modulo)
  fix i :: 'b and j assume "j < DIM('a)"
  note linear_less_than_times[OF pi'_range[of i] this]
  moreover assume "?l"
  ultimately show "P (j + \<pi>' i * DIM('a))" by auto
next
  fix i j assume "i < CARD('b)" "j < DIM('a)" and "?r"
  from `?r`[rule_format, OF `j < DIM('a)`, of "\<pi> i"] `i < CARD('b)`
  show "P (j + i * DIM('a))" by simp
qed

lemma (in real_basis) exists_CARD_DIM:
  "(\<exists>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<exists>i::'b::finite. \<exists>j<DIM('a). P (j + \<pi>' i * DIM('a)))"
  using forall_CARD_DIM[where 'b='b, of "\<lambda>x. \<not> P x"] by blast

lemma forall_CARD:
  "(\<forall>i<CARD('b). P i) \<longleftrightarrow> (\<forall>i::'b::finite. P (\<pi>' i))"
  using forall_CARD_DIM[where 'a=real, of P] by simp

lemma exists_CARD:
  "(\<exists>i<CARD('b). P i) \<longleftrightarrow> (\<exists>i::'b::finite. P (\<pi>' i))"
  using exists_CARD_DIM[where 'a=real, of P] by simp

lemmas cart_simps = forall_CARD_DIM exists_CARD_DIM forall_CARD exists_CARD

lemma cart_euclidean_nth[simp]:
  fixes x :: "('a::real_basis_with_inner, 'b::finite) cart"
  assumes j:"j < DIM('a)"
  shows "x $$ (j + \<pi>' i * DIM('a)) = x $ i $$ j"
  unfolding euclidean_component_def inner_vector_def basis_eq_pi'[OF j] if_distrib cond_application_beta
  by (simp add: setsum_cases)

lemma real_euclidean_nth:
  fixes x :: "real^'n"
  shows "x $$ \<pi>' i = (x $ i :: real)"
  using cart_euclidean_nth[where 'a=real, of 0 x i] by simp

lemmas nth_conv_component = real_euclidean_nth[symmetric]

lemma mult_split_eq:
  fixes A :: nat assumes "x < A" "y < A"
  shows "x + i * A = y + j * A \<longleftrightarrow> x = y \<and> i = j"
proof
  assume *: "x + i * A = y + j * A"
  { fix x y i j assume "i < j" "x < A" and *: "x + i * A = y + j * A"
    hence "x + i * A < Suc i * A" using `x < A` by simp
    also have "\<dots> \<le> j * A" using `i < j` unfolding mult_le_cancel2 by simp
    also have "\<dots> \<le> y + j * A" by simp
    finally have "i = j" using * by simp }
  note eq = this

  have "i = j"
  proof (cases rule: linorder_cases)
    assume "i < j" from eq[OF this `x < A` *] show "i = j" by simp
  next
    assume "j < i" from eq[OF this `y < A` *[symmetric]] show "i = j" by simp
  qed simp
  thus "x = y \<and> i = j" using * by simp
qed simp

instance cart :: (euclidean_space,finite) euclidean_space
proof (default, safe elim!: split_dimensions')
  let ?b = "basis :: nat \<Rightarrow> 'a^'b"
  have if_distrib_op: "\<And>f P Q a b c d.
    f (if P then a else b) (if Q then c else d) =
      (if P then if Q then f a c else f a d else if Q then f b c else f b d)"
    by simp

  fix i j k l
  assume "i < CARD('b)" "k < CARD('b)" "j < DIM('a)" "l < DIM('a)"
  thus "?b (j + i * DIM('a)) \<bullet> ?b (l + k * DIM('a)) =
    (if j + i * DIM('a) = l + k * DIM('a) then 1 else 0)"
    using inj_on_iff[OF \<pi>_inj_on[where 'n='b], of k i]
    by (auto simp add: basis_eq inner_vector_def if_distrib_op[of inner] setsum_cases basis_orthonormal mult_split_eq)
qed

instance cart :: (ordered_euclidean_space,finite) ordered_euclidean_space
proof
  fix x y::"'a^'b"
  show "(x \<le> y) = (\<forall>i<DIM(('a, 'b) cart). x $$ i \<le> y $$ i)"
    unfolding vector_le_def apply(subst eucl_le) by (simp add: cart_simps)
  show"(x < y) = (\<forall>i<DIM(('a, 'b) cart). x $$ i < y $$ i)"
    unfolding vector_less_def apply(subst eucl_less) by (simp add: cart_simps)
qed

subsection{* Basis vectors in coordinate directions. *}

definition "cart_basis k = (\<chi> i. if i = k then 1 else 0)"

lemma basis_component [simp]: "cart_basis k $ i = (if k=i then 1 else 0)"
  unfolding cart_basis_def by simp

lemma norm_basis[simp]:
  shows "norm (cart_basis k :: real ^'n) = 1"
  apply (simp add: cart_basis_def norm_eq_sqrt_inner) unfolding inner_vector_def
  apply (vector delta_mult_idempotent)
  using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"] by auto

lemma norm_basis_1: "norm(cart_basis 1 :: real ^'n::{finite,one}) = 1"
  by (rule norm_basis)

lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n). norm x = c"
  by (rule exI[where x="c *\<^sub>R cart_basis arbitrary"]) simp

lemma vector_choose_dist: assumes e: "0 <= e"
  shows "\<exists>(y::real^'n). dist x y = e"
proof-
  from vector_choose_size[OF e] obtain c:: "real ^'n"  where "norm c = e"
    by blast
  then have "dist x (x - c) = e" by (simp add: dist_norm)
  then show ?thesis by blast
qed

lemma basis_inj[intro]: "inj (cart_basis :: 'n \<Rightarrow> real ^'n)"
  by (simp add: inj_on_def Cart_eq)

lemma basis_expansion:
  "setsum (\<lambda>i. (x$i) *s cart_basis i) UNIV = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _")
  by (auto simp add: Cart_eq if_distrib setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong)

lemma smult_conv_scaleR: "c *s x = scaleR c x"
  unfolding vector_scalar_mult_def vector_scaleR_def by simp

lemma basis_expansion':
  "setsum (\<lambda>i. (x$i) *\<^sub>R cart_basis i) UNIV = x"
  by (rule basis_expansion [where 'a=real, unfolded smult_conv_scaleR])

lemma basis_expansion_unique:
  "setsum (\<lambda>i. f i *s cart_basis i) UNIV = (x::('a::comm_ring_1) ^'n) \<longleftrightarrow> (\<forall>i. f i = x$i)"
  by (simp add: Cart_eq setsum_delta if_distrib cong del: if_weak_cong)

lemma dot_basis:
  shows "cart_basis i \<bullet> x = x$i" "x \<bullet> (cart_basis i) = (x$i)"
  by (auto simp add: inner_vector_def cart_basis_def cond_application_beta if_distrib setsum_delta
           cong del: if_weak_cong)

lemma inner_basis:
  fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n"
  shows "inner (cart_basis i) x = inner 1 (x $ i)"
    and "inner x (cart_basis i) = inner (x $ i) 1"
  unfolding inner_vector_def cart_basis_def
  by (auto simp add: cond_application_beta if_distrib setsum_delta cong del: if_weak_cong)

lemma basis_eq_0: "cart_basis i = (0::'a::semiring_1^'n) \<longleftrightarrow> False"
  by (auto simp add: Cart_eq)

lemma basis_nonzero:
  shows "cart_basis k \<noteq> (0:: 'a::semiring_1 ^'n)"
  by (simp add: basis_eq_0)

text {* some lemmas to map between Eucl and Cart *}
lemma basis_real_n[simp]:"(basis (\<pi>' i)::real^'a) = cart_basis i"
  unfolding basis_cart_def using pi'_range[where 'n='a]
  by (auto simp: Cart_eq Cart_lambda_beta)

subsection {* Orthogonality on cartesian products *}

lemma orthogonal_basis:
  shows "orthogonal (cart_basis i) x \<longleftrightarrow> x$i = (0::real)"
  by (auto simp add: orthogonal_def inner_vector_def cart_basis_def if_distrib
                     cond_application_beta setsum_delta cong del: if_weak_cong)

lemma orthogonal_basis_basis:
  shows "orthogonal (cart_basis i :: real^'n) (cart_basis j) \<longleftrightarrow> i \<noteq> j"
  unfolding orthogonal_basis[of i] basis_component[of j] by simp

subsection {* Linearity on cartesian products *}

lemma linear_vmul_component:
  assumes lf: "linear f"
  shows "linear (\<lambda>x. f x $ k *\<^sub>R v)"
  using lf
  by (auto simp add: linear_def algebra_simps)


subsection{* Adjoints on cartesian products *}

text {* TODO: The following lemmas about adjoints should hold for any
Hilbert space (i.e. complete inner product space).
(see \url{http://en.wikipedia.org/wiki/Hermitian_adjoint})
*}

lemma adjoint_works_lemma:
  fixes f:: "real ^'n \<Rightarrow> real ^'m"
  assumes lf: "linear f"
  shows "\<forall>x y. f x \<bullet> y = x \<bullet> adjoint f y"
proof-
  let ?N = "UNIV :: 'n set"
  let ?M = "UNIV :: 'm set"
  have fN: "finite ?N" by simp
  have fM: "finite ?M" by simp
  {fix y:: "real ^ 'm"
    let ?w = "(\<chi> i. (f (cart_basis i) \<bullet> y)) :: real ^ 'n"
    {fix x
      have "f x \<bullet> y = f (setsum (\<lambda>i. (x$i) *\<^sub>R cart_basis i) ?N) \<bullet> y"
        by (simp only: basis_expansion')
      also have "\<dots> = (setsum (\<lambda>i. (x$i) *\<^sub>R f (cart_basis i)) ?N) \<bullet> y"
        unfolding linear_setsum[OF lf fN]
        by (simp add: linear_cmul[OF lf])
      finally have "f x \<bullet> y = x \<bullet> ?w"
        apply (simp only: )
        apply (simp add: inner_vector_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] field_simps)
        done}
  }
  then show ?thesis unfolding adjoint_def
    some_eq_ex[of "\<lambda>f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y"]
    using choice_iff[of "\<lambda>a b. \<forall>x. f x \<bullet> a = x \<bullet> b "]
    by metis
qed

lemma adjoint_works:
  fixes f:: "real ^'n \<Rightarrow> real ^'m"
  assumes lf: "linear f"
  shows "x \<bullet> adjoint f y = f x \<bullet> y"
  using adjoint_works_lemma[OF lf] by metis

lemma adjoint_linear:
  fixes f:: "real ^'n \<Rightarrow> real ^'m"
  assumes lf: "linear f"
  shows "linear (adjoint f)"
  unfolding linear_def vector_eq_ldot[where 'a="real^'n", symmetric] apply safe
  unfolding inner_simps smult_conv_scaleR adjoint_works[OF lf] by auto

lemma adjoint_clauses:
  fixes f:: "real ^'n \<Rightarrow> real ^'m"
  assumes lf: "linear f"
  shows "x \<bullet> adjoint f y = f x \<bullet> y"
  and "adjoint f y \<bullet> x = y \<bullet> f x"
  by (simp_all add: adjoint_works[OF lf] inner_commute)

lemma adjoint_adjoint:
  fixes f:: "real ^'n \<Rightarrow> real ^'m"
  assumes lf: "linear f"
  shows "adjoint (adjoint f) = f"
  by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])


subsection {* Matrix operations *}

text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *}

definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"  (infixl "**" 70)
  where "m ** m' == (\<chi> i j. setsum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"

definition matrix_vector_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"  (infixl "*v" 70)
  where "m *v x \<equiv> (\<chi> i. setsum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"

definition vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "  (infixl "v*" 70)
  where "v v* m == (\<chi> j. setsum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"

definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
definition transpose where 
  "(transpose::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
definition "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))"
definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"
definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
definition "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"

lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)
lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
  by (vector matrix_matrix_mult_def setsum_addf[symmetric] field_simps)

lemma matrix_mul_lid:
  fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
  shows "mat 1 ** A = A"
  apply (simp add: matrix_matrix_mult_def mat_def)
  apply vector
  by (auto simp only: if_distrib cond_application_beta setsum_delta'[OF finite]  mult_1_left mult_zero_left if_True UNIV_I)


lemma matrix_mul_rid:
  fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
  shows "A ** mat 1 = A"
  apply (simp add: matrix_matrix_mult_def mat_def)
  apply vector
  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)

lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
  apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)
  apply (subst setsum_commute)
  apply simp
  done

lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
  apply (vector matrix_matrix_mult_def matrix_vector_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)
  apply (subst setsum_commute)
  apply simp
  done

lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
  apply (vector matrix_vector_mult_def mat_def)
  by (simp add: if_distrib cond_application_beta
    setsum_delta' cong del: if_weak_cong)

lemma matrix_transpose_mul: "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
  by (simp add: matrix_matrix_mult_def transpose_def Cart_eq mult_commute)

lemma matrix_eq:
  fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
  shows "A = B \<longleftrightarrow>  (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")
  apply auto
  apply (subst Cart_eq)
  apply clarify
  apply (clarsimp simp add: matrix_vector_mult_def cart_basis_def if_distrib cond_application_beta Cart_eq cong del: if_weak_cong)
  apply (erule_tac x="cart_basis ia" in allE)
  apply (erule_tac x="i" in allE)
  by (auto simp add: cart_basis_def if_distrib cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong)

lemma matrix_vector_mul_component:
  shows "((A::real^_^_) *v x)$k = (A$k) \<bullet> x"
  by (simp add: matrix_vector_mult_def inner_vector_def)

lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
  apply (simp add: inner_vector_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
  apply (subst setsum_commute)
  by simp

lemma transpose_mat: "transpose (mat n) = mat n"
  by (vector transpose_def mat_def)

lemma transpose_transpose: "transpose(transpose A) = A"
  by (vector transpose_def)

lemma row_transpose:
  fixes A:: "'a::semiring_1^_^_"
  shows "row i (transpose A) = column i A"
  by (simp add: row_def column_def transpose_def Cart_eq)

lemma column_transpose:
  fixes A:: "'a::semiring_1^_^_"
  shows "column i (transpose A) = row i A"
  by (simp add: row_def column_def transpose_def Cart_eq)

lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
by (auto simp add: rows_def columns_def row_transpose intro: set_ext)

lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" by (metis transpose_transpose rows_transpose)

text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *}

lemma matrix_mult_dot: "A *v x = (\<chi> i. A$i \<bullet> x)"
  by (simp add: matrix_vector_mult_def inner_vector_def)

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)"
  by (simp add: matrix_vector_mult_def Cart_eq column_def mult_commute)

lemma vector_componentwise:
  "(x::'a::ring_1^'n) = (\<chi> j. setsum (\<lambda>i. (x$i) * (cart_basis i :: 'a^'n)$j) (UNIV :: 'n set))"
  apply (subst basis_expansion[symmetric])
  by (vector Cart_eq setsum_component)

lemma linear_componentwise:
  fixes f:: "real ^'m \<Rightarrow> real ^ _"
  assumes lf: "linear f"
  shows "(f x)$j = setsum (\<lambda>i. (x$i) * (f (cart_basis i)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
proof-
  let ?M = "(UNIV :: 'm set)"
  let ?N = "(UNIV :: 'n set)"
  have fM: "finite ?M" by simp
  have "?rhs = (setsum (\<lambda>i.(x$i) *\<^sub>R f (cart_basis i) ) ?M)$j"
    unfolding vector_smult_component[symmetric] smult_conv_scaleR
    unfolding setsum_component[of "(\<lambda>i.(x$i) *\<^sub>R f (cart_basis i :: real^'m))" ?M]
    ..
  then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion' ..
qed

text{* Inverse matrices  (not necessarily square) *}

definition "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"

definition "matrix_inv(A:: 'a::semiring_1^'n^'m) =
        (SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"

text{* Correspondence between matrices and linear operators. *}

definition matrix:: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
where "matrix f = (\<chi> i j. (f(cart_basis j))$i)"

lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
  by (simp add: linear_def matrix_vector_mult_def Cart_eq field_simps setsum_right_distrib setsum_addf)

lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::real ^ 'n)"
apply (simp add: matrix_def matrix_vector_mult_def Cart_eq mult_commute)
apply clarify
apply (rule linear_componentwise[OF lf, symmetric])
done

lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))" by (simp add: ext matrix_works)

lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"
  by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)

lemma matrix_compose:
  assumes lf: "linear (f::real^'n \<Rightarrow> real^'m)"
  and lg: "linear (g::real^'m \<Rightarrow> real^_)"
  shows "matrix (g o f) = matrix g ** matrix f"
  using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]]
  by (simp  add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)

lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
  by (simp add: matrix_vector_mult_def transpose_def Cart_eq mult_commute)

lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
  apply (rule adjoint_unique)
  apply (simp add: transpose_def inner_vector_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)
  apply (subst setsum_commute)
  apply (auto simp add: mult_ac)
  done

lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
  shows "matrix(adjoint f) = transpose(matrix f)"
  apply (subst matrix_vector_mul[OF lf])
  unfolding adjoint_matrix matrix_of_matrix_vector_mul ..

section {* lambda skolemization on cartesian products *}

(* FIXME: rename do choice_cart *)

lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
   (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
  let ?S = "(UNIV :: 'n set)"
  {assume H: "?rhs"
    then have ?lhs by auto}
  moreover
  {assume H: "?lhs"
    then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
    let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
    {fix i
      from f have "P i (f i)" by metis
      then have "P i (?x $ i)" by auto
    }
    hence "\<forall>i. P i (?x$i)" by metis
    hence ?rhs by metis }
  ultimately show ?thesis by metis
qed

subsection {* Standard bases are a spanning set, and obviously finite. *}

lemma span_stdbasis:"span {cart_basis i :: real^'n | i. i \<in> (UNIV :: 'n set)} = UNIV"
apply (rule set_ext)
apply auto
apply (subst basis_expansion'[symmetric])
apply (rule span_setsum)
apply simp
apply auto
apply (rule span_mul)
apply (rule span_superset)
apply (auto simp add: Collect_def mem_def)
done

lemma finite_stdbasis: "finite {cart_basis i ::real^'n |i. i\<in> (UNIV:: 'n set)}" (is "finite ?S")
proof-
  have eq: "?S = cart_basis ` UNIV" by blast
  show ?thesis unfolding eq by auto
qed

lemma card_stdbasis: "card {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)} = CARD('n)" (is "card ?S = _")
proof-
  have eq: "?S = cart_basis ` UNIV" by blast
  show ?thesis unfolding eq using card_image[OF basis_inj] by simp
qed


lemma independent_stdbasis_lemma:
  assumes x: "(x::real ^ 'n) \<in> span (cart_basis ` S)"
  and iS: "i \<notin> S"
  shows "(x$i) = 0"
proof-
  let ?U = "UNIV :: 'n set"
  let ?B = "cart_basis ` S"
  let ?P = "\<lambda>(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0"
 {fix x::"real^_" assume xS: "x\<in> ?B"
   from xS have "?P x" by auto}
 moreover
 have "subspace ?P"
   by (auto simp add: subspace_def Collect_def mem_def)
 ultimately show ?thesis
   using x span_induct[of ?B ?P x] iS by blast
qed

lemma independent_stdbasis: "independent {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)}"
proof-
  let ?I = "UNIV :: 'n set"
  let ?b = "cart_basis :: _ \<Rightarrow> real ^'n"
  let ?B = "?b ` ?I"
  have eq: "{?b i|i. i \<in> ?I} = ?B"
    by auto
  {assume d: "dependent ?B"
    then obtain k where k: "k \<in> ?I" "?b k \<in> span (?B - {?b k})"
      unfolding dependent_def by auto
    have eq1: "?B - {?b k} = ?B - ?b ` {k}"  by simp
    have eq2: "?B - {?b k} = ?b ` (?I - {k})"
      unfolding eq1
      apply (rule inj_on_image_set_diff[symmetric])
      apply (rule basis_inj) using k(1) by auto
    from k(2) have th0: "?b k \<in> span (?b ` (?I - {k}))" unfolding eq2 .
    from independent_stdbasis_lemma[OF th0, of k, simplified]
    have False by simp}
  then show ?thesis unfolding eq dependent_def ..
qed

lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
  unfolding inner_simps smult_conv_scaleR by auto

lemma linear_eq_stdbasis_cart:
  assumes lf: "linear (f::real^'m \<Rightarrow> _)" and lg: "linear g"
  and fg: "\<forall>i. f (cart_basis i) = g(cart_basis i)"
  shows "f = g"
proof-
  let ?U = "UNIV :: 'm set"
  let ?I = "{cart_basis i:: real^'m|i. i \<in> ?U}"
  {fix x assume x: "x \<in> (UNIV :: (real^'m) set)"
    from equalityD2[OF span_stdbasis]
    have IU: " (UNIV :: (real^'m) set) \<subseteq> span ?I" by blast
    from linear_eq[OF lf lg IU] fg x
    have "f x = g x" unfolding Collect_def  Ball_def mem_def by metis}
  then show ?thesis by (auto intro: ext)
qed

lemma bilinear_eq_stdbasis_cart:
  assumes bf: "bilinear (f:: real^'m \<Rightarrow> real^'n \<Rightarrow> _)"
  and bg: "bilinear g"
  and fg: "\<forall>i j. f (cart_basis i) (cart_basis j) = g (cart_basis i) (cart_basis j)"
  shows "f = g"
proof-
  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
  from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by (blast intro: ext)
qed

lemma left_invertible_transpose:
  "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
  by (metis matrix_transpose_mul transpose_mat transpose_transpose)

lemma right_invertible_transpose:
  "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
  by (metis matrix_transpose_mul transpose_mat transpose_transpose)

lemma matrix_left_invertible_injective:
"(\<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)"
proof-
  {fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y"
    from xy have "B*v (A *v x) = B *v (A*v y)" by simp
    hence "x = y"
      unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid .}
  moreover
  {assume A: "\<forall>x y. A *v x = A *v y \<longrightarrow> x = y"
    hence i: "inj (op *v A)" unfolding inj_on_def by auto
    from linear_injective_left_inverse[OF matrix_vector_mul_linear i]
    obtain g where g: "linear g" "g o op *v A = id" by blast
    have "matrix g ** A = mat 1"
      unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
      using g(2) by (simp add: o_def id_def stupid_ext)
    then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast}
  ultimately show ?thesis by blast
qed

lemma matrix_left_invertible_ker:
  "(\<exists>B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"
  unfolding matrix_left_invertible_injective
  using linear_injective_0[OF matrix_vector_mul_linear, of A]
  by (simp add: inj_on_def)

lemma matrix_right_invertible_surjective:
"(\<exists>B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
proof-
  {fix B :: "real ^'m^'n"  assume AB: "A ** B = mat 1"
    {fix x :: "real ^ 'm"
      have "A *v (B *v x) = x"
        by (simp add: matrix_vector_mul_lid matrix_vector_mul_assoc AB)}
    hence "surj (op *v A)" unfolding surj_def by metis }
  moreover
  {assume sf: "surj (op *v A)"
    from linear_surjective_right_inverse[OF matrix_vector_mul_linear sf]
    obtain g:: "real ^'m \<Rightarrow> real ^'n" where g: "linear g" "op *v A o g = id"
      by blast

    have "A ** (matrix g) = mat 1"
      unfolding matrix_eq  matrix_vector_mul_lid
        matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
      using g(2) unfolding o_def stupid_ext[symmetric] id_def
      .
    hence "\<exists>B. A ** (B::real^'m^'n) = mat 1" by blast
  }
  ultimately show ?thesis unfolding surj_def by blast
qed

lemma matrix_left_invertible_independent_columns:
  fixes A :: "real^'n^'m"
  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))"
   (is "?lhs \<longleftrightarrow> ?rhs")
proof-
  let ?U = "UNIV :: 'n set"
  {assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0"
    {fix c i assume c: "setsum (\<lambda>i. c i *s column i A) ?U = 0"
      and i: "i \<in> ?U"
      let ?x = "\<chi> i. c i"
      have th0:"A *v ?x = 0"
        using c
        unfolding matrix_mult_vsum Cart_eq
        by auto
      from k[rule_format, OF th0] i
      have "c i = 0" by (vector Cart_eq)}
    hence ?rhs by blast}
  moreover
  {assume H: ?rhs
    {fix x assume x: "A *v x = 0"
      let ?c = "\<lambda>i. ((x$i ):: real)"
      from H[rule_format, of ?c, unfolded matrix_mult_vsum[symmetric], OF x]
      have "x = 0" by vector}}
  ultimately show ?thesis unfolding matrix_left_invertible_ker by blast
qed

lemma matrix_right_invertible_independent_rows:
  fixes A :: "real^'n^'m"
  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))"
  unfolding left_invertible_transpose[symmetric]
    matrix_left_invertible_independent_columns
  by (simp add: column_transpose)

lemma matrix_right_invertible_span_columns:
  "(\<exists>(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \<longleftrightarrow> span (columns A) = UNIV" (is "?lhs = ?rhs")
proof-
  let ?U = "UNIV :: 'm set"
  have fU: "finite ?U" by simp
  have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::real^'m). setsum (\<lambda>i. (x$i) *s column i A) ?U = y)"
    unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def
    apply (subst eq_commute) ..
  have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> span (columns A))" by blast
  {assume h: ?lhs
    {fix x:: "real ^'n"
        from h[unfolded lhseq, rule_format, of x] obtain y:: "real ^'m"
          where y: "setsum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
        have "x \<in> span (columns A)"
          unfolding y[symmetric]
          apply (rule span_setsum[OF fU])
          apply clarify
          unfolding smult_conv_scaleR
          apply (rule span_mul)
          apply (rule span_superset)
          unfolding columns_def
          by blast}
    then have ?rhs unfolding rhseq by blast}
  moreover
  {assume h:?rhs
    let ?P = "\<lambda>(y::real ^'n). \<exists>(x::real^'m). setsum (\<lambda>i. (x$i) *s column i A) ?U = y"
    {fix y have "?P y"
      proof(rule span_induct_alt[of ?P "columns A", folded smult_conv_scaleR])
        show "\<exists>x\<Colon>real ^ 'm. setsum (\<lambda>i. (x$i) *s column i A) ?U = 0"
          by (rule exI[where x=0], simp)
      next
        fix c y1 y2 assume y1: "y1 \<in> columns A" and y2: "?P y2"
        from y1 obtain i where i: "i \<in> ?U" "y1 = column i A"
          unfolding columns_def by blast
        from y2 obtain x:: "real ^'m" where
          x: "setsum (\<lambda>i. (x$i) *s column i A) ?U = y2" by blast
        let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::real^'m"
        show "?P (c*s y1 + y2)"
          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)
            fix j
            have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
           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)
              by (simp add: field_simps)
            have "setsum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
           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"
              apply (rule setsum_cong[OF refl])
              using th by blast
            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"
              by (simp add: setsum_addf)
            also have "\<dots> = c * ((column i A)$j) + setsum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
              unfolding setsum_delta[OF fU]
              using i(1) by simp
            finally show "setsum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
           else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + setsum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" .
          qed
        next
          show "y \<in> span (columns A)" unfolding h by blast
        qed}
    then have ?lhs unfolding lhseq ..}
  ultimately show ?thesis by blast
qed

lemma matrix_left_invertible_span_rows:
  "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
  unfolding right_invertible_transpose[symmetric]
  unfolding columns_transpose[symmetric]
  unfolding matrix_right_invertible_span_columns
 ..

text {* The same result in terms of square matrices. *}

lemma matrix_left_right_inverse:
  fixes A A' :: "real ^'n^'n"
  shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1"
proof-
  {fix A A' :: "real ^'n^'n" assume AA': "A ** A' = mat 1"
    have sA: "surj (op *v A)"
      unfolding surj_def
      apply clarify
      apply (rule_tac x="(A' *v y)" in exI)
      by (simp add: matrix_vector_mul_assoc AA' matrix_vector_mul_lid)
    from linear_surjective_isomorphism[OF matrix_vector_mul_linear sA]
    obtain f' :: "real ^'n \<Rightarrow> real ^'n"
      where f': "linear f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
    have th: "matrix f' ** A = mat 1"
      by (simp add: matrix_eq matrix_works[OF f'(1)] matrix_vector_mul_assoc[symmetric] matrix_vector_mul_lid f'(2)[rule_format])
    hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp
    hence "matrix f' = A'" by (simp add: matrix_mul_assoc[symmetric] AA' matrix_mul_rid matrix_mul_lid)
    hence "matrix f' ** A = A' ** A" by simp
    hence "A' ** A = mat 1" by (simp add: th)}
  then show ?thesis by blast
qed

text {* Considering an n-element vector as an n-by-1 or 1-by-n matrix. *}

definition "rowvector v = (\<chi> i j. (v$j))"

definition "columnvector v = (\<chi> i j. (v$i))"

lemma transpose_columnvector:
 "transpose(columnvector v) = rowvector v"
  by (simp add: transpose_def rowvector_def columnvector_def Cart_eq)

lemma transpose_rowvector: "transpose(rowvector v) = columnvector v"
  by (simp add: transpose_def columnvector_def rowvector_def Cart_eq)

lemma dot_rowvector_columnvector:
  "columnvector (A *v v) = A ** columnvector v"
  by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)

lemma dot_matrix_product: "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1"
  by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vector_def)

lemma dot_matrix_vector_mul:
  fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
  shows "(A *v x) \<bullet> (B *v y) =
      (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
unfolding dot_matrix_product transpose_columnvector[symmetric]
  dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..


lemma infnorm_cart:"infnorm (x::real^'n) = Sup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
  unfolding infnorm_def apply(rule arg_cong[where f=Sup]) apply safe
  apply(rule_tac x="\<pi> i" in exI) defer
  apply(rule_tac x="\<pi>' i" in exI) unfolding nth_conv_component using pi'_range by auto

lemma infnorm_set_image_cart:
  "{abs(x$i) |i. i\<in> (UNIV :: _ set)} =
  (\<lambda>i. abs(x$i)) ` (UNIV)" by blast

lemma infnorm_set_lemma_cart:
  shows "finite {abs((x::'a::abs ^'n)$i) |i. i\<in> (UNIV :: 'n set)}"
  and "{abs(x$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}"
  unfolding  infnorm_set_image_cart
  by (auto intro: finite_imageI)

lemma component_le_infnorm_cart:
  shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"
  unfolding nth_conv_component
  using component_le_infnorm[of x] .

instance cart :: (perfect_space, finite) perfect_space
proof
  fix x :: "'a ^ 'b"
  {
    fix e :: real assume "0 < e"
    def a \<equiv> "x $ undefined"
    have "a islimpt UNIV" by (rule islimpt_UNIV)
    with `0 < e` obtain b where "b \<noteq> a" and "dist b a < e"
      unfolding islimpt_approachable by auto
    def y \<equiv> "Cart_lambda ((Cart_nth x)(undefined := b))"
    from `b \<noteq> a` have "y \<noteq> x"
      unfolding a_def y_def by (simp add: Cart_eq)
    from `dist b a < e` have "dist y x < e"
      unfolding dist_vector_def a_def y_def
      apply simp
      apply (rule le_less_trans [OF setL2_le_setsum [OF zero_le_dist]])
      apply (subst setsum_diff1' [where a=undefined], simp, simp, simp)
      done
    from `y \<noteq> x` and `dist y x < e`
    have "\<exists>y\<in>UNIV. y \<noteq> x \<and> dist y x < e" by auto
  }
  then show "x islimpt UNIV" unfolding islimpt_approachable by blast
qed

lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
proof-
  let ?U = "UNIV :: 'n set"
  let ?O = "{x::real^'n. \<forall>i. x$i\<ge>0}"
  {fix x:: "real^'n" and i::'n assume H: "\<forall>e>0. \<exists>x'\<in>?O. x' \<noteq> x \<and> dist x' x < e"
    and xi: "x$i < 0"
    from xi have th0: "-x$i > 0" by arith
    from H[rule_format, OF th0] obtain x' where x': "x' \<in>?O" "x' \<noteq> x" "dist x' x < -x $ i" by blast
      have th:" \<And>b a (x::real). abs x <= b \<Longrightarrow> b <= a ==> ~(a + x < 0)" by arith
      have th': "\<And>x (y::real). x < 0 \<Longrightarrow> 0 <= y ==> abs x <= abs (y - x)" by arith
      have th1: "\<bar>x$i\<bar> \<le> \<bar>(x' - x)$i\<bar>" using x'(1) xi
        apply (simp only: vector_component)
        by (rule th') auto
      have th2: "\<bar>dist x x'\<bar> \<ge> \<bar>(x' - x)$i\<bar>" using  component_le_norm_cart[of "x'-x" i]
        apply (simp add: dist_norm) by norm
      from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) }
  then show ?thesis unfolding closed_limpt islimpt_approachable
    unfolding not_le[symmetric] by blast
qed
lemma Lim_component_cart:
  fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
  shows "(f ---> l) net \<Longrightarrow> ((\<lambda>a. f a $i) ---> l$i) net"
  unfolding tendsto_iff
  apply (clarify)
  apply (drule spec, drule (1) mp)
  apply (erule eventually_elim1)
  apply (erule le_less_trans [OF dist_nth_le_cart])
  done

lemma bounded_component_cart: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x $ i) ` s)"
unfolding bounded_def
apply clarify
apply (rule_tac x="x $ i" in exI)
apply (rule_tac x="e" in exI)
apply clarify
apply (rule order_trans [OF dist_nth_le_cart], simp)
done

lemma compact_lemma_cart:
  fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
  assumes "bounded s" and "\<forall>n. f n \<in> s"
  shows "\<forall>d.
        \<exists>l r. subseq r \<and>
        (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
proof
  fix d::"'n set" have "finite d" by simp
  thus "\<exists>l::'a ^ 'n. \<exists>r. subseq r \<and>
      (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
  proof(induct d) case empty thus ?case unfolding subseq_def by auto
  next case (insert k d)
    have s': "bounded ((\<lambda>x. x $ k) ` s)" using `bounded s` by (rule bounded_component_cart)
    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"
      using insert(3) by auto
    have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` s" using `\<forall>n. f n \<in> s` by simp
    obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) $ k) ---> l2) sequentially"
      using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
    def r \<equiv> "r1 \<circ> r2" have r:"subseq r"
      using r1 and r2 unfolding r_def o_def subseq_def by auto
    moreover
    def l \<equiv> "(\<chi> i. if i = k then l2 else l1$i)::'a^'n"
    { fix e::real assume "e>0"
      from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially" by blast
      from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) $ k) l2 < e) sequentially" by (rule tendstoD)
      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) $ i) (l1 $ i) < e) sequentially"
        by (rule eventually_subseq)
      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) $ i) (l $ i) < e) sequentially"
        using N1' N2 by (rule eventually_elim2, simp add: l_def r_def)
    }
    ultimately show ?case by auto
  qed
qed

instance cart :: (heine_borel, finite) heine_borel
proof
  fix s :: "('a ^ 'b) set" and f :: "nat \<Rightarrow> 'a ^ 'b"
  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
  then obtain l r where r: "subseq r"
    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially"
    using compact_lemma_cart [OF s f] by blast
  let ?d = "UNIV::'b set"
  { fix e::real assume "e>0"
    hence "0 < e / (real_of_nat (card ?d))"
      using zero_less_card_finite using divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto
    with l have "eventually (\<lambda>n. \<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))) sequentially"
      by simp
    moreover
    { fix n assume n: "\<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))"
      have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) $ i) (l $ i))"
        unfolding dist_vector_def using zero_le_dist by (rule setL2_le_setsum)
      also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
        by (rule setsum_strict_mono) (simp_all add: n)
      finally have "dist (f (r n)) l < e" by simp
    }
    ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
      by (rule eventually_elim1)
  }
  hence *:"((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp
  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto
qed

lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
unfolding continuous_at by (intro tendsto_intros)

lemma continuous_on_component: "continuous_on s (\<lambda>x. x $ i)"
unfolding continuous_on_def by (intro ballI tendsto_intros)

lemma interval_cart: fixes a :: "'a::ord^'n" shows
  "{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
  "{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
  by (auto simp add: expand_set_eq vector_less_def vector_le_def)

lemma mem_interval_cart: fixes a :: "'a::ord^'n" shows
  "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
  "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
  using interval_cart[of a b] by(auto simp add: expand_set_eq vector_less_def vector_le_def)

lemma interval_eq_empty_cart: fixes a :: "real^'n" shows
 "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
 "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
proof-
  { fix i x assume as:"b$i \<le> a$i" and x:"x\<in>{a <..< b}"
    hence "a $ i < x $ i \<and> x $ i < b $ i" unfolding mem_interval_cart by auto
    hence "a$i < b$i" by auto
    hence False using as by auto  }
  moreover
  { assume as:"\<forall>i. \<not> (b$i \<le> a$i)"
    let ?x = "(1/2) *\<^sub>R (a + b)"
    { fix i
      have "a$i < b$i" using as[THEN spec[where x=i]] by auto
      hence "a$i < ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i < b$i"
        unfolding vector_smult_component and vector_add_component
        by auto  }
    hence "{a <..< b} \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto  }
  ultimately show ?th1 by blast

  { fix i x assume as:"b$i < a$i" and x:"x\<in>{a .. b}"
    hence "a $ i \<le> x $ i \<and> x $ i \<le> b $ i" unfolding mem_interval_cart by auto
    hence "a$i \<le> b$i" by auto
    hence False using as by auto  }
  moreover
  { assume as:"\<forall>i. \<not> (b$i < a$i)"
    let ?x = "(1/2) *\<^sub>R (a + b)"
    { fix i
      have "a$i \<le> b$i" using as[THEN spec[where x=i]] by auto
      hence "a$i \<le> ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i \<le> b$i"
        unfolding vector_smult_component and vector_add_component
        by auto  }
    hence "{a .. b} \<noteq> {}" using mem_interval_cart(2)[of "?x" a b] by auto  }
  ultimately show ?th2 by blast
qed

lemma interval_ne_empty_cart: fixes a :: "real^'n" shows
  "{a  ..  b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i \<le> b$i)" and
  "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i < b$i)"
  unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le)
    (* BH: Why doesn't just "auto" work here? *)

lemma subset_interval_imp_cart: fixes a :: "real^'n" shows
 "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}" and
 "(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}" and
 "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}" and
 "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
  unfolding subset_eq[unfolded Ball_def] unfolding mem_interval_cart
  by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)

lemma interval_sing: fixes a :: "'a::linorder^'n" shows
 "{a .. a} = {a} \<and> {a<..<a} = {}"
apply(auto simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
apply (simp add: order_eq_iff)
apply (auto simp add: not_less less_imp_le)
done

lemma interval_open_subset_closed_cart:  fixes a :: "'a::preorder^'n" shows
 "{a<..<b} \<subseteq> {a .. b}"
proof(simp add: subset_eq, rule)
  fix x
  assume x:"x \<in>{a<..<b}"
  { fix i
    have "a $ i \<le> x $ i"
      using x order_less_imp_le[of "a$i" "x$i"]
      by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
  }
  moreover
  { fix i
    have "x $ i \<le> b $ i"
      using x order_less_imp_le[of "x$i" "b$i"]
      by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
  }
  ultimately
  show "a \<le> x \<and> x \<le> b"
    by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
qed

lemma subset_interval_cart: fixes a :: "real^'n" shows
 "{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
 "{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
 "{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
 "{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)
  using subset_interval[of c d a b] by (simp_all add: cart_simps real_euclidean_nth)

lemma disjoint_interval_cart: fixes a::"real^'n" shows
  "{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
  "{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
  "{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
  "{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)
  using disjoint_interval[of a b c d] by (simp_all add: cart_simps real_euclidean_nth)

lemma inter_interval_cart: fixes a :: "'a::linorder^'n" shows
 "{a .. b} \<inter> {c .. d} =  {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
  unfolding expand_set_eq and Int_iff and mem_interval_cart
  by auto

lemma closed_interval_left_cart: fixes b::"real^'n"
  shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}"
proof-
  { fix i
    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"
    { assume "x$i > b$i"
      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
      hence False using component_le_norm_cart[of "y - x" i] unfolding dist_norm and vector_minus_component by auto   }
    hence "x$i \<le> b$i" by(rule ccontr)auto  }
  thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
qed

lemma closed_interval_right_cart: fixes a::"real^'n"
  shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}"
proof-
  { fix i
    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"
    { assume "a$i > x$i"
      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
      hence False using component_le_norm_cart[of "y - x" i] unfolding dist_norm and vector_minus_component by auto   }
    hence "a$i \<le> x$i" by(rule ccontr)auto  }
  thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
qed

lemma is_interval_cart:"is_interval (s::(real^'n) set) \<longleftrightarrow>
  (\<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)"
  unfolding is_interval_def Ball_def by (simp add: cart_simps real_euclidean_nth)

lemma closed_halfspace_component_le_cart:
  shows "closed {x::real^'n. x$i \<le> a}"
  using closed_halfspace_le[of "(cart_basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto

lemma closed_halfspace_component_ge_cart:
  shows "closed {x::real^'n. x$i \<ge> a}"
  using closed_halfspace_ge[of a "(cart_basis i)::real^'n"] unfolding inner_basis[OF assms] by auto

lemma open_halfspace_component_lt_cart:
  shows "open {x::real^'n. x$i < a}"
  using open_halfspace_lt[of "(cart_basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto

lemma open_halfspace_component_gt_cart:
  shows "open {x::real^'n. x$i  > a}"
  using open_halfspace_gt[of a "(cart_basis i)::real^'n"] unfolding inner_basis[OF assms] by auto

lemma Lim_component_le_cart: fixes f :: "'a \<Rightarrow> real^'n"
  assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)$i \<le> b) net"
  shows "l$i \<le> b"
proof-
  { 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
  show ?thesis using Lim_in_closed_set[of "{x. inner (cart_basis i) x \<le> b}" f net l] unfolding *
    using closed_halfspace_le[of "(cart_basis i)::real^'n" b] and assms(1,2,3) by auto
qed

lemma Lim_component_ge_cart: fixes f :: "'a \<Rightarrow> real^'n"
  assumes "(f ---> l) net"  "\<not> (trivial_limit net)"  "eventually (\<lambda>x. b \<le> (f x)$i) net"
  shows "b \<le> l$i"
proof-
  { 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
  show ?thesis using Lim_in_closed_set[of "{x. inner (cart_basis i) x \<ge> b}" f net l] unfolding *
    using closed_halfspace_ge[of b "(cart_basis i)::real^'n"] and assms(1,2,3) by auto
qed

lemma Lim_component_eq_cart: fixes f :: "'a \<Rightarrow> real^'n"
  assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)$i = b) net"
  shows "l$i = b"
  using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge_cart[OF net, of b i] and
    Lim_component_le_cart[OF net, of i b] by auto

lemma connected_ivt_component_cart: fixes x::"real^'n" shows
 "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)"
  using connected_ivt_hyperplane[of s x y "(cart_basis k)::real^'n" a] by (auto simp add: inner_basis)

lemma subspace_substandard_cart:
 "subspace {x::real^_. (\<forall>i. P i \<longrightarrow> x$i = 0)}"
  unfolding subspace_def by auto

lemma closed_substandard_cart:
 "closed {x::real^'n. \<forall>i. P i --> x$i = 0}" (is "closed ?A")
proof-
  let ?D = "{i. P i}"
  let ?Bs = "{{x::real^'n. inner (cart_basis i) x = 0}| i. i \<in> ?D}"
  { fix x
    { assume "x\<in>?A"
      hence x:"\<forall>i\<in>?D. x $ i = 0" by auto
      hence "x\<in> \<Inter> ?Bs" by(auto simp add: inner_basis x) }
    moreover
    { assume x:"x\<in>\<Inter>?Bs"
      { fix i assume i:"i \<in> ?D"
        then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::real^'n. inner (cart_basis i) x = 0}" by auto
        hence "x $ i = 0" unfolding B using x unfolding inner_basis by auto  }
      hence "x\<in>?A" by auto }
    ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" .. }
  hence "?A = \<Inter> ?Bs" by auto
  thus ?thesis by(auto simp add: closed_Inter closed_hyperplane)
qed

lemma dim_substandard_cart:
  shows "dim {x::real^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d" (is "dim ?A = _")
proof- have *:"{x. \<forall>i<DIM((real, 'n) cart). i \<notin> \<pi>' ` d \<longrightarrow> x $$ i = 0} = 
    {x::real^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0}"apply safe
    apply(erule_tac x="\<pi>' i" in allE) defer
    apply(erule_tac x="\<pi> i" in allE)
    unfolding image_iff real_euclidean_nth[symmetric] by (auto simp: pi'_inj[THEN inj_eq])
  have " \<pi>' ` d \<subseteq> {..<DIM((real, 'n) cart)}" using pi'_range[where 'n='n] by auto
  thus ?thesis using dim_substandard[of "\<pi>' ` d", where 'a="real^'n"] 
    unfolding * using card_image[of "\<pi>'" d] using pi'_inj unfolding inj_on_def by auto
qed

lemma affinity_inverses:
  assumes m0: "m \<noteq> (0::'a::field)"
  shows "(\<lambda>x. m *s x + c) o (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
  "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) o (\<lambda>x. m *s x + c) = id"
  using m0
apply (auto simp add: expand_fun_eq vector_add_ldistrib)
by (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric])

lemma vector_affinity_eq:
  assumes m0: "(m::'a::field) \<noteq> 0"
  shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)"
proof
  assume h: "m *s x + c = y"
  hence "m *s x = y - c" by (simp add: field_simps)
  hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
  then show "x = inverse m *s y + - (inverse m *s c)"
    using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
next
  assume h: "x = inverse m *s y + - (inverse m *s c)"
  show "m *s x + c = y" unfolding h diff_minus[symmetric]
    using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
qed

lemma vector_eq_affinity:
 "(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)"
  using vector_affinity_eq[where m=m and x=x and y=y and c=c]
  by metis

lemma const_vector_cart:"((\<chi> i. d)::real^'n) = (\<chi>\<chi> i. d)"
  apply(subst euclidean_eq)
proof safe case goal1
  hence *:"(basis i::real^'n) = cart_basis (\<pi> i)"
    unfolding basis_real_n[THEN sym] by auto
  have "((\<chi> i. d)::real^'n) $$ i = d" unfolding euclidean_component_def *
    unfolding dot_basis by auto
  thus ?case using goal1 by auto
qed

section "Convex Euclidean Space"

lemma Cart_1:"(1::real^'n) = (\<chi>\<chi> i. 1)"
  apply(subst euclidean_eq)
proof safe case goal1 thus ?case using nth_conv_component[THEN sym,where i1="\<pi> i" and x1="1::real^'n"] by auto
qed

declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp]
declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp]

lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta basis_component vector_uminus_component

lemma convex_box_cart:
  assumes "\<And>i. convex {x. P i x}"
  shows "convex {x. \<forall>i. P i (x$i)}"
  using assms unfolding convex_def by auto

lemma convex_positive_orthant_cart: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}"
  by (rule convex_box_cart) (simp add: atLeast_def[symmetric] convex_real_interval)

lemma unit_interval_convex_hull_cart:
  "{0::real^'n .. 1} = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}" (is "?int = convex hull ?points")
  unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"]
  apply(rule arg_cong[where f="\<lambda>x. convex hull x"]) apply(rule set_ext) unfolding mem_Collect_eq
  apply safe apply(erule_tac x="\<pi>' i" in allE) unfolding nth_conv_component defer
  apply(erule_tac x="\<pi> i" in allE) by auto

lemma cube_convex_hull_cart:
  assumes "0 < d" obtains s::"(real^'n) set" where "finite s" "{x - (\<chi> i. d) .. x + (\<chi> i. d)} = convex hull s" 
proof- from cube_convex_hull[OF assms, where 'a="real^'n" and x=x] guess s . note s=this
  show thesis apply(rule that[OF s(1)]) unfolding s(2)[THEN sym] const_vector_cart ..
qed

lemma std_simplex_cart:
  "(insert (0::real^'n) { cart_basis i | i. i\<in>UNIV}) =
  (insert 0 { basis i | i. i<DIM((real,'n) cart)})"
  apply(rule arg_cong[where f="\<lambda>s. (insert 0 s)"])
  unfolding basis_real_n[THEN sym] apply safe
  apply(rule_tac x="\<pi>' i" in exI) defer
  apply(rule_tac x="\<pi> i" in exI) using pi'_range[where 'n='n] by auto

subsection "Brouwer Fixpoint"

lemma kuhn_labelling_lemma_cart:
  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)"
  shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and>
             (\<forall>x i. P x \<and> Q i \<and> (x$i = 0) \<longrightarrow> (l x i = 0)) \<and>
             (\<forall>x i. P x \<and> Q i \<and> (x$i = 1) \<longrightarrow> (l x i = 1)) \<and>
             (\<forall>x i. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x$i \<le> f(x)$i) \<and>
             (\<forall>x i. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x)$i \<le> x$i)" proof-
  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
  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
  show ?thesis unfolding and_forall_thm apply(subst choice_iff[THEN sym])+ proof(rule,rule) case goal1
    let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x $ xa = 0 \<longrightarrow> y = (0::nat)) \<and>
        (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)"
    { 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]
        apply(drule_tac assms(1)[rule_format]) by auto }
    hence "?R 0 \<or> ?R 1" by auto thus ?case by auto qed qed 

lemma interval_bij_cart:"interval_bij = (\<lambda> (a,b) (u,v) (x::real^'n).
    (\<chi> i. u$i + (x$i - a$i) / (b$i - a$i) * (v$i - u$i))::real^'n)"
  unfolding interval_bij_def apply(rule ext)+ apply safe
  unfolding Cart_eq Cart_lambda_beta unfolding nth_conv_component
  apply rule apply(subst euclidean_lambda_beta) using pi'_range by auto

lemma interval_bij_affine_cart:
 "interval_bij (a,b) (u,v) = (\<lambda>x. (\<chi> i. (v$i - u$i) / (b$i - a$i) * x$i) +
            (\<chi> i. u$i - (v$i - u$i) / (b$i - a$i) * a$i)::real^'n)"
  apply rule unfolding Cart_eq interval_bij_cart vector_component_simps
  by(auto simp add: field_simps add_divide_distrib[THEN sym]) 

subsection "Derivative"

lemma has_derivative_vmul_component_cart: fixes c::"real^'a \<Rightarrow> real^'b" and v::"real^'c"
  assumes "(c has_derivative c') net"
  shows "((\<lambda>x. c(x)$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)$k *\<^sub>R v)) net" 
  using has_derivative_vmul_component[OF assms] 
  unfolding nth_conv_component .

lemma differentiable_at_imp_differentiable_on: "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
  unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI)

definition "jacobian f net = matrix(frechet_derivative f net)"

lemma jacobian_works: "(f::(real^'a) \<Rightarrow> (real^'b)) differentiable net \<longleftrightarrow> (f has_derivative (\<lambda>h. (jacobian f net) *v h)) net"
  apply rule unfolding jacobian_def apply(simp only: matrix_works[OF linear_frechet_derivative]) defer
  apply(rule differentiableI) apply assumption unfolding frechet_derivative_works by assumption

subsection {* Component of the differential must be zero if it exists at a local        *)
(* maximum or minimum for that corresponding component. *}

lemma differential_zero_maxmin_component: fixes f::"real^'a \<Rightarrow> real^'b"
  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))"
  "f differentiable (at x)" shows "jacobian f (at x) $ k = 0"
(* FIXME: reuse proof of generic differential_zero_maxmin_component*)

proof(rule ccontr)
  def D \<equiv> "jacobian f (at x)" assume "jacobian f (at x) $ k \<noteq> 0"
  then obtain j where j:"D$k$j \<noteq> 0" unfolding Cart_eq D_def by auto
  hence *:"abs (jacobian f (at x) $ k $ j) / 2 > 0" unfolding D_def by auto
  note as = assms(3)[unfolded jacobian_works has_derivative_at_alt]
  guess e' using as[THEN conjunct2,rule_format,OF *] .. note e' = this
  guess d using real_lbound_gt_zero[OF assms(1) e'[THEN conjunct1]] .. note d = this
  { fix c assume "abs c \<le> d" 
    hence *:"norm (x + c *\<^sub>R cart_basis j - x) < e'" using norm_basis[of j] d by auto
    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))" 
      by(rule component_le_norm_cart)
    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
    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
    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>"
      unfolding vector_component_simps matrix_vector_mul_component unfolding smult_conv_scaleR[symmetric] 
      unfolding inner_simps dot_basis smult_conv_scaleR by simp  } note * = this
  have "x + d *\<^sub>R cart_basis j \<in> ball x e" "x - d *\<^sub>R cart_basis j \<in> ball x e"
    unfolding mem_ball dist_norm using norm_basis[of j] d by auto
  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>
         ((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
  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
  show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\<bar>D $ k $ j\<bar> / 2 * \<bar>d\<bar>"]) 
    using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left
    unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
qed

subsection {* Lemmas for working on @{typ "real^1"} *}

lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
  by (metis num1_eq_iff)

lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
  by auto (metis num1_eq_iff)

lemma exhaust_2:
  fixes x :: 2 shows "x = 1 \<or> x = 2"
proof (induct x)
  case (of_int z)
  then have "0 <= z" and "z < 2" by simp_all
  then have "z = 0 | z = 1" by arith
  then show ?case by auto
qed

lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
  by (metis exhaust_2)

lemma exhaust_3:
  fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3"
proof (induct x)
  case (of_int z)
  then have "0 <= z" and "z < 3" by simp_all
  then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
  then show ?case by auto
qed

lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
  by (metis exhaust_3)

lemma UNIV_1 [simp]: "UNIV = {1::1}"
  by (auto simp add: num1_eq_iff)

lemma UNIV_2: "UNIV = {1::2, 2::2}"
  using exhaust_2 by auto

lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
  using exhaust_3 by auto

lemma setsum_1: "setsum f (UNIV::1 set) = f 1"
  unfolding UNIV_1 by simp

lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"
  unfolding UNIV_2 by simp

lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
  unfolding UNIV_3 by (simp add: add_ac)

instantiation num1 :: cart_one begin
instance proof
  show "CARD(1) = Suc 0" by auto
qed end

(* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *)

abbreviation vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x \<equiv> vec x"

abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
  where "dest_vec1 x \<equiv> (x$1)"

lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
  by (simp_all add:  Cart_eq)

lemma vec1_component[simp]: "(vec1 x)$1 = x"
  by (simp_all add:  Cart_eq)

declare vec1_dest_vec1(1) [simp]

lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
  by (metis vec1_dest_vec1(1))

lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
  by (metis vec1_dest_vec1(1))

lemma vec1_eq[simp]:  "vec1 x = vec1 y \<longleftrightarrow> x = y"
  by (metis vec1_dest_vec1(2))

lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
  by (metis vec1_dest_vec1(1))

subsection{* The collapse of the general concepts to dimension one. *}

lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
  by (simp add: Cart_eq)

lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
  apply auto
  apply (erule_tac x= "x$1" in allE)
  apply (simp only: vector_one[symmetric])
  done

lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
  by (simp add: norm_vector_def)

lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
  by (simp add: norm_vector_1)

lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
  by (auto simp add: norm_real dist_norm)

subsection{* Explicit vector construction from lists. *}

primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}"
where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n"

lemma from_nat [simp]: "from_nat = of_nat"
by (rule ext, induct_tac x, simp_all)

primrec
  list_fun :: "nat \<Rightarrow> _ list \<Rightarrow> _ \<Rightarrow> _"
where
  "list_fun n [] = (\<lambda>x. 0)"
| "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x"

definition "vector l = (\<chi> i. list_fun 1 l i)"
(*definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"*)

lemma vector_1: "(vector[x]) $1 = x"
  unfolding vector_def by simp

lemma vector_2:
 "(vector[x,y]) $1 = x"
 "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
  unfolding vector_def by simp_all

lemma vector_3:
 "(vector [x,y,z] ::('a::zero)^3)$1 = x"
 "(vector [x,y,z] ::('a::zero)^3)$2 = y"
 "(vector [x,y,z] ::('a::zero)^3)$3 = z"
  unfolding vector_def by simp_all

lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
  apply auto
  apply (erule_tac x="v$1" in allE)
  apply (subgoal_tac "vector [v$1] = v")
  apply simp
  apply (vector vector_def)
  apply simp
  done

lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
  apply auto
  apply (erule_tac x="v$1" in allE)
  apply (erule_tac x="v$2" in allE)
  apply (subgoal_tac "vector [v$1, v$2] = v")
  apply simp
  apply (vector vector_def)
  apply (simp add: forall_2)
  done

lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
  apply auto
  apply (erule_tac x="v$1" in allE)
  apply (erule_tac x="v$2" in allE)
  apply (erule_tac x="v$3" in allE)
  apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
  apply simp
  apply (vector vector_def)
  apply (simp add: forall_3)
  done

lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
  apply(rule_tac x="dest_vec1 x" in bexI) by auto

lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
  by (simp)

lemma dest_vec1_vec: "dest_vec1(vec x) = x"
  by (simp)

lemma dest_vec1_sum: assumes fS: "finite S"
  shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
  apply (induct rule: finite_induct[OF fS])
  apply simp
  apply auto
  done

lemma norm_vec1 [simp]: "norm(vec1 x) = abs(x)"
  by (simp add: vec_def norm_real)

lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
  by (simp only: dist_real vec1_component)
lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
  by (metis vec1_dest_vec1(1) norm_vec1)

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
   vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def

lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
  unfolding bounded_linear_def additive_def bounded_linear_axioms_def 
  unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps
  apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto

lemma linear_vmul_dest_vec1:
  fixes f:: "real^_ \<Rightarrow> real^1"
  shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
  unfolding smult_conv_scaleR
  by (rule linear_vmul_component)

lemma linear_from_scalars:
  assumes lf: "linear (f::real^1 \<Rightarrow> real^_)"
  shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
  unfolding smult_conv_scaleR
  apply (rule ext)
  apply (subst matrix_works[OF lf, symmetric])
  apply (auto simp add: Cart_eq matrix_vector_mult_def column_def mult_commute)
  done

lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \<Rightarrow> real^1)"
  shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
  apply (rule ext)
  apply (subst matrix_works[OF lf, symmetric])
  apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute)
  done

lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
  by (simp add: dest_vec1_eq[symmetric])

lemma setsum_scalars: assumes fS: "finite S"
  shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)"
  unfolding vec_setsum[OF fS] by simp

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"
  apply (cases "dest_vec1 x \<le> dest_vec1 y")
  apply simp
  apply (subgoal_tac "dest_vec1 y \<le> dest_vec1 x")
  apply (auto)
  done

text{* Lifting and dropping *}

lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
  assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)"
  using assms unfolding continuous_on_iff apply safe
  apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe
  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
  apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def)

lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
  assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)"
  using assms unfolding continuous_on_iff apply safe
  apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe
  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
  apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def)

lemma continuous_on_vec1:"continuous_on A (vec1::real\<Rightarrow>real^1)"
  by(rule linear_continuous_on[OF bounded_linear_vec1])

lemma mem_interval_1: fixes x :: "real^1" shows
 "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
 "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
by(simp_all add: Cart_eq vector_less_def vector_le_def)

lemma vec1_interval:fixes a::"real" shows
  "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
  "vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
  apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval_cart
  unfolding forall_1 unfolding vec1_dest_vec1_simps
  apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
  apply(rule_tac x="dest_vec1 x" in bexI) by auto

(* Some special cases for intervals in R^1.                                  *)

lemma interval_cases_1: fixes x :: "real^1" shows
 "x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
  unfolding Cart_eq vector_less_def vector_le_def mem_interval_cart by(auto simp del:dest_vec1_eq)

lemma in_interval_1: fixes x :: "real^1" shows
 "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b) \<and>
  (x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
  unfolding Cart_eq vector_less_def vector_le_def mem_interval_cart by(auto simp del:dest_vec1_eq)

lemma interval_eq_empty_1: fixes a :: "real^1" shows
  "{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
  "{a<..<b} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a"
  unfolding interval_eq_empty_cart and ex_1 by auto

lemma subset_interval_1: fixes a :: "real^1" shows
 "({a .. b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
 "({a .. b} \<subseteq> {c<..<d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
                dest_vec1 c < dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b < dest_vec1 d)"
 "({a<..<b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b \<le> dest_vec1 a \<or>
                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
 "({a<..<b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
  unfolding subset_interval_cart[of a b c d] unfolding forall_1 by auto

lemma eq_interval_1: fixes a :: "real^1" shows
 "{a .. b} = {c .. d} \<longleftrightarrow>
          dest_vec1 b < dest_vec1 a \<and> dest_vec1 d < dest_vec1 c \<or>
          dest_vec1 a = dest_vec1 c \<and> dest_vec1 b = dest_vec1 d"
unfolding set_eq_subset[of "{a .. b}" "{c .. d}"]
unfolding subset_interval_1(1)[of a b c d]
unfolding subset_interval_1(1)[of c d a b]
by auto

lemma disjoint_interval_1: fixes a :: "real^1" shows
  "{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"
  "{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"
  "{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"
  "{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"
  unfolding disjoint_interval_cart and ex_1 by auto

lemma open_closed_interval_1: fixes a :: "real^1" shows
 "{a<..<b} = {a .. b} - {a, b}"
  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)

lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)

lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
  "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
  using Lim_component_le_cart[of f l net 1 b] by auto

lemma Lim_drop_ge: fixes f :: "'a \<Rightarrow> real^1" shows
 "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. b \<le> dest_vec1 (f x)) net ==> b \<le> dest_vec1 l"
  using Lim_component_ge_cart[of f l net b 1] by auto

text{* Also more convenient formulations of monotone convergence.                *}

lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real^1"
  assumes "bounded {s n| n::nat. True}"  "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
  shows "\<exists>l. (s ---> l) sequentially"
proof-
  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
  { fix m::nat
    have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
      apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq)  }
  hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
  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
  thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
    unfolding dist_norm unfolding abs_dest_vec1  by auto
qed

lemma dest_vec1_simps[simp]: fixes a::"real^1"
  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"*)
  "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
  by(auto simp add: vector_le_def Cart_eq)

lemma dest_vec1_inverval:
  "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"
  "dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}"
  "dest_vec1 ` {a ..<b} = {dest_vec1 a ..<dest_vec1 b}"
  "dest_vec1 ` {a<..<b} = {dest_vec1 a<..<dest_vec1 b}"
  apply(rule_tac [!] equalityI)
  unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff
  apply(rule_tac [!] allI)apply(rule_tac [!] impI)
  apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
  apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
  by (auto simp add: vector_less_def vector_le_def)

lemma dest_vec1_setsum: assumes "finite S"
  shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
  using dest_vec1_sum[OF assms] by auto

lemma open_dest_vec1_vimage: "open S \<Longrightarrow> open (dest_vec1 -` S)"
unfolding open_vector_def forall_1 by auto

lemma tendsto_dest_vec1 [tendsto_intros]:
  "(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
by(rule tendsto_Cart_nth)

lemma continuous_dest_vec1: "continuous net f \<Longrightarrow> continuous net (\<lambda>x. dest_vec1 (f x))"
  unfolding continuous_def by (rule tendsto_dest_vec1)

lemma forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))" 
  apply safe defer apply(erule_tac x="vec1 x" in allE) by auto

lemma forall_of_dest_vec1: "(\<forall>v. P (\<lambda>x. dest_vec1 (v x))) \<longleftrightarrow> (\<forall>x. P x)"
  apply rule apply rule apply(erule_tac x="(vec1 \<circ> x)" in allE) unfolding o_def vec1_dest_vec1 by auto 

lemma forall_of_dest_vec1': "(\<forall>v. P (dest_vec1 v)) \<longleftrightarrow> (\<forall>x. P x)"
  apply rule apply rule apply(erule_tac x="(vec1 x)" in allE) defer apply rule 
  apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto

lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding dist_norm by auto

lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
  shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
  { assume ?l guess K using linear_bounded[OF `?l`] ..
    hence "\<exists>K. \<forall>x. \<bar>f x\<bar> \<le> \<bar>x\<bar> * K" apply(rule_tac x=K in exI)
      unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) }
  thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def
    unfolding vec1_dest_vec1_simps by auto qed

lemma vec1_le[simp]:fixes a::real shows "vec1 a \<le> vec1 b \<longleftrightarrow> a \<le> b"
  unfolding vector_le_def by auto
lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \<longleftrightarrow> a < b"
  unfolding vector_less_def by auto


subsection {* Derivatives on real = Derivatives on @{typ "real^1"} *}

lemma has_derivative_within_vec1_dest_vec1: fixes f::"real\<Rightarrow>real" shows
  "((vec1 \<circ> f \<circ> dest_vec1) has_derivative (vec1 \<circ> f' \<circ> dest_vec1)) (at (vec1 x) within vec1 ` s)
  = (f has_derivative f') (at x within s)"
  unfolding has_derivative_within unfolding bounded_linear_vec1_dest_vec1[unfolded linear_conv_bounded_linear]
  unfolding o_def Lim_within Ball_def unfolding forall_vec1 
  unfolding vec1_dest_vec1_simps dist_vec1_0 image_iff by auto  

lemma has_derivative_at_vec1_dest_vec1: fixes f::"real\<Rightarrow>real" shows
  "((vec1 \<circ> f \<circ> dest_vec1) has_derivative (vec1 \<circ> f' \<circ> dest_vec1)) (at (vec1 x)) = (f has_derivative f') (at x)"
  using has_derivative_within_vec1_dest_vec1[where s=UNIV, unfolded range_vec1 within_UNIV] by auto

lemma bounded_linear_vec1': fixes f::"'a::real_normed_vector\<Rightarrow>real"
  shows "bounded_linear f = bounded_linear (vec1 \<circ> f)"
  unfolding bounded_linear_def additive_def bounded_linear_axioms_def o_def
  unfolding vec1_dest_vec1_simps by auto

lemma bounded_linear_dest_vec1: fixes f::"real\<Rightarrow>'a::real_normed_vector"
  shows "bounded_linear f = bounded_linear (f \<circ> dest_vec1)"
  unfolding bounded_linear_def additive_def bounded_linear_axioms_def o_def
  unfolding vec1_dest_vec1_simps by auto

lemma has_derivative_at_vec1: fixes f::"'a::real_normed_vector\<Rightarrow>real" shows
  "(f has_derivative f') (at x) = ((vec1 \<circ> f) has_derivative (vec1 \<circ> f')) (at x)"
  unfolding has_derivative_at unfolding bounded_linear_vec1'[unfolded linear_conv_bounded_linear]
  unfolding o_def Lim_at unfolding vec1_dest_vec1_simps dist_vec1_0 by auto

lemma has_derivative_within_dest_vec1:fixes f::"real\<Rightarrow>'a::real_normed_vector" shows
  "((f \<circ> dest_vec1) has_derivative (f' \<circ> dest_vec1)) (at (vec1 x) within vec1 ` s) = (f has_derivative f') (at x within s)"
  unfolding has_derivative_within bounded_linear_dest_vec1 unfolding o_def Lim_within Ball_def
  unfolding vec1_dest_vec1_simps dist_vec1_0 image_iff by auto

lemma has_derivative_at_dest_vec1:fixes f::"real\<Rightarrow>'a::real_normed_vector" shows
  "((f \<circ> dest_vec1) has_derivative (f' \<circ> dest_vec1)) (at (vec1 x)) = (f has_derivative f') (at x)"
  using has_derivative_within_dest_vec1[where s=UNIV] by(auto simp add:within_UNIV)

subsection {* In particular if we have a mapping into @{typ "real^1"}. *}

lemma onorm_vec1: fixes f::"real \<Rightarrow> real"
  shows "onorm (\<lambda>x. vec1 (f (dest_vec1 x))) = onorm f" proof-
  have "\<forall>x::real^1. norm x = 1 \<longleftrightarrow> x\<in>{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:Cart_eq)
  hence 1:"{x. norm x = 1} = {vec1 -1, vec1 (1::real)}" by auto
  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
  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
  have 4:"{norm (f x) |x. norm x = 1} = (\<lambda>x. norm (f x)) ` {x. norm x=1}" by auto
  show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max) qed

lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)"
  unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto

lemma bounded_linear_component_cart[intro]: "bounded_linear (\<lambda>x::real^'n. x $ k)"
  apply(rule bounded_linearI[where K=1]) 
  using component_le_norm_cart[of _ k] unfolding real_norm_def by auto

lemma bounded_vec1[intro]:  "bounded s \<Longrightarrow> bounded (vec1 ` (s::real set))"
  unfolding bounded_def apply safe apply(rule_tac x="vec1 x" in exI,rule_tac x=e in exI)
  by(auto simp add: dist_real dist_real_def)

(*lemma content_closed_interval_cases_cart:
  "content {a..b::real^'n} =
  (if {a..b} = {} then 0 else setprod (\<lambda>i. b$i - a$i) UNIV)" 
proof(cases "{a..b} = {}")
  case True thus ?thesis unfolding content_def by auto
next case Falsethus ?thesis unfolding content_def unfolding if_not_P[OF False]
  proof(cases "\<forall>i. a $ i \<le> b $ i")
    case False thus ?thesis unfolding content_def using t by auto
  next case True note interval_eq_empty
   apply auto 
  
  sorry*)

lemma integral_component_eq_cart[simp]: fixes f::"'n::ordered_euclidean_space \<Rightarrow> real^'m"
  assumes "f integrable_on s" shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
  using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] .

lemma interval_split_cart:
  "{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
  "{a..b} \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}"
  apply(rule_tac[!] set_ext) unfolding Int_iff mem_interval_cart mem_Collect_eq
  unfolding Cart_lambda_beta by auto

(*lemma content_split_cart:
  "content {a..b::real^'n} = content({a..b} \<inter> {x. x$k \<le> c}) + content({a..b} \<inter> {x. x$k >= c})"
proof- note simps = interval_split_cart content_closed_interval_cases_cart Cart_lambda_beta vector_le_def
  { presume "a\<le>b \<Longrightarrow> ?thesis" thus ?thesis apply(cases "a\<le>b") unfolding simps by auto }
  have *:"UNIV = insert k (UNIV - {k})" "\<And>x. finite (UNIV-{x::'n})" "\<And>x. x\<notin>UNIV-{x}" by auto
  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))"
    "(\<Prod>i\<in>UNIV. b$i - a$i) = (\<Prod>i\<in>UNIV-{k}. b$i - a$i) * (b$k - a$k)" 
    apply(subst *(1)) defer apply(subst *(1)) unfolding setprod_insert[OF *(2-)] by auto
  assume as:"a\<le>b" moreover have "\<And>x. min (b $ k) c = max (a $ k) c
    \<Longrightarrow> x* (b$k - a$k) = x*(max (a $ k) c - a $ k) + x*(b $ k - max (a $ k) c)"
    by  (auto simp add:field_simps)
  moreover have "\<not> a $ k \<le> c \<Longrightarrow> \<not> c \<le> b $ k \<Longrightarrow> False"
    unfolding not_le using as[unfolded vector_le_def,rule_format,of k] by auto
  ultimately show ?thesis 
    unfolding simps unfolding *(1)[of "\<lambda>i x. b$i - x"] *(1)[of "\<lambda>i x. x - a$i"] *(2) by(auto)
qed*)

lemma has_integral_vec1: assumes "(f has_integral k) {a..b}"
  shows "((\<lambda>x. vec1 (f x)) has_integral (vec1 k)) {a..b}"
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)"
    unfolding vec_sub Cart_eq by(auto simp add: split_beta)
  show ?thesis using assms unfolding has_integral apply safe
    apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
    apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed

end