Theory Convex_More

theory Convex_More
  imports "HOL-Analysis.Starlike"
begin

lemma convex_hull_union_explicit:
  fixes S T :: "'a::euclidean_space set"
  assumes "convex S"
      and "convex T"
    shows "convex hull (S ∪ T) =
            S ∪ T ∪
            {(1 - u) *⇩R x + u *⇩R y | x y u. x ∈ S ∧ y ∈ T ∧ 0 ≤ u ∧ u ≤ 1}"
  (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
  proof
    fix y
    assume "y ∈ convex hull (S ∪ T)"
    then obtain U f where U_facts:
      "finite U" "U ⊆ (S ∪ T)" "(∀x∈U. 0 ≤ f x)" "sum f U = 1" "(∑v∈U. f v *⇩R v) = y"
      unfolding convex_hull_explicit by auto
    have U_partition: "U = (U ∩ S) ∪ (U - S)"
      by auto
    have disjoint: "(U ∩ S) ∩ (U - S) = {}"
      by auto
    have "finite (U ∩ S)" "finite (U - S)" 
      using U_facts(1) by auto

    let ?a = "sum f (U ∩ S)"
    let ?b = "sum f (U - S)"
    have "?a + ?b = 1"
      using sum.union_disjoint[of "U ∩ S" "U - S" f] U_facts(1,4) U_partition disjoint
      by auto
    have vsum_eq: "y = (∑v∈U ∩ S. f v *⇩R v) + (∑v∈U - S. f v *⇩R v)"
      using sum.union_disjoint[of "U ∩ S" "U - S" "λv. f v *⇩R v"]
      using U_facts(1,5) U_partition disjoint
      by auto
    have "0 ≤ ?a" "0 ≤ ?b"
      using U_facts(3)
      by (auto intro: sum_nonneg)

    consider
      (a_zero) "?a = 0" |
      (b_zero) "?a ≠ 0" "?b = 0" |
      (both_pos) "?a ≠ 0" "?b ≠ 0"
      by auto
    then show "y ∈ ?rhs"
    proof cases
      case a_zero
      then have zero_on_S: "∀x∈U ∩ S. f x = 0"
        using U_facts(3) sum_nonneg_eq_0_iff[of "U ∩ S" f]
        by (simp add: ‹finite (U ∩ S)›)
      then have "y = (∑v∈U - S. f v *⇩R v)"
        using vsum_eq by simp
      moreover have "sum f (U - S) = 1"
        using ‹?a + ?b = 1› a_zero
        by simp
      moreover have "U - S ⊆ T"
        using U_facts(2) by auto
      moreover have "∀x∈U - S. 0 ≤ f x"
        using U_facts(3) by auto
      ultimately have "y ∈ T"
        using assms(2) ‹finite (U - S)› unfolding convex_explicit
        by blast
      then show ?thesis by auto
    next
      case b_zero
      then have zero_on_T: "∀x∈U - S. f x = 0"
        using U_facts(3) sum_nonneg_eq_0_iff[of "U - S" f]
        by (simp add: ‹finite (U - S)›)
      then have "y = (∑v∈U ∩ S. f v *⇩R v)"
        using vsum_eq by simp
      moreover have "sum f (U ∩ S) = 1"
        using ‹?a + ?b = 1› b_zero
        by simp
      moreover have "U ∩ S ⊆ S"
        by auto
      moreover have "∀x∈U ∩ S. 0 ≤ f x"
        using U_facts(3) by auto
      ultimately have "y ∈ S"
        using assms(1) ‹finite (U ∩ S)› unfolding convex_explicit
        by blast
      then show ?thesis by auto
    next
      case both_pos
      then have "0 < ?a" "0 < ?b"
        using ‹0 ≤ ?a› ‹0 ≤ ?b› by auto

      let ?x = "∑v∈U ∩ S. (f v / ?a) *⇩R v"
      let ?y' = "∑v∈U - S. (f v / ?b) *⇩R v"

      have "sum (λv. f v / ?a) (U ∩ S) = 1"
        using ‹0 < ?a›
        by (metis both_pos(1) div_self sum_divide_distrib)
      moreover have "∀v∈U ∩ S. 0 ≤ f v / ?a"
        using U_facts(3) ‹0 < ?a› by auto
      ultimately have "?x ∈ S"
        using assms(1) ‹finite (U ∩ S)› unfolding convex_explicit
        by simp

      have "sum (λv. f v / ?b) (U - S) = 1"
        using ‹0 < ?b›
        by (metis both_pos(2) div_self sum_divide_distrib)
      moreover have "∀v∈U - S. 0 ≤ f v / ?b"
        using U_facts(3) ‹0 < ?b› by auto
      moreover have "U - S ⊆ T"
        using U_facts(2) by auto
      ultimately have "?y' ∈ T"
        using assms(2) ‹finite (U - S)› unfolding convex_explicit
        by presburger

      have "(∑v∈U ∩ S. f v *⇩R v) = ?a *⇩R ?x"
        by (smt (verit) both_pos(1) eq_vector_fraction_iff scaleR_right.sum sum.cong)
      moreover have "(∑v∈U - S. f v *⇩R v) = ?b *⇩R ?y'"
        by (smt (verit) both_pos(2) eq_vector_fraction_iff scaleR_right.sum sum.cong)
      ultimately have "y = (1 - ?b) *⇩R ?x + ?b *⇩R ?y'"
        using vsum_eq ‹?a + ?b = 1› by auto

      moreover have "?b ≤ 1"
        using ‹0 ≤ ?a› ‹0 ≤ ?b› ‹?a + ?b = 1›
        by auto

      ultimately show ?thesis
        using ‹0 < ?b› ‹?x ∈ S› ‹?y' ∈ T› by auto
    qed
  qed
next
  have "S ∪ T ⊆ convex hull (S ∪ T)"
    using hull_subset by fast
  then show "?rhs ⊆ ?lhs"
    by (smt (verit, ccfv_threshold) assms(1,2) convex_hull_union_two empty_iff le_sup_iff
        mem_Collect_eq subsetI)
qed

lemma convex_hull_union_nonempty_explicit:
  fixes S T :: "'a::euclidean_space set"
  assumes "convex S"
      and "S ≠ {}"
      and "convex T"
      and "T ≠ {}"
    shows "convex hull (S ∪ T) =
            {(1 - u) *⇩R x + u *⇩R y | x y u. x ∈ S ∧ y ∈ T ∧ 0 ≤ u ∧ u ≤ 1}"
  (is "_ = ?rhs")
proof -
  have "S ⊆ ?rhs"
    using assms(4) by fastforce
  moreover have "T ⊆ ?rhs"
    by (smt (verit, ccfv_threshold) add_0 assms(2) equals0I mem_Collect_eq scaleR_one scaleR_zero_left subset_iff)
  ultimately show ?thesis
    using convex_hull_union_explicit[OF assms(1,3)]
    by blast
qed

lemma convex_hull_isometry:
  assumes "orthogonal_transformation f"
  shows "(λx. c + f x) ` (convex hull S) = convex hull ((λx. c + f x) ` S)"
  using orthogonal_transformation_linear[OF assms] convex_hull_linear_image[of f S]
    convex_hull_translation[of c "f ` S"]
  by (metis image_image)

end