The append affine equivalence fixes the origin, hence equals its linear part.
theorem
addLinearMap_image_directSum_eq_add
(n : ℕ)
(C1 C2 : Set (EuclideanSpace ℝ (Fin n)))
:
have A :=
(LinearMap.fst ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin n)) + LinearMap.snd ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin n))) ∘ₗ ↑(appendAffineEquiv n n).symm.linear;
⇑A '' directSumSetEuclidean n n C1 C2 = C1 + C2
The addition linear map sends the direct-sum set to the Minkowski sum.
theorem
convex_directSumSetEuclidean
(n : ℕ)
(C1 C2 : Set (EuclideanSpace ℝ (Fin n)))
(hC1 : Convex ℝ C1)
(hC2 : Convex ℝ C2)
:
Convex ℝ (directSumSetEuclidean n n C1 C2)
Convexity of the direct-sum set.
theorem
convex_directSumSetEuclidean_general
(n m : ℕ)
(C1 : Set (EuclideanSpace ℝ (Fin n)))
(C2 : Set (EuclideanSpace ℝ (Fin m)))
(hC1 : Convex ℝ C1)
(hC2 : Convex ℝ C2)
:
Convex ℝ (directSumSetEuclidean n m C1 C2)
Convexity of a direct-sum set in general dimensions.
theorem
euclideanRelativeInterior_add_eq_and_closure_add_superset
(n : ℕ)
(C1 C2 : Set (EuclideanSpace ℝ (Fin n)))
(hC1 : Convex ℝ C1)
(hC2 : Convex ℝ C2)
:
euclideanRelativeInterior n (C1 + C2) = euclideanRelativeInterior n C1 + euclideanRelativeInterior n C2 ∧ closure C1 + closure C2 ⊆ closure (C1 + C2)
Corollary 6.6.2. For any convex sets C1 and C2 in R^n,
ri (C1 + C2) = ri C1 + ri C2, and cl (C1 + C2) ⊇ cl C1 + cl C2.
theorem
preimage_eq_proj_graph_inter_directSum
(n m : ℕ)
(A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m))
(S : Set (EuclideanSpace ℝ (Fin m)))
:
have e := appendAffineEquiv n m;
have P := LinearMap.fst ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin m)) ∘ₗ ↑e.symm.linear;
have M := AffineSubspace.map (↑e) A.graph.toAffineSubspace;
have D_S := directSumSetEuclidean n m Set.univ S;
⇑P '' (↑M ∩ D_S) = ⇑A ⁻¹' S
Projection of a graph intersected with a direct-sum set recovers the preimage.
theorem
ri_closure_directSum_univ_eq
(n m : ℕ)
(C : Set (EuclideanSpace ℝ (Fin m)))
:
have D := directSumSetEuclidean n m Set.univ C;
euclideanRelativeInterior (n + m) D = directSumSetEuclidean n m Set.univ (euclideanRelativeInterior m C) ∧ closure D = directSumSetEuclidean n m Set.univ (closure C)
Relative interior and closure of univ ⊕ C.
theorem
graph_inter_ri_directSum_nonempty
(n m : ℕ)
(A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m))
(C : Set (EuclideanSpace ℝ (Fin m)))
(hri : (⇑A ⁻¹' euclideanRelativeInterior m C).Nonempty)
:
have e := appendAffineEquiv n m;
have M := AffineSubspace.map (↑e) A.graph.toAffineSubspace;
have D := directSumSetEuclidean n m Set.univ C;
(↑M ∩ euclideanRelativeInterior (n + m) D).Nonempty
A preimage point gives a graph point in the relative interior of the direct-sum set.
theorem
euclideanRelativeInterior_preimage_linearMap_eq_and_closure_preimage
(n m : ℕ)
(A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m))
(C : Set (EuclideanSpace ℝ (Fin m)))
(hC : Convex ℝ C)
(hri : (⇑A ⁻¹' euclideanRelativeInterior m C).Nonempty)
:
Theorem 6.7: Let A be a linear transformation from R^n to R^m. Let C be a convex
set in R^m such that A ⁻¹' (ri C) is nonempty. Then
ri (A ⁻¹' C) = A ⁻¹' (ri C) and cl (A ⁻¹' C) = A ⁻¹' (cl C).
theorem
section_D_eq_image_projection
(m p : ℕ)
(C : Set (EuclideanSpace ℝ (Fin (m + p))))
(y : EuclideanSpace ℝ (Fin m))
(z : EuclideanSpace ℝ (Fin p))
:
have e := appendAffineEquiv m p;
have P := LinearMap.fst ℝ (EuclideanSpace ℝ (Fin m)) (EuclideanSpace ℝ (Fin p)) ∘ₗ ↑e.symm.linear;
have Cy := fun (y : EuclideanSpace ℝ (Fin m)) => {z : EuclideanSpace ℝ (Fin p) | e (y, z) ∈ C};
have D := {y : EuclideanSpace ℝ (Fin m) | (Cy y).Nonempty};
D = ⇑P '' C ∧ P (e (y, z)) = y
The projection from R^{m+p} onto R^m identifies the section domain.
theorem
section_fiber_affineSubspace_eq
(m p : ℕ)
(C : Set (EuclideanSpace ℝ (Fin (m + p))))
(y : EuclideanSpace ℝ (Fin m))
:
have e := appendAffineEquiv m p;
have P := LinearMap.fst ℝ (EuclideanSpace ℝ (Fin m)) (EuclideanSpace ℝ (Fin p)) ∘ₗ ↑e.symm.linear;
have Cy := fun (y : EuclideanSpace ℝ (Fin m)) => {z : EuclideanSpace ℝ (Fin p) | e (y, z) ∈ C};
have M := AffineSubspace.mk' (e (y, 0)) (LinearMap.ker P);
↑M = {w : EuclideanSpace ℝ (Fin (m + p)) | P w = y} ∧ ↑M ∩ C = (fun (z : EuclideanSpace ℝ (Fin p)) => e (y, z)) '' Cy y
The projection fiber is an affine subspace, and its intersection with C is the section.
theorem
ri_fiber_eq_ri_section
(m p : ℕ)
(C : Set (EuclideanSpace ℝ (Fin (m + p))))
(hC : Convex ℝ C)
(y : EuclideanSpace ℝ (Fin m))
:
have e := appendAffineEquiv m p;
have Cy := fun (y : EuclideanSpace ℝ (Fin m)) => {z : EuclideanSpace ℝ (Fin p) | e (y, z) ∈ C};
euclideanRelativeInterior (m + p) (directSumSetEuclidean m p {y} (Cy y)) = (fun (z : EuclideanSpace ℝ (Fin p)) => e (y, z)) '' euclideanRelativeInterior p (Cy y)
Relative interior of a section {y} ⊕ C_y is the image of ri C_y.
theorem
euclideanRelativeInterior_mem_iff_relativeInterior_section
(m p : ℕ)
(C : Set (EuclideanSpace ℝ (Fin (m + p))))
(hC : Convex ℝ C)
(y : EuclideanSpace ℝ (Fin m))
(z : EuclideanSpace ℝ (Fin p))
:
have append := fun (y : EuclideanSpace ℝ (Fin m)) (z : EuclideanSpace ℝ (Fin p)) =>
(EuclideanSpace.equiv (Fin (m + p)) ℝ).symm
((Fin.appendIsometry m p) ((EuclideanSpace.equiv (Fin m) ℝ) y, (EuclideanSpace.equiv (Fin p) ℝ) z));
have Cy := fun (y : EuclideanSpace ℝ (Fin m)) => {z : EuclideanSpace ℝ (Fin p) | append y z ∈ C};
have D := {y : EuclideanSpace ℝ (Fin m) | (Cy y).Nonempty};
append y z ∈ euclideanRelativeInterior (m + p) C ↔ y ∈ euclideanRelativeInterior m D ∧ z ∈ euclideanRelativeInterior p (Cy y)
Theorem 6.8: Let C be a convex set in R^{m+p}. For each y ∈ R^m, let C_y be the set
of vectors z ∈ R^p such that (y, z) ∈ C. Let D = {y | C_y ≠ ∅}. Then (y, z) ∈ ri C if and
only if y ∈ ri D and z ∈ ri C_y.
Convexity of the slice {v | first v = 1 ∧ tail v ∈ C}.
theorem
mem_K_iff_first_tail
(n : ℕ)
(C : Set (EuclideanSpace ℝ (Fin n)))
(hC : Convex ℝ C)
:
have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ);
have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0;
have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) =>
(EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i);
have S := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C};
have K := ↑(ConvexCone.hull ℝ S);
∀ (v : EuclideanSpace ℝ (Fin (1 + n))), v ∈ K ↔ 0 < first v ∧ tail v ∈ first v • C
Membership in the generated cone in terms of the first and tail coordinates.
theorem
first_tail_append
(n : ℕ)
(y : EuclideanSpace ℝ (Fin 1))
(z : EuclideanSpace ℝ (Fin n))
:
have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ);
have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0;
have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) =>
(EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i);
have append := fun (y : EuclideanSpace ℝ (Fin 1)) (z : EuclideanSpace ℝ (Fin n)) =>
(EuclideanSpace.equiv (Fin (1 + n)) ℝ).symm
((Fin.appendIsometry 1 n) ((EuclideanSpace.equiv (Fin 1) ℝ) y, (EuclideanSpace.equiv (Fin n) ℝ) z));
first (append y z) = (EuclideanSpace.equiv (Fin 1) ℝ) y 0 ∧ tail (append y z) = z
First and tail coordinates of the append map for m = 1.