Quellcode-Bibliothek Affine.thy Sprache: Isabelle

section "Affine Sets"

theory Affine
imports Linear_Algebra
begin

lemma if_smult: "(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)"
  by simp

lemma sum_delta_notmem:
  assumes "x \ s"
  shows "sum (\y. if (y = x) then P x else Q y) s = sum Q s"
    and "sum (\y. if (x = y) then P x else Q y) s = sum Q s"
    and "sum (\y. if (y = x) then P y else Q y) s = sum Q s"
    and "sum (\y. if (x = y) then P y else Q y) s = sum Q s"
  by (smt (verit, best) assms sum.cong)+

lemma span_substd_basis:
  assumes d: "d \ Basis"
  shows "span d = {x. \i\Basis. i \ d \ x\i = 0}"
  (is "_ = ?B")
proof -
  have "d \ ?B"
    using d by (auto simp: inner_Basis)
  moreover have s: "subspace ?B"
    using subspace_substandard[of "\i. i \ d"] .
  ultimately have "span d \ ?B"
    using span_mono[of d "?B"] span_eq_iff[of "?B"] by blast
  moreover have *: "card d \ dim (span d)"
    by (simp add: d dim_eq_card_independent independent_substdbasis)
  moreover from * have "dim ?B \ dim (span d)"
    using dim_substandard[OF assms] by auto
  ultimately show ?thesis
    by (simp add: s subspace_dim_equal)
qed

lemma basis_to_substdbasis_subspace_isomorphism:
  fixes B :: "'a::euclidean_space set"
  assumes "independent B"
  shows "\f d::'a set. card d = card B \ linear f \ f ` B = d \
    f ` span B = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} \<and> inj_on f (span B) \<and> d \<subseteq> Basis"
proof -
  have B: "card B = dim B"
    using dim_unique[of B B "card B"] assms span_superset[of B] by auto
  have "dim B \ card (Basis :: 'a set)"
    using dim_subset_UNIV[of B] by simp
  from obtain_subset_with_card_n[OF this]
  obtain d :: "'a set" where d: "d \ Basis" and t: "card d = dim B"
    by auto
  let ?t = "{x::'a::euclidean_space. \i\Basis. i \ d \ x\i = 0}"
  have "\f. linear f \ f ` B = d \ f ` span B = ?t \ inj_on f (span B)"
  proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_superset)
    show "d \ {x. \i\Basis. i \ d \ x \ i = 0}"
      using d inner_not_same_Basis by blast
  qed (auto simp: span_substd_basis independent_substdbasis dim_substandard d t B assms)
  with t \<open>card B = dim B\<close> d show ?thesis by auto
qed

subsection \<open>Affine set and affine hull\<close>

definition\<^marker>\<open>tag important\<close> affine :: "'a::real_vector set \<Rightarrow> bool"
  where "affine S \ (\x\S. \y\S. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ S)"

lemma affine_alt: "affine S \ (\x\S. \y\S. \u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \ S)"
  unfolding affine_def by (metis eq_diff_eq')

lemma affine_empty [iff]: "affine {}"
  unfolding affine_def by auto

lemma affine_sing [iff]: "affine {x}"
  unfolding affine_alt by (auto simp: scaleR_left_distrib [symmetric])

lemma affine_UNIV [iff]: "affine UNIV"
  unfolding affine_def by auto

lemma affine_Inter [intro]: "(\S. S\\ \ affine S) \ affine (\\)"
  unfolding affine_def by auto

lemma affine_Int[intro]: "affine S \ affine T \ affine (S \ T)"
  unfolding affine_def by auto

lemma affine_scaling: "affine S \ affine ((*\<^sub>R) c ` S)"
  apply (clarsimp simp: affine_def)
  apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI)
  apply (auto simp: algebra_simps)
  done

lemma affine_affine_hull [simp]: "affine(affine hull S)"
  unfolding hull_def
  using affine_Inter[of "{T. affine T \ S \ T}"] by auto

lemma affine_hull_eq[simp]: "(affine hull s = s) \ affine s"
  by (metis affine_affine_hull hull_same)

lemma affine_hyperplane: "affine {x. a \ x = b}"
  by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral)

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Some explicit formulations\<close>

text "Formalized by Lars Schewe."

lemma affine:
  fixes V::"'a::real_vector set"
  shows "affine V \
         (\<forall>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> V \<and> sum u S = 1 \<longrightarrow> (\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V)"
proof -
  have "u *\<^sub>R x + v *\<^sub>R y \ V" if "x \ V" "y \ V" "u + v = (1::real)"
    and *: "\S u. \finite S; S \ {}; S \ V; sum u S = 1\ \ (\x\S. u x *\<^sub>R x) \ V" for x y u v
  proof (cases "x = y")
    case True
    then show ?thesis
      using that by (metis scaleR_add_left scaleR_one)
  next
    case False
    then show ?thesis
      using that *[of "{x,y}" "\w. if w = x then u else v"] by auto
  qed
  moreover have "(\x\S. u x *\<^sub>R x) \ V"
                if *: "\x y u v. \x\V; y\V; u + v = 1\ \ u *\<^sub>R x + v *\<^sub>R y \ V"
                  and "finite S" "S \ {}" "S \ V" "sum u S = 1" for S u
  proof -
    define n where "n = card S"
    consider "card S = 0" | "card S = 1" | "card S = 2" | "card S > 2" by linarith
    then show "(\x\S. u x *\<^sub>R x) \ V"
    proof cases
      assume "card S = 1"
      then obtain a where "S={a}"
        by (auto simp: card_Suc_eq)
      then show ?thesis
        using that by simp
    next
      assume "card S = 2"
      then obtain a b where "S = {a, b}"
        by (metis Suc_1 card_1_singletonE card_Suc_eq)
      then show ?thesis
        using *[of a b] that
        by (auto simp: sum_clauses(2))
    next
      assume "card S > 2"
      then show ?thesis using that n_def
      proof (induct n arbitrary: u S)
        case 0
        then show ?case by auto
      next
        case (Suc n u S)
        have "sum u S = card S" if "\ (\x\S. u x \ 1)"
          using that unfolding card_eq_sum by auto
        with Suc.prems obtain x where "x \ S" and x: "u x \ 1" by force
        have c: "card (S - {x}) = card S - 1"
          by (simp add: Suc.prems(3) \<open>x \<in> S\<close>)
        have "sum u (S - {x}) = 1 - u x"
          by (simp add: Suc.prems sum_diff1 \<open>x \<in> S\<close>)
        with x have eq1: "inverse (1 - u x) * sum u (S - {x}) = 1"
          by auto
        have inV: "(\y\S - {x}. (inverse (1 - u x) * u y) *\<^sub>R y) \ V"
        proof (cases "card (S - {x}) > 2")
          case True
          then have S: "S - {x} \ {}" "card (S - {x}) = n"
            using Suc.prems c by force+
          show ?thesis
          proof (rule Suc.hyps)
            show "(\a\S - {x}. inverse (1 - u x) * u a) = 1"
              by (auto simp: eq1 sum_distrib_left[symmetric])
          qed (use S Suc.prems True in auto)
        next
          case False
          then have "card (S - {x}) = Suc (Suc 0)"
            using Suc.prems c by auto
          then obtain a b where ab: "(S - {x}) = {a, b}" "a\b"
            unfolding card_Suc_eq by auto
          then show ?thesis
            using eq1 \<open>S \<subseteq> V\<close>
            by (auto simp: sum_distrib_left distrib_left intro!: Suc.prems(2)[of a b])
        qed
        have "u x + (1 - u x) = 1 \
          u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\<Sum>y\<in>S - {x}. u y *\<^sub>R y) /\<^sub>R (1 - u x)) \<in> V"
          by (rule Suc.prems) (use \<open>x \<in> S\<close> Suc.prems inV in \<open>auto simp: scaleR_right.sum\<close>)
        moreover have "(\a\S. u a *\<^sub>R a) = u x *\<^sub>R x + (\a\S - {x}. u a *\<^sub>R a)"
          by (meson Suc.prems(3) sum.remove \<open>x \<in> S\<close>)
        ultimately show "(\x\S. u x *\<^sub>R x) \ V"
          by (simp add: x)
      qed
    qed (use \<open>S\<noteq>{}\<close> \<open>finite S\<close> in auto)
  qed
  ultimately show ?thesis
    unfolding affine_def by meson
