theorem linearMap_relativeInterior_image_eq_and_image_closure_subset (n m : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : ⇑A '' euclideanRelativeInterior n C = euclideanRelativeInterior m (⇑A '' C) ∧ ⇑A '' closure C ⊆ closure (⇑A '' C)

Proposition 9.0.0.1. For a convex set C and linear map A, one has ri (A '' C) = A '' ri C, while in general only closure (A '' C) ⊇ A '' closure C (Theorem 6.6); the text asks when equality holds and when the image of a closed convex set is closed.

theorem image_epigraph_not_closed_and_Ah_not_lsc : have h := fun (x : Fin 2 → ℝ) => if 0 ≤ x 0 ∧ 0 ≤ x 1 then ↑(Real.exp (-√(x 0 * x 1))) else ⊤; have A := fun (x : Fin 2 → ℝ) => x 0; have B := fun (p : (Fin 2 → ℝ) × ℝ) => (A p.1, p.2); have Ah := fun (xi1 : ℝ) => if 0 < xi1 then 0 else if xi1 = 0 then 1 else ⊤; ¬IsClosed (B '' epigraph Set.univ h) ∧ ¬LowerSemicontinuousAt Ah 0

The projected epigraph is not closed, and the induced Ah is not lsc at 0.

theorem image_neg_sqrt_mul_nonneg : (fun (x : Fin 2 → ℝ) => -√(x 0 * x 1)) '' {x : Fin 2 → ℝ | 0 ≤ x 0 ∧ 0 ≤ x 1} = Set.Iic 0

Image of the nonnegative orthant under x ↦ -sqrt(x0*x1) is (-∞, 0].

theorem convexOn_exp_neg_sqrt_mul_nonneg : ConvexOn ℝ {x : Fin 2 → ℝ | 0 ≤ x 0 ∧ 0 ≤ x 1} fun (x : Fin 2 → ℝ) => Real.exp (-√(x 0 * x 1))

Convexity of x ↦ exp(-sqrt(x0*x1)) on the nonnegative orthant.

theorem h_convexFunctionOn_univ : ConvexFunctionOn Set.univ fun (x : Fin 2 → ℝ) => if 0 ≤ x 0 ∧ 0 ≤ x 1 then ↑(Real.exp (-√(x 0 * x 1))) else ⊤

Convexity of the extended-value function h on Set.univ.

theorem h_proper : ProperConvexFunctionOn Set.univ fun (x : Fin 2 → ℝ) => if 0 ≤ x 0 ∧ 0 ≤ x 1 then ↑(Real.exp (-√(x 0 * x 1))) else ⊤

Properness of the function h.

theorem h_lowerSemicontinuous : LowerSemicontinuous fun (x : Fin 2 → ℝ) => if 0 ≤ x 0 ∧ 0 ≤ x 1 then ↑(Real.exp (-√(x 0 * x 1))) else ⊤

Lower semicontinuity of the function h.

theorem projection_epigraph_not_closed_example : have h := fun (x : Fin 2 → ℝ) => if 0 ≤ x 0 ∧ 0 ≤ x 1 then ↑(Real.exp (-√(x 0 * x 1))) else ⊤; have A := fun (x : Fin 2 → ℝ) => x 0; have B := fun (p : (Fin 2 → ℝ) × ℝ) => (A p.1, p.2); have Ah := fun (xi1 : ℝ) => if 0 < xi1 then 0 else if xi1 = 0 then 1 else ⊤; ClosedConvexFunction h ∧ ProperConvexFunctionOn Set.univ h ∧ ¬IsClosed (B '' epigraph Set.univ h) ∧ ¬LowerSemicontinuousAt Ah 0

Example 9.0.0.2. Let h : R^2 -> (-infty, +infty] be given by h(x) = exp[-(xi1 * xi2)^(1/2)] for x = (xi1, xi2) ≥ 0, and h(x) = +infty otherwise. For the projection A (xi1, xi2) = xi1 and B (x, mu) = (A x, mu), the image of epi h under B need not be closed (even though h is closed proper convex), and the image function (Ah) satisfies (Ah)(xi1) = 0 for xi1 > 0, (Ah)(0) = 1, and (Ah)(xi1) = +infty for xi1 < 0, so (Ah) is not lower semicontinuous at 0.

theorem verticalLine_intersection_eq_closedHalfLine_of_minimizer {X : Type u_1} {Y : Type u_2} {A : X → Y} {h : X → ℝ} {y : Y} {F : Set (Y × ℝ)} (hF : F = {p : Y × ℝ | ∃ (x : X), A x = p.1 ∧ h x ≤ p.2}) {x0 : X} (hx0 : A x0 = y ∧ ∀ (z : X), A z = y → h x0 ≤ h z) : have verticalLine := {p : Y × ℝ | p.1 = y}; have closedHalfLine := fun (mu0 : ℝ) => {p : Y × ℝ | p.1 = y ∧ mu0 ≤ p.2}; verticalLine ∩ F = closedHalfLine (h x0)

If x0 minimizes h on the fiber A x = y, then the vertical section of F is the closed half-line starting at h x0.

theorem minimizer_of_verticalLine_eq_closedHalfLine {X : Type u_1} {Y : Type u_2} {A : X → Y} {h : X → ℝ} {y : Y} {F : Set (Y × ℝ)} (hF : F = {p : Y × ℝ | ∃ (x : X), A x = p.1 ∧ h x ≤ p.2}) {mu0 : ℝ} (hline : have verticalLine := {p : Y × ℝ | p.1 = y}; have closedHalfLine := fun (mu0 : ℝ) => {p : Y × ℝ | p.1 = y ∧ mu0 ≤ p.2}; verticalLine ∩ F = closedHalfLine mu0) : ∃ (x : X), A x = y ∧ ∀ (z : X), A z = y → h x ≤ h z

If the vertical section is a closed half-line, then h attains its infimum on the fiber A x = y.

theorem infimum_attained_iff_verticalLine_intersection_closedHalfLine {X : Type u_1} {Y : Type u_2} (A : X → Y) (h : X → ℝ) (y : Y) (F : Set (Y × ℝ)) (hF : F = {p : Y × ℝ | ∃ (x : X), A x = p.1 ∧ h x ≤ p.2}) (hne : ∃ (x : X), A x = y) : (∃ (x : X), A x = y ∧ ∀ (z : X), A z = y → h x ≤ h z) ↔ have verticalLine := {p : Y × ℝ | p.1 = y}; have closedHalfLine := fun (mu0 : ℝ) => {p : Y × ℝ | p.1 = y ∧ mu0 ≤ p.2}; (∃ (mu0 : ℝ), verticalLine ∩ F = closedHalfLine mu0) ∨ verticalLine ∩ F = ∅

Proposition 9.0.0.3. The value (A h)(y) is the infimum of h on the affine set {x | A x = y}; the infimum is attained iff the vertical line {(y, mu) | mu ∈ Real} meets F in a closed half-line (or is empty), which would hold if F is closed and has no downward direction of recession.

theorem image_A_C_eq_Ioi : (fun (x : Fin 2 → ℝ) => x 0) '' {x : Fin 2 → ℝ | 0 < x 0 ∧ x 1 ≥ (x 0)⁻¹} = Set.Ioi 0

The projection of C is (0, +∞).

theorem convex_C : Convex ℝ {x : Fin 2 → ℝ | 0 < x 0 ∧ x 1 ≥ (x 0)⁻¹}

Convexity of the set {x | 0 < x 0 ∧ x 1 ≥ (x 0)⁻¹}.

theorem seqClosed_C : IsSeqClosed {x : Fin 2 → ℝ | 0 < x 0 ∧ x 1 ≥ (x 0)⁻¹}

Sequential closedness of the set {x | 0 < x 0 ∧ x 1 ≥ (x 0)⁻¹}.

theorem projection_closed_convex_not_closed_image_example : have C := {x : Fin 2 → ℝ | 0 < x 0 ∧ x 1 ≥ (x 0)⁻¹}; have A := fun (x : Fin 2 → ℝ) => x 0; IsClosed C ∧ Convex ℝ C ∧ ¬IsClosed (A '' C)

Example 9.0.0.4. The closed convex set C = {(xi1, xi2) | xi1 > 0, xi2 ≥ xi1^{-1}} in ℝ^2 has nonclosed projection A (xi1, xi2) = xi1; the difficulty is that C is asymptotic to a vertical line, and the recession cone condition rules out directions (0,1) and (0,-1).

theorem lineality_inter_kernel_nonempty {n m : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : ((closure C).linealitySpace ∩ ↑(LinearMap.ker A)).Nonempty

Theorem 9.1. Let C be a non-empty convex set in ℝ^n, and let A be a linear transformation from ℝ^n to ℝ^m. Assume that every non-zero vector z ∈ 0+ (cl C) satisfying Az = 0 belongs to the lineality space of cl C. Then cl (A C) = A (cl C) and 0+ (A (cl C)) = A (0+ (cl C)). In particular, if C is closed, and z = 0 is the only z ∈ 0+ C such that Az = 0, then A C is closed.

theorem recessionCone_inter_kernel_eq_lineality_inter_kernel {n m : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (hlineal : ∀ (z : EuclideanSpace ℝ (Fin n)), z ≠ 0 → z ∈ (closure C).recessionCone → A z = 0 → z ∈ (closure C).linealitySpace) : (closure C).recessionCone ∩ ↑(LinearMap.ker A) = (closure C).linealitySpace ∩ ↑(LinearMap.ker A)

Kernel intersection of the recession cone equals the kernel intersection of the lineality space under the kernel-lineality hypothesis.

theorem image_closure_eq_image_Lperp_inter {n m : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (L0 : Submodule ℝ (EuclideanSpace ℝ (Fin n))) (hL0 : ↑L0 = (closure C).linealitySpace) : have L := L0 ⊓ LinearMap.ker A; ⇑A '' closure C = ⇑A '' (↑Lᗮ ∩ closure C)

Projecting along lin(closure C) ∩ ker A preserves the image of closure C.

theorem recessionCone_submodule_eq {n : ℕ} (L : Submodule ℝ (EuclideanSpace ℝ (Fin n))) : (↑L).recessionCone = ↑L

The recession cone of a submodule is the submodule itself.

theorem Ceps_nonempty_closed_bounded {n m : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (L0 : Submodule ℝ (EuclideanSpace ℝ (Fin n))) (hL0 : ↑L0 = (closure C).linealitySpace) (hlineal : ∀ (z : EuclideanSpace ℝ (Fin n)), z ≠ 0 → z ∈ (closure C).recessionCone → A z = 0 → z ∈ (closure C).linealitySpace) {y : EuclideanSpace ℝ (Fin m)} (hy : y ∈ closure (⇑A '' C)) {ε : ℝ} (hε : 0 < ε) : have L := L0 ⊓ LinearMap.ker A; have Dε := ⇑A ⁻¹' Metric.closedBall y ε; have Cε := ↑Lᗮ ∩ closure C ∩ Dε; Cε.Nonempty ∧ IsClosed Cε ∧ Bornology.IsBounded Cε

The approximation sets near a closure point of the image are closed and bounded.

theorem closure_image_eq_image_closure_of_kernel_lineality {n m : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (hlineal : ∀ (z : EuclideanSpace ℝ (Fin n)), z ≠ 0 → z ∈ (closure C).recessionCone → A z = 0 → z ∈ (closure C).linealitySpace) : closure (⇑A '' C) = ⇑A '' closure C

Closure of the image equals the image of the closure under the kernel-lineality hypothesis.

theorem recessionCone_add_mem {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCconv : Convex ℝ C) {y₁ y₂ : EuclideanSpace ℝ (Fin n)} (hy₁ : y₁ ∈ C.recessionCone) (hy₂ : y₂ ∈ C.recessionCone) : y₁ + y₂ ∈ C.recessionCone

The recession cone of a convex set is closed under addition.