theorem
coneSet_sum_iff_exists_convex_combo
{n : ℕ}
{C1 C2 : Set (Fin n → ℝ)}
(x : Fin n → ℝ)
:
(have K1 := {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C1};
have K2 := {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C2};
have K :=
{p : ℝ × (Fin n → ℝ) | ∃ (r1 : ℝ) (r2 : ℝ) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ),
p.1 = r1 + r2 ∧ p.2 = x1 + x2 ∧ (r1, x1) ∈ K1 ∧ (r2, x2) ∈ K2};
(1, x) ∈ K) ↔ ∃ (r1 : ℝ) (r2 : ℝ) (c1 : Fin n → ℝ) (c2 : Fin n → ℝ),
0 ≤ r1 ∧ 0 ≤ r2 ∧ r1 + r2 = 1 ∧ c1 ∈ C1 ∧ c2 ∈ C2 ∧ x = r1 • c1 + r2 • c2
Membership in the cone-sum set is equivalent to an explicit convex combination.
theorem
coneSet_sum_iff_mem_convexJoin
{n : ℕ}
{C1 C2 : Set (Fin n → ℝ)}
(x : Fin n → ℝ)
:
(have K1 := {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C1};
have K2 := {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C2};
have K :=
{p : ℝ × (Fin n → ℝ) | ∃ (r1 : ℝ) (r2 : ℝ) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ),
p.1 = r1 + r2 ∧ p.2 = x1 + x2 ∧ (r1, x1) ∈ K1 ∧ (r2, x2) ∈ K2};
(1, x) ∈ K) ↔ x ∈ convexJoin ℝ C1 C2
Membership in the cone-sum set is equivalent to membership in the convex join.
theorem
coneSet_sum_iff_convexHull_union
{n : ℕ}
{C1 C2 : Set (Fin n → ℝ)}
(hC1 : Convex ℝ C1)
(hC2 : Convex ℝ C2)
(hC1ne : C1.Nonempty)
(hC2ne : C2.Nonempty)
(x : Fin n → ℝ)
:
have K1 := {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C1};
have K2 := {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ p.2 ∈ p.1 • C2};
have K :=
{p : ℝ × (Fin n → ℝ) | ∃ (r1 : ℝ) (r2 : ℝ) (x1 : Fin n → ℝ) (x2 : Fin n → ℝ),
p.1 = r1 + r2 ∧ p.2 = x1 + x2 ∧ (r1, x1) ∈ K1 ∧ (r2, x2) ∈ K2};
(1, x) ∈ K ↔ x ∈ (convexHull ℝ) (C1 ∪ C2)
theorem
convex_coneSet_sum
{n : ℕ}
{C1 C2 : Set (Fin n → ℝ)}
(hC1 : Convex ℝ C1)
(hC2 : Convex ℝ C2)
:
Text 3.6.11: For convex sets C1 and C2, let
K1 = { (λ, x) | 0 ≤ λ ∧ x ∈ λ • C1 },
K2 = { (λ, x) | 0 ≤ λ ∧ x ∈ λ • C2 }, and
K = { (λ, x) | ∃ λ1 λ2 x1 x2, λ = λ1 + λ2, x = x1 + x2, (λ1, x1) ∈ K1, (λ2, x2) ∈ K2 }.
Then K is convex.