qed

lemma affine_hull_explicit:
  "affine hull p = {y. \S u. finite S \ S \ {} \ S \ p \ sum u S = 1 \ sum (\v. u v *\<^sub>R v) S = y}"
  (is "_ = ?rhs")
proof (rule hull_unique)
  have "\x. sum (\z. 1) {x} = 1"
      by auto
  show "p \ ?rhs"
  proof (intro subsetI CollectI exI conjI)
    show "\x. sum (\z. 1) {x} = 1"
      by auto
  qed auto
  show "?rhs \ T" if "p \ T" "affine T" for T
    using that unfolding affine by blast
  show "affine ?rhs"
    unfolding affine_def
  proof clarify
    fix u v :: real and sx ux sy uy
    assume uv: "u + v = 1"
      and x: "finite sx" "sx \ {}" "sx \ p" "sum ux sx = (1::real)"
      and y: "finite sy" "sy \ {}" "sy \ p" "sum uy sy = (1::real)"
    have **: "(sx \ sy) \ sx = sx" "(sx \ sy) \ sy = sy"
      by auto
    show "\S w. finite S \ S \ {} \ S \ p \
        sum w S = 1 \<and> (\<Sum>v\<in>S. w v *\<^sub>R v) = u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)"
    proof (intro exI conjI)
      show "finite (sx \ sy)"
        using x y by auto
      show "sum (\i. (if i\sx then u * ux i else 0) + (if i\sy then v * uy i else 0)) (sx \ sy) = 1"
        using x y uv
        by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] sum_distrib_left [symmetric] **)
      have "(\i\sx \ sy. ((if i \ sx then u * ux i else 0) + (if i \ sy then v * uy i else 0)) *\<^sub>R i)
          = (\<Sum>i\<in>sx. (u * ux i) *\<^sub>R i) + (\<Sum>i\<in>sy. (v * uy i) *\<^sub>R i)"
        using x y
        unfolding scaleR_left_distrib scaleR_zero_left if_smult
        by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric]  **)
      also have "\ = u *\<^sub>R (\v\sx. ux v *\<^sub>R v) + v *\<^sub>R (\v\sy. uy v *\<^sub>R v)"
        unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] by blast
      finally show "(\i\sx \ sy. ((if i \ sx then u * ux i else 0) + (if i \ sy then v * uy i else 0)) *\<^sub>R i)
                  = u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)" .
    qed (use x y in auto)
  qed
qed

lemma affine_hull_finite:
  assumes "finite S"
  shows "affine hull S = {y. \u. sum u S = 1 \ sum (\v. u v *\<^sub>R v) S = y}"
proof -
  have *: "\h. sum h S = 1 \ (\v\S. h v *\<^sub>R v) = x"
    if "F \ S" "finite F" "F \ {}" and sum: "sum u F = 1" and x: "(\v\F. u v *\<^sub>R v) = x" for x F u
  proof -
    have "S \ F = F"
      using that by auto
    show ?thesis
    proof (intro exI conjI)
      show "(\x\S. if x \ F then u x else 0) = 1"
        by (metis (mono_tags, lifting) \<open>S \<inter> F = F\<close> assms sum.inter_restrict sum)
      show "(\v\S. (if v \ F then u v else 0) *\<^sub>R v) = x"
        by (simp add: if_smult cong: if_cong) (metis (no_types) \<open>S \<inter> F = F\<close> assms sum.inter_restrict x)
    qed
  qed
  show ?thesis
    unfolding affine_hull_explicit using assms
    by (fastforce dest: *)
qed

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Stepping theorems and hence small special cases\<close>

lemma affine_hull_empty[simp]: "affine hull {} = {}"
  by simp

lemma affine_hull_finite_step:
  fixes y :: "'a::real_vector"
  shows "finite S \
      (\<exists>u. sum u (insert a S) = w \<and> sum (\<lambda>x. u x *\<^sub>R x) (insert a S) = y) \<longleftrightarrow>
      (\<exists>v u. sum u S = w - v \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y - v *\<^sub>R a)" (is "_ \<Longrightarrow> ?lhs = ?rhs")
proof -
  assume fin: "finite S"
  show "?lhs = ?rhs"
  proof
    assume ?lhs
    then obtain u where u: "sum u (insert a S) = w \ (\x\insert a S. u x *\<^sub>R x) = y"
      by auto
    show ?rhs
    proof (cases "a \ S")
      case True
      then show ?thesis
        using u by (simp add: insert_absorb) (metis diff_zero real_vector.scale_zero_left)
    next
      case False
      show ?thesis
        by (rule exI [where x="u a"]) (use u fin False in auto)
    qed
  next
    assume ?rhs
    then obtain v u where vu: "sum u S = w - v"  "(\x\S. u x *\<^sub>R x) = y - v *\<^sub>R a"
      by auto
    have *: "\x M. (if x = a then v else M) *\<^sub>R x = (if x = a then v *\<^sub>R x else M *\<^sub>R x)"
      by auto
    show ?lhs
    proof (cases "a \ S")
      case True
      show ?thesis
        by (rule exI [where x="\x. (if x=a then v else 0) + u x"])
           (simp add: True scaleR_left_distrib sum.distrib sum_clauses fin vu * cong: if_cong)
    next
      case False
      then show ?thesis
        apply (rule_tac x="\x. if x=a then v else u x" in exI)
        apply (simp add: vu sum_clauses(2)[OF fin] *)
        by (simp add: sum_delta_notmem(3) vu)
    qed
  qed
qed

lemma affine_hull_2:
  fixes a b :: "'a::real_vector"
  shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}"
  (is "?lhs = ?rhs")
proof -
  have *:
    "\x y z. z = x - y \ y + z = (x::real)"
    "\x y z. z = x - y \ y + z = (x::'a)" by auto
  have "?lhs = {y. \u. sum u {a, b} = 1 \ (\v\{a, b}. u v *\<^sub>R v) = y}"
    using affine_hull_finite[of "{a,b}"] by auto
  also have "\ = {y. \v u. u b = 1 - v \ u b *\<^sub>R b = y - v *\<^sub>R a}"
    by (simp add: affine_hull_finite_step[of "{b}" a])
  also have "\ = ?rhs" unfolding * by auto
  finally show ?thesis by auto
qed

lemma affine_hull_3:
  fixes a b c :: "'a::real_vector"
  shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}"
proof -
  have *:
    "\x y z. z = x - y \ y + z = (x::real)"
    "\x y z. z = x - y \ y + z = (x::'a)" by auto
  show ?thesis
    apply (simp add: affine_hull_finite affine_hull_finite_step)
    unfolding *
    apply safe
     apply (metis add.assoc)
    apply (rule_tac x=u in exI, force)
    done
qed

lemma mem_affine:
  assumes "affine S" "x \ S" "y \ S" "u + v = 1"
  shows "u *\<^sub>R x + v *\<^sub>R y \ S"
  using assms affine_def[of S] by auto

lemma mem_affine_3:
  assumes "affine S" "x \ S" "y \ S" "z \ S" "u + v + w = 1"
  shows "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \ S"
proof -
  have "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \ affine hull {x, y, z}"
    using affine_hull_3[of x y z] assms by auto
  moreover
  have "affine hull {x, y, z} \ affine hull S"
    using hull_mono[of "{x, y, z}" "S"] assms by auto
  moreover
  have "affine hull S = S"
    using assms affine_hull_eq[of S] by auto
  ultimately show ?thesis by auto
qed

lemma mem_affine_3_minus:
  assumes "affine S" "x \ S" "y \ S" "z \ S"
  shows "x + v *\<^sub>R (y-z) \ S"
  using mem_affine_3[of S x y z 1 v "-v"] assms
  by (simp add: algebra_simps)

corollary%unimportant mem_affine_3_minus2:
    "\affine S; x \ S; y \ S; z \ S\ \ x - v *\<^sub>R (y-z) \ S"
  by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left)

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Some relations between affine hull and subspaces\<close>

lemma affine_hull_insert_subset_span:
  "affine hull (insert a S) \ {a + v| v . v \ span {x - a | x . x \ S}}"
proof -
  have "\v T u. x = a + v \ (finite T \ T \ {x - a |x. x \ S} \ (\v\T. u v *\<^sub>R v) = v)"
    if "finite F" "F \ {}" "F \ insert a S" "sum u F = 1" "(\v\F. u v *\<^sub>R v) = x"
    for x F u
  proof -
    have *: "(\x. x - a) ` (F - {a}) \ {x - a |x. x \ S}"
      using that by auto
    show ?thesis
    proof (intro exI conjI)
      show "finite ((\x. x - a) ` (F - {a}))"
        by (simp add: that(1))
      show "(\v\(\x. x - a) ` (F - {a}). u(v+a) *\<^sub>R v) = x-a"
        by (simp add: sum.reindex[unfolded inj_on_def] algebra_simps
            sum_subtractf scaleR_left.sum[symmetric] sum_diff1 that)
    qed (use \<open>F \<subseteq> insert a S\<close> in auto)
  qed
  then show ?thesis
    unfolding affine_hull_explicit span_explicit by fast
qed

lemma affine_hull_insert_span:
  assumes "a \ S"
  shows "affine hull (insert a S) = {a + v | v . v \ span {x - a | x. x \ S}}"
proof -
  have *: "\G u. finite G \ G \ {} \ G \ insert a S \ sum u G = 1 \ (\v\G. u v *\<^sub>R v) = y"
    if "v \ span {x - a |x. x \ S}" "y = a + v" for y v
  proof -
    from that
    obtain T u where u: "finite T" "T \ {x - a |x. x \ S}" "a + (\v\T. u v *\<^sub>R v) = y"
      unfolding span_explicit by auto
    define F where "F = (\x. x + a) ` T"
    have F: "finite F" "F \ S" "(\v\F. u (v - a) *\<^sub>R (v - a)) = y - a"
      unfolding F_def using u by (auto simp: sum.reindex[unfolded inj_on_def])
    have *: "F \ {a} = {}" "F \ - {a} = F"
      using F assms by auto
    show "\G u. finite G \ G \ {} \ G \ insert a S \ sum u G = 1 \ (\v\G. u v *\<^sub>R v) = y"
      apply (rule_tac x = "insert a F" in exI)
      apply (rule_tac x = "\x. if x=a then 1 - sum (\x. u (x - a)) F else u (x - a)" in exI)
      using assms F
      apply (auto simp:  sum_clauses sum.If_cases if_smult sum_subtractf scaleR_left.sum algebra_simps *)
      done
  qed
  show ?thesis
    by (intro subset_antisym affine_hull_insert_subset_span) (auto simp: affine_hull_explicit dest!: *)
qed

lemma affine_hull_span:
  assumes "a \ S"
  shows "affine hull S = {a + v | v. v \ span {x - a | x. x \ S - {a}}}"
  using affine_hull_insert_span[of a "S - {a}", unfolded insert_Diff[OF assms]] by auto

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Parallel affine sets\<close>

definition affine_parallel :: "'a::real_vector set \ 'a::real_vector set \ bool"
  where "affine_parallel S T \ (\a. T = (\x. a + x) ` S)"

lemma affine_parallel_expl_aux:
  fixes S T :: "'a::real_vector set"
  assumes "\x. x \ S \ a + x \ T"
  shows "T = (\x. a + x) ` S"
proof -
  have "x \ ((\x. a + x) ` S)" if "x \ T" for x
    using that
    by (simp add: image_iff) (metis add.commute diff_add_cancel assms)
  moreover have "T \ (\x. a + x) ` S"
    using assms by auto
  ultimately show ?thesis by auto
qed

lemma affine_parallel_expl: "affine_parallel S T \ (\a. \x. x \ S \ a + x \ T)"
  by (auto simp add: affine_parallel_def)
    (use affine_parallel_expl_aux [of S _ T] in blast)

lemma affine_parallel_reflex: "affine_parallel S S"
  unfolding affine_parallel_def
  using image_add_0 by blast

lemma affine_parallel_commute:
  assumes "affine_parallel A B"
  shows "affine_parallel B A"
  by (metis affine_parallel_def assms translation_galois)

lemma affine_parallel_assoc:
  assumes "affine_parallel A B"
    and "affine_parallel B C"
  shows "affine_parallel A C"
  by (metis affine_parallel_def assms translation_assoc)

lemma affine_translation_aux:
  fixes a :: "'a::real_vector"
  assumes "affine ((\x. a + x) ` S)"
  shows "affine S"
proof -
  {
    fix x y u v
    assume xy: "x \ S" "y \ S" "(u :: real) + v = 1"
    then have "(a + x) \ ((\x. a + x) ` S)" "(a + y) \ ((\x. a + x) ` S)"
      by auto
    then have h1: "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) \ (\x. a + x) ` S"
      using xy assms unfolding affine_def by auto
    have "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) = (u + v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)"
      by (simp add: algebra_simps)
    also have "\ = a + (u *\<^sub>R x + v *\<^sub>R y)"
      using \<open>u + v = 1\<close> by auto
    ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) \ (\x. a + x) ` S"
      using h1 by auto
    then have "u *\<^sub>R x + v *\<^sub>R y \ S" by auto
  }
  then show ?thesis unfolding affine_def by auto
qed

lemma affine_translation:
  "affine S \ affine ((+) a ` S)" for a :: "'a::real_vector"
  by (metis affine_translation_aux translation_galois)

lemma parallel_is_affine:
  fixes S T :: "'a::real_vector set"
  assumes "affine S" "affine_parallel S T"
  shows "affine T"
  by (metis affine_parallel_def affine_translation assms)

lemma subspace_imp_affine: "subspace s \ affine s"
  unfolding subspace_def affine_def by auto

lemma affine_hull_subset_span: "(affine hull s) \ (span s)"
  by (metis hull_minimal span_superset subspace_imp_affine subspace_span)

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Subspace parallel to an affine set\<close>

lemma subspace_affine: "subspace S \ affine S \ 0 \ S"
  by (metis add_cancel_right_left affine_alt diff_add_cancel mem_affine_3 scaleR_eq_0_iff subspace_def vector_space_assms(4))

lemma affine_diffs_subspace:
  assumes "affine S" "a \ S"
  shows "subspace ((\x. (-a)+x) ` S)"
  by (metis ab_left_minus affine_translation assms image_eqI subspace_affine)

lemma affine_diffs_subspace_subtract:
  "subspace ((\x. x - a) ` S)" if "affine S" "a \ S"
  using that affine_diffs_subspace [of _ a] by simp

lemma parallel_subspace_explicit:
  assumes "affine S"
    and "a \ S"
  assumes "L \ {y. \x \ S. (-a) + x = y}"
  shows "subspace L \ affine_parallel S L"
  by (smt (verit) Collect_cong ab_left_minus affine_parallel_def assms image_def mem_Collect_eq parallel_is_affine subspace_affine)

lemma parallel_subspace_aux:
  assumes "subspace A"
    and "subspace B"
    and "affine_parallel A B"
  shows "A \ B"
  by (metis add.right_neutral affine_parallel_expl assms subsetI subspace_def)

lemma parallel_subspace:
  assumes "subspace A"
    and "subspace B"
    and "affine_parallel A B"
  shows "A = B"
  by (simp add: affine_parallel_commute assms parallel_subspace_aux subset_antisym)

lemma affine_parallel_subspace:
  assumes "affine S" "S \ {}"
  shows "\!L. subspace L \ affine_parallel S L"
  by (meson affine_parallel_assoc affine_parallel_commute assms equals0I parallel_subspace parallel_subspace_explicit)

subsection \<open>Affine Dependence\<close>

text "Formalized by Lars Schewe."

definition\<^marker>\<open>tag important\<close> affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
  where "affine_dependent S \ (\x\S. x \ affine hull (S - {x}))"

lemma affine_dependent_imp_dependent: "affine_dependent S \ dependent S"
  unfolding affine_dependent_def dependent_def
  using affine_hull_subset_span by auto

lemma affine_dependent_subset:
   "\affine_dependent S; S \ T\ \ affine_dependent T"
  using hull_mono [OF Diff_mono [OF _ subset_refl]]
  by (smt (verit) affine_dependent_def subsetD)

lemma affine_independent_subset:
  shows "\\ affine_dependent T; S \ T\ \ \ affine_dependent S"
  by (metis affine_dependent_subset)

lemma affine_independent_Diff:
   "\ affine_dependent S \ \ affine_dependent(S - T)"
by (meson Diff_subset affine_dependent_subset)

proposition affine_dependent_explicit:
  "affine_dependent p \
    (\<exists>S U. finite S \<and> S \<subseteq> p \<and> sum U S = 0 \<and> (\<exists>v\<in>S. U v \<noteq> 0) \<and> sum (\<lambda>v. U v *\<^sub>R v) S = 0)"
proof -
  have "\S U. finite S \ S \ p \ sum U S = 0 \ (\v\S. U v \ 0) \ (\w\S. U w *\<^sub>R w) = 0"
    if "(\w\S. U w *\<^sub>R w) = x" "x \ p" "finite S" "S \ {}" "S \ p - {x}" "sum U S = 1" for x S U
  proof (intro exI conjI)
    have "x \ S"
      using that by auto
    then show "(\v \ insert x S. if v = x then - 1 else U v) = 0"
      using that by (simp add: sum_delta_notmem)
    show "(\w \ insert x S. (if w = x then - 1 else U w) *\<^sub>R w) = 0"
      using that \<open>x \<notin> S\<close> by (simp add: if_smult sum_delta_notmem cong: if_cong)
  qed (use that in auto)
  moreover have "\x\p. \S U. finite S \ S \ {} \ S \ p - {x} \ sum U S = 1 \ (\v\S. U v *\<^sub>R v) = x"
    if "(\v\S. U v *\<^sub>R v) = 0" "finite S" "S \ p" "sum U S = 0" "v \ S" "U v \ 0" for S U v
  proof (intro bexI exI conjI)
    have "S \ {v}"
      using that by auto
    then show "S - {v} \ {}"
      using that by auto
    show "(\x \ S - {v}. - (1 / U v) * U x) = 1"
      unfolding sum_distrib_left[symmetric] sum_diff1[OF \<open>finite S\<close>] by (simp add: that)
    show "(\x\S - {v}. (- (1 / U v) * U x) *\<^sub>R x) = v"
      unfolding sum_distrib_left [symmetric] scaleR_scaleR[symmetric]
                scaleR_right.sum [symmetric] sum_diff1[OF \<open>finite S\<close>]
      using that by auto
    show "S - {v} \ p - {v}"
      using that by auto
  qed (use that in auto)
  ultimately show ?thesis
    unfolding affine_dependent_def affine_hull_explicit by auto
qed

lemma affine_dependent_explicit_finite:
  fixes S :: "'a::real_vector set"
  assumes "finite S"
  shows "affine_dependent S \
    (\<exists>U. sum U S = 0 \<and> (\<exists>v\<in>S. U v \<noteq> 0) \<and> sum (\<lambda>v. U v *\<^sub>R v) S = 0)"
  (is "?lhs = ?rhs")
proof
  have *: "\vt U v. (if vt then U v else 0) *\<^sub>R v = (if vt then (U v) *\<^sub>R v else 0::'a)"
    by auto
  assume ?lhs
  then obtain T U v where
    "finite T" "T \ S" "sum U T = 0" "v\T" "U v \ 0" "(\v\T. U v *\<^sub>R v) = 0"
    unfolding affine_dependent_explicit by auto
  then show ?rhs
    apply (rule_tac x="\x. if x\T then U x else 0" in exI)
    apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF \<open>T\<subseteq>S\<close>])
    done
next
  assume ?rhs
  then obtain U v where "sum U S = 0"  "v\S" "U v \ 0" "(\v\S. U v *\<^sub>R v) = 0"
    by auto
  then show ?lhs unfolding affine_dependent_explicit
    using assms by auto
qed

lemma dependent_imp_affine_dependent:
  assumes "dependent {x - a| x . x \ S}"
    and "a \ S"
  shows "affine_dependent (insert a S)"
proof -
  from assms(1)[unfolded dependent_explicit] obtain S' U v
    where S: "finite S'" "S' \ {x - a |x. x \ S}" "v\S'" "U v \ 0" "(\v\S'. U v *\<^sub>R v) = 0"
    by auto
  define T where "T = (\x. x + a) ` S'"
  have inj: "inj_on (\x. x + a) S'"
    unfolding inj_on_def by auto
  have "0 \ S'"
    using S(2) assms(2) unfolding subset_eq by auto
  have fin: "finite T" and "T \ S"
    unfolding T_def using S(1,2) by auto
  then have "finite (insert a T)" and "insert a T \ insert a S"
    by auto
  moreover have *: "\P Q. (\x\T. (if x = a then P x else Q x)) = (\x\T. Q x)"
    by (smt (verit, best) \<open>T \<subseteq> S\<close> assms(2) subsetD sum.cong)
  have "(\x\insert a T. if x = a then - (\x\T. U (x - a)) else U (x - a)) = 0"
    by (smt (verit) \<open>T \<subseteq> S\<close> assms(2) fin insert_absorb insert_subset sum.insert sum_mono)
  moreover have "\v\insert a T. (if v = a then - (\x\T. U (x - a)) else U (v - a)) \ 0"
    using S(3,4) \<open>0\<notin>S'\<close>
    by (rule_tac x="v + a" in bexI) (auto simp: T_def)
  moreover have *: "\P Q. (\x\T. (if x = a then P x else Q x) *\<^sub>R x) = (\x\T. Q x *\<^sub>R x)"
    using \<open>a\<notin>S\<close> \<open>T\<subseteq>S\<close> by (auto intro!: sum.cong)
  have "(\x\T. U (x - a)) *\<^sub>R a = (\v\T. U (v - a) *\<^sub>R v)"
    unfolding scaleR_left.sum
    unfolding T_def and sum.reindex[OF inj] and o_def
    using S(5)
    by (auto simp: sum.distrib scaleR_right_distrib)
  then have "(\v\insert a T. (if v = a then - (\x\T. U (x - a)) else U (v - a)) *\<^sub>R v) = 0"
    unfolding sum_clauses(2)[OF fin] using \<open>a\<notin>S\<close> \<open>T\<subseteq>S\<close> by (auto simp: *)
  ultimately show ?thesis
    unfolding affine_dependent_explicit
    by (force intro!: exI[where x="insert a T"])
qed

lemma affine_dependent_biggerset:
  fixes S :: "'a::euclidean_space set"
  assumes "finite S" "card S \ DIM('a) + 2"
  shows "affine_dependent S"
proof -
  have "S \ {}" using assms by auto
  then obtain a where "a\S" by auto
  have *: "{x - a |x. x \ S - {a}} = (\x. x - a) ` (S - {a})"
    by auto
  have "card {x - a |x. x \ S - {a}} = card (S - {a})"
    unfolding * by (simp add: card_image inj_on_def)
  also have "\ > DIM('a)" using assms(2)
    unfolding card_Diff_singleton[OF \<open>a\<in>S\<close>] by auto
  finally  have "affine_dependent (insert a (S - {a}))"
    using dependent_biggerset dependent_imp_affine_dependent by blast
  then show ?thesis
    by (simp add: \<open>a \<in> S\<close> insert_absorb)
qed

lemma affine_dependent_biggerset_general:
  assumes "finite (S :: 'a::euclidean_space set)"
    and "card S \ dim S + 2"
  shows "affine_dependent S"
proof -
  from assms(2) have "S \ {}" by auto
  then obtain a where "a\S" by auto
  have *: "{x - a |x. x \ S - {a}} = (\x. x - a) ` (S - {a})"
    by auto
  have **: "card {x - a |x. x \ S - {a}} = card (S - {a})"
    by (metis (no_types, lifting) "*" card_image diff_add_cancel inj_on_def)
  have "dim {x - a |x. x \ S - {a}} \ dim S"
    using \<open>a\<in>S\<close> by (auto simp: span_base span_diff intro: subset_le_dim)
  also have "\ < dim S + 1" by auto
  also have "\ \ card (S - {a})"
    using assms card_Diff_singleton[OF \<open>a\<in>S\<close>] by auto
  finally have "affine_dependent (insert a (S - {a}))"
    by (smt (verit) Collect_cong dependent_imp_affine_dependent dependent_biggerset_general ** Diff_iff insertCI)
  then show ?thesis
    by (simp add: \<open>a \<in> S\<close> insert_absorb)
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Some Properties of Affine Dependent Sets\<close>

lemma affine_independent_0 [simp]: "\ affine_dependent {}"
  by (simp add: affine_dependent_def)

lemma affine_independent_1 [simp]: "\ affine_dependent {a}"
  by (simp add: affine_dependent_def)

lemma affine_independent_2 [simp]: "\ affine_dependent {a,b}"
  by (simp add: affine_dependent_def insert_Diff_if hull_same)

lemma affine_hull_translation: "affine hull ((\x. a + x) ` S) = (\x. a + x) ` (affine hull S)"
proof -
  have "affine ((\x. a + x) ` (affine hull S))"
    using affine_translation affine_affine_hull by blast
  moreover have "(\x. a + x) ` S \ (\x. a + x) ` (affine hull S)"
    using hull_subset[of S] by auto
  ultimately have h1: "affine hull ((\x. a + x) ` S) \ (\x. a + x) ` (affine hull S)"
    by (metis hull_minimal)
  have "affine((\x. -a + x) ` (affine hull ((\x. a + x) ` S)))"
    using affine_translation affine_affine_hull by blast
  moreover have "(\x. -a + x) ` (\x. a + x) ` S \ (\x. -a + x) ` (affine hull ((\x. a + x) ` S))"
    using hull_subset[of "(\x. a + x) ` S"] by auto
  moreover have "S = (\x. -a + x) ` (\x. a + x) ` S"
    using translation_assoc[of "-a" a] by auto
  ultimately have "(\x. -a + x) ` (affine hull ((\x. a + x) ` S)) >= (affine hull S)"
    by (metis hull_minimal)
  then have "affine hull ((\x. a + x) ` S) >= (\x. a + x) ` (affine hull S)"
    by auto
  then show ?thesis using h1 by auto
qed

lemma affine_dependent_translation:
  assumes "affine_dependent S"
  shows "affine_dependent ((\x. a + x) ` S)"
proof -
  obtain x where x: "x \ S \ x \ affine hull (S - {x})"
    using assms affine_dependent_def by auto
  have "(+) a ` (S - {x}) = (+) a ` S - {a + x}"
    by auto
  then have "a + x \ affine hull ((\x. a + x) ` S - {a + x})"
    using affine_hull_translation[of a "S - {x}"] x by auto
  moreover have "a + x \ (\x. a + x) ` S"
    using x by auto
  ultimately show ?thesis
    unfolding affine_dependent_def by auto
qed

lemma affine_dependent_translation_eq:
  "affine_dependent S \ affine_dependent ((\x. a + x) ` S)"
  by (metis affine_dependent_translation translation_galois)

lemma affine_hull_0_dependent:
  assumes "0 \ affine hull S"
  shows "dependent S"
proof -
  obtain s u where s_u: "finite s \ s \ {} \ s \ S \ sum u s = 1 \ (\v\s. u v *\<^sub>R v) = 0"
    using assms affine_hull_explicit[of S] by auto
  then have "\v\s. u v \ 0" by auto
  then have "finite s \ s \ S \ (\v\s. u v \ 0 \ (\v\s. u v *\<^sub>R v) = 0)"
    using s_u by auto
  then show ?thesis
    unfolding dependent_explicit[of S] by auto
qed

lemma affine_dependent_imp_dependent2:
  assumes "affine_dependent (insert 0 S)"
  shows "dependent S"
proof -
  obtain x where x: "x \ insert 0 S \ x \ affine hull (insert 0 S - {x})"
    using affine_dependent_def[of "(insert 0 S)"] assms by blast
  then have "x \ span (insert 0 S - {x})"
    using affine_hull_subset_span by auto
  moreover have "span (insert 0 S - {x}) = span (S - {x})"
    using insert_Diff_if[of "0" S "{x}"] span_insert_0[of "S-{x}"] by auto
  ultimately have "x \ span (S - {x})" by auto
  then have "x \ 0 \ dependent S"
    using x dependent_def by auto
  moreover have "dependent S" if "x = 0"
    by (metis that affine_hull_0_dependent Diff_insert_absorb dependent_zero x)
  ultimately show ?thesis by auto
qed

lemma affine_dependent_iff_dependent:
  assumes "a \ S"
  shows "affine_dependent (insert a S) \ dependent ((\x. -a + x) ` S)"
proof -
  have "((+) (- a) ` S) = {x - a| x . x \ S}" by auto
  then show ?thesis
    using affine_dependent_translation_eq[of "(insert a S)" "-a"]
      affine_dependent_imp_dependent2 assms
      dependent_imp_affine_dependent[of a S]
    by (auto simp del: uminus_add_conv_diff)
qed

lemma affine_dependent_iff_dependent2:
  assumes "a \ S"
  shows "affine_dependent S \ dependent ((\x. -a + x) ` (S-{a}))"
  by (metis Diff_iff affine_dependent_iff_dependent assms insert_Diff singletonI)

lemma affine_hull_insert_span_gen:
  "affine hull (insert a S) = (\x. a + x) ` span ((\x. - a + x) ` S)"
proof -
  have h1: "{x - a |x. x \ S} = ((\x. -a+x) ` S)"
    by auto
  {
    assume "a \ S"
    then have ?thesis
      using affine_hull_insert_span[of a S] h1 by auto
  }
  moreover
  {
    assume a1: "a \ S"
    then have "insert 0 ((\x. -a+x) ` (S - {a})) = (\x. -a+x) ` S"
      by auto
    then have "span ((\x. -a+x) ` (S - {a})) = span ((\x. -a+x) ` S)"
      using span_insert_0[of "(+) (- a) ` (S - {a})"]
      by presburger
    moreover have "{x - a |x. x \ (S - {a})} = ((\x. -a+x) ` (S - {a}))"
      by auto
    moreover have "insert a (S - {a}) = insert a S"
      by auto
    ultimately have ?thesis
      using affine_hull_insert_span[of "a" "S-{a}"] by auto
  }
  ultimately show ?thesis by auto
qed

lemma affine_hull_span2:
  assumes "a \ S"
  shows "affine hull S = (\x. a+x) ` span ((\x. -a+x) ` (S-{a}))"
  by (metis affine_hull_insert_span_gen assms insert_Diff)

lemma affine_hull_span_gen:
  assumes "a \ affine hull S"
  shows "affine hull S = (\x. a+x) ` span ((\x. -a+x) ` S)"
  by (metis affine_hull_insert_span_gen assms hull_redundant)

lemma affine_hull_span_0:
  assumes "0 \ affine hull S"
  shows "affine hull S = span S"
  using affine_hull_span_gen[of "0" S] assms by auto

lemma extend_to_affine_basis_nonempty:
  fixes S V :: "'n::real_vector set"
  assumes "\ affine_dependent S" "S \ V" "S \ {}"
  shows "\T. \ affine_dependent T \ S \ T \ T \ V \ affine hull T = affine hull V"
proof -
  obtain a where a: "a \ S"
    using assms by auto
  then have h0: "independent ((\x. -a + x) ` (S-{a}))"
    using affine_dependent_iff_dependent2 assms by auto
  obtain B where B:
    "(\x. -a+x) ` (S - {a}) \ B \ B \ (\x. -a+x) ` V \ independent B \ (\x. -a+x) ` V \ span B"
    using assms
    by (blast intro: maximal_independent_subset_extend[OF _ h0, of "(\x. -a + x) ` V"])
  define T where "T = (\x. a+x) ` insert 0 B"
  then have "T = insert a ((\x. a+x) ` B)"
    by auto
  then have "affine hull T = (\x. a+x) ` span B"
    using affine_hull_insert_span_gen[of a "((\x. a+x) ` B)"] translation_assoc[of "-a" a B]
    by auto
  then have "V \ affine hull T"
    using B assms translation_inverse_subset[of a V "span B"]
    by auto
  moreover have "T \ V"
    using T_def B a assms by auto
  ultimately have "affine hull T = affine hull V"
    by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono)
  moreover have "S \ T"
    using T_def B translation_inverse_subset[of a "S-{a}" B]
    by auto
  moreover have "\ affine_dependent T"
    using T_def affine_dependent_translation_eq[of "insert 0 B"]
      affine_dependent_imp_dependent2 B
    by auto
  ultimately show ?thesis using \<open>T \<subseteq> V\<close> by auto
qed

lemma affine_basis_exists:
  fixes V :: "'n::real_vector set"
  shows "\B. B \ V \ \ affine_dependent B \ affine hull V = affine hull B"
  by (metis affine_dependent_def affine_independent_1 empty_subsetI extend_to_affine_basis_nonempty insert_subset order_refl)

proposition extend_to_affine_basis:
  fixes S V :: "'n::real_vector set"
  assumes "\ affine_dependent S" "S \ V"
  obtains T where "\ affine_dependent T" "S \ T" "T \ V" "affine hull T = affine hull V"
  by (metis affine_basis_exists assms(1) assms(2) bot.extremum extend_to_affine_basis_nonempty)

subsection \<open>Affine Dimension of a Set\<close>

definition\<^marker>\<open>tag important\<close> aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
  where "aff_dim V =
  (SOME d :: int.
    \<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"

lemma aff_dim_basis_exists:
  fixes V :: "('n::euclidean_space) set"
  shows "\B. affine hull B = affine hull V \ \ affine_dependent B \ of_nat (card B) = aff_dim V + 1"
proof -
  obtain B where "\ affine_dependent B \ affine hull B = affine hull V"
    using affine_basis_exists[of V] by auto
  then show ?thesis
    unfolding aff_dim_def
      some_eq_ex[of "\d. \B. affine hull B = affine hull V \ \ affine_dependent B \ of_nat (card B) = d + 1"]
    apply auto
    apply (rule exI[of _ "int (card B) - (1 :: int)"])
    apply (rule exI[of _ "B"], auto)
    done
qed

lemma affine_hull_eq_empty [simp]: "affine hull S = {} \ S = {}"
by (metis affine_empty subset_empty subset_hull)

lemma empty_eq_affine_hull[simp]: "{} = affine hull S \ S = {}"
  by (metis affine_hull_eq_empty)

lemma aff_dim_parallel_subspace_aux:
  fixes B :: "'n::euclidean_space set"
  assumes "\ affine_dependent B" "a \ B"
  shows "finite B \ ((card B) - 1 = dim (span ((\x. -a+x) ` (B-{a}))))"
proof -
  have "independent ((\x. -a + x) ` (B-{a}))"
    using affine_dependent_iff_dependent2 assms by auto
  then have fin: "dim (span ((\x. -a+x) ` (B-{a}))) = card ((\x. -a + x) ` (B-{a}))"
    "finite ((\x. -a + x) ` (B - {a}))"
    using indep_card_eq_dim_span[of "(\x. -a+x) ` (B-{a})"] by auto
  show ?thesis
  proof (cases "(\x. -a + x) ` (B - {a}) = {}")
    case True
    have "B = insert a ((\x. a + x) ` (\x. -a + x) ` (B - {a}))"
      using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto
    then have "B = {a}" using True by auto
    then show ?thesis using assms fin by auto
  next
    case False
    then have "card ((\x. -a + x) ` (B - {a})) > 0"
      using fin by auto
    moreover have h1: "card ((\x. -a + x) ` (B-{a})) = card (B-{a})"
      by (rule card_image) (use translate_inj_on in blast)
    ultimately have "card (B-{a}) > 0" by auto
    then have *: "finite (B - {a})"
      using card_gt_0_iff[of "(B - {a})"] by auto
    then have "card (B - {a}) = card B - 1"
      using card_Diff_singleton assms by auto
    with * show ?thesis using fin h1 by auto
  qed
qed

lemma aff_dim_parallel_subspace:
  fixes V L :: "'n::euclidean_space set"
  assumes "V \ {}"
    and "subspace L"
    and "affine_parallel (affine hull V) L"
  shows "aff_dim V = int (dim L)"
proof -
  obtain B where
    B: "affine hull B = affine hull V \ \ affine_dependent B \ int (card B) = aff_dim V + 1"
    using aff_dim_basis_exists by auto
  then have "B \ {}"
    using assms B
    by auto
  then obtain a where a: "a \ B" by auto
  define Lb where "Lb = span ((\x. -a+x) ` (B-{a}))"
  moreover have "affine_parallel (affine hull B) Lb"
    using Lb_def B assms affine_hull_span2[of a B] a
      affine_parallel_commute[of "Lb" "(affine hull B)"]
    unfolding affine_parallel_def
    by auto
  moreover have "subspace Lb"
    using Lb_def subspace_span by auto
  moreover have "affine hull B \ {}"
    using assms B by auto
  ultimately have "L = Lb"
    using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B
    by auto
  then have "dim L = dim Lb"
    by auto
  moreover have "card B - 1 = dim Lb" and "finite B"
    using Lb_def aff_dim_parallel_subspace_aux a B by auto
  ultimately show ?thesis
    using B \<open>B \<noteq> {}\<close> card_gt_0_iff[of B] by auto
qed

lemma aff_independent_finite:
  fixes B :: "'n::euclidean_space set"
  assumes "\ affine_dependent B"
  shows "finite B"
  using aff_dim_parallel_subspace_aux assms finite.simps by fastforce

lemma aff_dim_empty:
  fixes S :: "'n::euclidean_space set"
  shows "S = {} \ aff_dim S = -1"
proof -
  obtain B where *: "affine hull B = affine hull S"
    and "\ affine_dependent B"
    and "int (card B) = aff_dim S + 1"
    using aff_dim_basis_exists by auto
  moreover
  from * have "S = {} \ B = {}"
    by auto
  ultimately show ?thesis
    using aff_independent_finite[of B] card_gt_0_iff[of B] by auto
qed

lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1"
  using aff_dim_empty by blast

lemma aff_dim_affine_hull [simp]: "aff_dim (affine hull S) = aff_dim S"
  unfolding aff_dim_def using hull_hull[of _ S] by auto

lemma aff_dim_affine_hull2:
  assumes "affine hull S = affine hull T"
  shows "aff_dim S = aff_dim T"
  unfolding aff_dim_def using assms by auto

lemma aff_dim_unique:
  fixes B V :: "'n::euclidean_space set"
  assumes "affine hull B = affine hull V \ \ affine_dependent B"
  shows "of_nat (card B) = aff_dim V + 1"
proof (cases "B = {}")
  case True
  then have "V = {}"
    using assms
    by auto
  then have "aff_dim V = (-1::int)"
    using aff_dim_empty by auto
  then show ?thesis
    using \<open>B = {}\<close> by auto
next
  case False
  then obtain a where a: "a \ B" by auto
  define Lb where "Lb = span ((\x. -a+x) ` (B-{a}))"
  have "affine_parallel (affine hull B) Lb"
    using Lb_def affine_hull_span2[of a B] a
      affine_parallel_commute[of "Lb" "(affine hull B)"]
    unfolding affine_parallel_def by auto
  moreover have "subspace Lb"
    using Lb_def subspace_span by auto
  ultimately have "aff_dim B = int(dim Lb)"
    using aff_dim_parallel_subspace[of B Lb] \<open>B \<noteq> {}\<close> by auto
  moreover have "(card B) - 1 = dim Lb" "finite B"
    using Lb_def aff_dim_parallel_subspace_aux a assms by auto
  ultimately have "of_nat (card B) = aff_dim B + 1"
    using \<open>B \<noteq> {}\<close> card_gt_0_iff[of B] by auto
  then show ?thesis
    using aff_dim_affine_hull2 assms by auto
qed

lemma aff_dim_affine_independent:
  fixes B :: "'n::euclidean_space set"
  assumes "\ affine_dependent B"
  shows "of_nat (card B) = aff_dim B + 1"
  using aff_dim_unique[of B B] assms by auto

lemma affine_independent_iff_card:
    fixes S :: "'a::euclidean_space set"
    shows "\ affine_dependent S \ finite S \ aff_dim S = int(card S) - 1" (is "?lhs = ?rhs")
proof
  show "?lhs \ ?rhs"
    by (simp add: aff_dim_affine_independent aff_independent_finite)
  show "?rhs \ ?lhs"
    by (metis of_nat_eq_iff affine_basis_exists aff_dim_unique card_subset_eq diff_add_cancel)
qed

lemma aff_dim_sing [simp]:
  fixes a :: "'n::euclidean_space"
  shows "aff_dim {a} = 0"
  using aff_dim_affine_independent[of "{a}"] affine_independent_1 by auto

lemma aff_dim_2 [simp]:
  fixes a :: "'n::euclidean_space"
  shows "aff_dim {a,b} = (if a = b then 0 else 1)"
proof (clarsimp)
  assume "a \ b"
  then have "aff_dim{a,b} = card{a,b} - 1"
    using affine_independent_2 [of a b] aff_dim_affine_independent by fastforce
  also have "\ = 1"
    using \<open>a \<noteq> b\<close> by simp
  finally show "aff_dim {a, b} = 1" .
qed

lemma aff_dim_inner_basis_exists:
  fixes V :: "('n::euclidean_space) set"
  shows "\B. B \ V \ affine hull B = affine hull V \
    \<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1"
  by (metis aff_dim_unique affine_basis_exists)

lemma aff_dim_le_card:
  fixes V :: "'n::euclidean_space set"
  assumes "finite V"
  shows "aff_dim V \ of_nat (card V) - 1"
  by (metis aff_dim_inner_basis_exists assms card_mono le_diff_eq of_nat_le_iff)

lemma aff_dim_parallel_le:
  fixes S T :: "'n::euclidean_space set"
  assumes "affine_parallel (affine hull S) (affine hull T)"
  shows "aff_dim S \ aff_dim T"
proof (cases "S={} \ T={}")
  case True
  then show ?thesis
    by (smt (verit, best) aff_dim_affine_hull2 affine_hull_empty affine_parallel_def assms empty_is_image)
next
  case False
    then obtain L where L: "subspace L" "affine_parallel (affine hull T) L"
      by (metis affine_affine_hull affine_hull_eq_empty affine_parallel_subspace)
    with False show ?thesis
      by (metis aff_dim_parallel_subspace affine_parallel_assoc assms dual_order.refl)
qed

lemma aff_dim_parallel_eq:
  fixes S T :: "'n::euclidean_space set"
  assumes "affine_parallel (affine hull S) (affine hull T)"
  shows "aff_dim S = aff_dim T"
  by (smt (verit, del_insts) aff_dim_parallel_le affine_parallel_commute assms)

lemma aff_dim_translation_eq:
  "aff_dim ((+) a ` S) = aff_dim S" for a :: "'n::euclidean_space"
  by (metis aff_dim_parallel_eq affine_hull_translation affine_parallel_def)

lemma aff_dim_translation_eq_subtract:
  "aff_dim ((\x. x - a) ` S) = aff_dim S" for a :: "'n::euclidean_space"
  using aff_dim_translation_eq [of "- a"] by (simp cong: image_cong_simp)

lemma aff_dim_affine:
  fixes S L :: "'n::euclidean_space set"
  assumes "affine S" "subspace L" "affine_parallel S L" "S \ {}"
  shows "aff_dim S = int (dim L)"
  by (simp add: aff_dim_parallel_subspace assms hull_same)

lemma dim_affine_hull [simp]:
  fixes S :: "'n::euclidean_space set"
  shows "dim (affine hull S) = dim S"
  by (metis affine_hull_subset_span dim_eq_span dim_mono hull_subset span_eq_dim)

lemma aff_dim_subspace:
  fixes S :: "'n::euclidean_space set"
  assumes "subspace S"
  shows "aff_dim S = int (dim S)"
  by (metis aff_dim_affine affine_parallel_subspace assms empty_iff parallel_subspace subspace_affine)

lemma aff_dim_zero:
  fixes S :: "'n::euclidean_space set"
  assumes "0 \ affine hull S"
  shows "aff_dim S = int (dim S)"
  by (metis aff_dim_affine_hull aff_dim_subspace affine_hull_span_0 assms dim_span subspace_span)

lemma aff_dim_eq_dim:
  fixes S :: "'n::euclidean_space set"
  assumes "a \ affine hull S"
  shows "aff_dim S = int (dim ((+) (- a) ` S))"
  by (metis ab_left_minus aff_dim_translation_eq aff_dim_zero affine_hull_translation image_eqI assms)

lemma aff_dim_eq_dim_subtract:
  fixes S :: "'n::euclidean_space set"
  assumes "a \ affine hull S"
  shows "aff_dim S = int (dim ((\x. x - a) ` S))"
  using aff_dim_eq_dim assms by auto

lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
  by (simp add: aff_dim_subspace)

lemma aff_dim_geq:
  fixes V :: "'n::euclidean_space set"
  shows "aff_dim V \ -1"
  by (metis add_le_cancel_right aff_dim_basis_exists diff_self of_nat_0_le_iff uminus_add_conv_diff)

lemma aff_dim_negative_iff [simp]:
  fixes S :: "'n::euclidean_space set"
  shows "aff_dim S < 0 \ S = {}"
  by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq)

lemma aff_lowdim_subset_hyperplane:
  fixes S :: "'a::euclidean_space set"
  assumes "aff_dim S < DIM('a)"
  obtains a b where "a \ 0" "S \ {x. a \ x = b}"
proof (cases "S={}")
  case True
  moreover
  have "(SOME b. b \ Basis) \ 0"
    by (metis norm_some_Basis norm_zero zero_neq_one)
  ultimately show ?thesis
    using that by blast
next
  case False
  then obtain c S' where "c \ S'" "S = insert c S'"
    by (meson equals0I mk_disjoint_insert)
  have "dim ((+) (-c) ` S) < DIM('a)"
    by (metis \<open>S = insert c S'\<close> aff_dim_eq_dim assms hull_inc insertI1 of_nat_less_imp_less)
  then obtain a where "a \ 0" "span ((+) (-c) ` S) \ {x. a \ x = 0}"
    using lowdim_subset_hyperplane by blast
  moreover
  have "a \ w = a \ c" if "span ((+) (- c) ` S) \ {x. a \ x = 0}" "w \ S" for w
  proof -
    have "w-c \ span ((+) (- c) ` S)"
      by (simp add: span_base \<open>w \<in> S\<close>)
    with that have "w-c \ {x. a \ x = 0}"
      by blast
    then show ?thesis
      by (auto simp: algebra_simps)
  qed
  ultimately have "S \ {x. a \ x = a \ c}"
    by blast
  then show ?thesis
    by (rule that[OF \<open>a \<noteq> 0\<close>])
qed

lemma affine_independent_card_dim_diffs:
  fixes S :: "'a :: euclidean_space set"
  assumes "\ affine_dependent S" "a \ S"
    shows "card S = dim ((\x. x - a) ` S) + 1"
  using aff_dim_affine_independent aff_dim_eq_dim_subtract assms hull_subset by fastforce

lemma independent_card_le_aff_dim:
  fixes B :: "'n::euclidean_space set"
  assumes "B \ V"
  assumes "\ affine_dependent B"
  shows "int (card B) \ aff_dim V + 1"
  by (metis aff_dim_unique aff_independent_finite assms card_mono extend_to_affine_basis of_nat_mono)

lemma aff_dim_subset:
  fixes S T :: "'n::euclidean_space set"
  assumes "S \ T"
  shows "aff_dim S \ aff_dim T"
  by (metis add_le_cancel_right aff_dim_inner_basis_exists assms dual_order.trans independent_card_le_aff_dim)

lemma aff_dim_le_DIM:
  fixes S :: "'n::euclidean_space set"
  shows "aff_dim S \ int (DIM('n))"
  by (metis aff_dim_UNIV aff_dim_subset top_greatest)

lemma affine_dim_equal:
  fixes S :: "'n::euclidean_space set"
  assumes "affine S" "affine T" "S \ {}" "S \ T" "aff_dim S = aff_dim T"
  shows "S = T"
proof -
  obtain a where "a \ S" "a \ T" "T \ {}" using assms by auto
  define LS where "LS = {y. \x \ S. (-a) + x = y}"
  then have ls: "subspace LS" "affine_parallel S LS"
    using assms parallel_subspace_explicit[of S a LS] \<open>a \<in> S\<close> by auto
  then have h1: "int(dim LS) = aff_dim S"
    using assms aff_dim_affine[of S LS] by auto
  define LT where "LT = {y. \x \ T. (-a) + x = y}"
  then have lt: "subspace LT \ affine_parallel T LT"
    using assms parallel_subspace_explicit[of T a LT] \<open>a \<in> T\<close> by auto
  then have "dim LS = dim LT"
    using assms aff_dim_affine[of T LT] \<open>T \<noteq> {}\<close>  h1 by auto
  moreover have "LS \ LT"
    using LS_def LT_def assms by auto
  ultimately have "LS = LT"
    using subspace_dim_equal[of LS LT] ls lt by auto
  moreover have "S = {x. \y \ LS. a+y=x}" "T = {x. \y \ LT. a+y=x}"
    using LS_def LT_def by auto
  ultimately show ?thesis by auto
qed

lemma aff_dim_eq_0:
  fixes S :: "'a::euclidean_space set"
  shows "aff_dim S = 0 \ (\a. S = {a})"
proof (cases "S = {}")
  case False
  then obtain a where "a \ S" by auto
  show ?thesis
  proof safe
    assume 0: "aff_dim S = 0"
    have "\ {a,b} \ S" if "b \ a" for b
      by (metis "0" aff_dim_2 aff_dim_subset not_one_le_zero that)
    then show "\a. S = {a}"
      using \<open>a \<in> S\<close> by blast
  qed auto
qed auto

lemma affine_hull_UNIV:
  fixes S :: "'n::euclidean_space set"
  assumes "aff_dim S = int(DIM('n))"
  shows "affine hull S = (UNIV :: ('n::euclidean_space) set)"
  by (simp add: aff_dim_empty affine_dim_equal assms)

lemma disjoint_affine_hull:
  fixes S :: "'n::euclidean_space set"
  assumes "\ affine_dependent S" "T \ S" "U \ S" "T \ U = {}"
    shows "(affine hull T) \ (affine hull U) = {}"
proof -
  obtain "finite S" "finite T" "finite U"
    using assms by (simp add: aff_independent_finite finite_subset)
  have False if "y \ affine hull T" and "y \ affine hull U" for y
  proof -
    from that obtain a b
      where a1 [simp]: "sum a T = 1"
        and [simp]: "sum (\v. a v *\<^sub>R v) T = y"
        and [simp]: "sum b U = 1" "sum (\v. b v *\<^sub>R v) U = y"
      by (auto simp: affine_hull_finite \<open>finite T\<close> \<open>finite U\<close>)
    define c where "c x = (if x \ T then a x else if x \ U then -(b x) else 0)" for x
    have [simp]: "S \ T = T" "S \ - T \ U = U"
      using assms by auto
    have "sum c S = 0"
      by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite S\<close> sum_negf)
    moreover have "\ (\v\S. c v = 0)"
      by (metis (no_types) IntD1 \<open>S \<inter> T = T\<close> a1 c_def sum.neutral zero_neq_one)
    moreover have "(\v\S. c v *\<^sub>R v) = 0"
      by (simp add: c_def if_smult sum_negf comm_monoid_add_class.sum.If_cases \<open>finite S\<close>)
    ultimately show ?thesis
      using assms(1) \<open>finite S\<close> by (auto simp: affine_dependent_explicit)
  qed
  then show ?thesis by blast
qed

end

quality95%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.26Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.