theorem mem_ker_linearMap_prod_iff {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (p : (Fin n → ℝ) × ℝ) : p ∈ LinearMap.ker (linearMap_prod A) ↔ A p.1 = 0 ∧ p.2 = 0

Membership in the kernel of linearMap_prod is componentwise.

theorem recessionCone_image_linearEquiv {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (e : E ≃ₗ[ℝ] F) (C : Set E) : (⇑e '' C).recessionCone = ⇑e '' C.recessionCone

Recession cones commute with linear equivalences.

theorem recessionCone_embedded_epigraph_eq_epigraph_h0_plus {n : ℕ} {h h0_plus : (Fin n → ℝ) → EReal} (hrec : (epigraph Set.univ h).recessionCone = epigraph Set.univ h0_plus) : (⇑prodLinearEquiv_append '' epigraph Set.univ h).recessionCone = ⇑prodLinearEquiv_append '' epigraph Set.univ h0_plus

The recession cone of the embedded epigraph is the embedded epigraph of h0_plus.

theorem h0_plus_neg_ge_neg_of_posHom_proper {n : ℕ} {h0_plus : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous h0_plus) (hproper : ProperConvexFunctionOn Set.univ h0_plus) (z : Fin n → ℝ) : h0_plus (-z) ≥ -h0_plus z

Corollary 4.7.2 specialized to h0_plus.

theorem properConvexFunctionOn_precomp_linearMap_surjective {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hA : Function.Surjective ⇑A) {f : (Fin m → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => f (A x)

Precomposition with a surjective linear map preserves proper convexity on Set.univ.

theorem lineality_of_kernel_recession_embedded_epigraph {n m : ℕ} {h h0_plus : (Fin n → ℝ) → EReal} (hclosed : ClosedConvexFunction h) (hrec : (epigraph Set.univ h).recessionCone = epigraph Set.univ h0_plus) (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hA : ∀ (z : Fin n → ℝ), h0_plus z ≤ 0 → h0_plus (-z) > 0 → A z ≠ 0) (z : EuclideanSpace ℝ (Fin (n + 1))) : z ≠ 0 → z ∈ (closure (⇑prodLinearEquiv_append '' epigraph Set.univ h)).recessionCone → (linearMap_prod_embedded A) z = 0 → z ∈ (closure (⇑prodLinearEquiv_append '' epigraph Set.univ h)).linealitySpace

Kernel directions in the embedded recession cone are lineality directions.

theorem no_downward_vertical_recession_image_epigraph {n m : ℕ} {h h0_plus : (Fin n → ℝ) → EReal} (hclosed : ClosedConvexFunction h) (hproper : ProperConvexFunctionOn Set.univ h) (hrec : (epigraph Set.univ h).recessionCone = epigraph Set.univ h0_plus) (hpos : PositivelyHomogeneous h0_plus) (hproper0 : ProperConvexFunctionOn Set.univ h0_plus) (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hA : ∀ (z : Fin n → ℝ), h0_plus z ≤ 0 → h0_plus (-z) > 0 → A z ≠ 0) : ¬∃ μ < 0, (0, μ) ∈ (⇑(linearMap_prod A) '' epigraph Set.univ h).recessionCone

The image epigraph has no downward vertical recession directions under h0_plus.

theorem image_epigraph_linearMap_eq {n m : ℕ} {h : (Fin n → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : ⇑(linearMap_prod A) '' epigraph Set.univ h = {p : (Fin m → ℝ) × ℝ | ∃ (x : Fin n → ℝ), A x = p.1 ∧ h x ≤ ↑p.2}

The image of the epigraph under the lifted linear map.

theorem image_epigraph_linearMap_subset_epigraph_infimum {n m : ℕ} {h : (Fin n → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : ⇑(linearMap_prod A) '' epigraph Set.univ h ⊆ epigraph Set.univ fun (y : Fin m → ℝ) => sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x}

The projected epigraph is contained in the epigraph of the fiber infimum.

theorem exists_preimage_of_sInf_ne_top {n m : ℕ} {h : (Fin n → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) {y : Fin m → ℝ} (hy : sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x} ≠ ⊤) : ∃ (x : Fin n → ℝ), A x = y

If the fiber infimum is not ⊤, then the fiber is nonempty.

theorem exists_preimage_of_sInf_lt {n m : ℕ} {h : (Fin n → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) {y : Fin m → ℝ} {μ : ℝ} (hμ : sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x} < ↑μ) : ∃ (x : Fin n → ℝ), A x = y ∧ h x ≤ ↑μ

If the fiber infimum is strictly below a real bound, there is a fiber point below that bound.

theorem epigraph_infimum_eq_image_of_closed_image {n m : ℕ} {h : (Fin n → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hclosed : IsClosed (⇑(linearMap_prod A) '' epigraph Set.univ h)) : (epigraph Set.univ fun (y : Fin m → ℝ) => sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x}) = ⇑(linearMap_prod A) '' epigraph Set.univ h

Closed image of the epigraph identifies the epigraph of the fiber infimum.

theorem exists_negative_vertical_recession_of_bot {n m : ℕ} {h : (Fin n → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hproper : ProperConvexFunctionOn Set.univ h) (himage_closed : IsClosed (⇑(linearMap_prod A) '' epigraph Set.univ h)) (hEq_epi : (epigraph Set.univ fun (y : Fin m → ℝ) => sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x}) = ⇑(linearMap_prod A) '' epigraph Set.univ h) {y : Fin m → ℝ} (hbot : sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x} = ⊥) : ∃ μ < 0, (0, μ) ∈ (⇑(linearMap_prod A) '' epigraph Set.univ h).recessionCone

If a fiber infimum is ⊥, the projected epigraph has a negative vertical recession direction.

theorem linearMap_infimum_closed_proper_convex_recession {n m : ℕ} {h h0_plus : (Fin n → ℝ) → EReal} (hclosed : ClosedConvexFunction h) (hproper : ProperConvexFunctionOn Set.univ h) (hrec : (epigraph Set.univ h).recessionCone = epigraph Set.univ h0_plus) (hpos : PositivelyHomogeneous h0_plus) (hproper0 : ProperConvexFunctionOn Set.univ h0_plus) (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hA : ∀ (z : Fin n → ℝ), h0_plus z ≤ 0 → h0_plus (-z) > 0 → A z ≠ 0) : have Ah := fun (y : Fin m → ℝ) => sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x}; have Ah0_plus := fun (y : Fin m → ℝ) => sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h0_plus x}; ClosedConvexFunction Ah ∧ ProperConvexFunctionOn Set.univ Ah ∧ (Ah0_plus = fun (y : Fin m → ℝ) => sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h0_plus x}) ∧ ∀ (y : Fin m → ℝ), Ah y ≠ ⊤ → ∃ (x : Fin n → ℝ), A x = y ∧ Ah y = h x

Theorem 9.2. Let h be a closed proper convex function on R^n, and let A be a linear transformation from R^n to R^m. Assume that A z ≠ 0 for every z such that (h0^+)(z) ≤ 0 and (h0^+)(-z) > 0. Then the function Ah, where (Ah)(y) = inf { h(x) | A x = y }, is a closed proper convex function, and (Ah)0^+ = A(h0^+). Moreover, for each y such that (Ah)(y) ≠ +infty, the infimum in the definition of (Ah)(y) is attained for some x.

theorem h0_plus_le_zero_imp_zero {n : ℕ} {h0_plus : (Fin n → ℝ) → EReal} (hno : ∀ (z : Fin n → ℝ), z ≠ 0 → h0_plus z > 0) (z : Fin n → ℝ) : h0_plus z ≤ 0 → z = 0

If h0_plus is strictly positive away from zero, then h0_plus z ≤ 0 forces z = 0.

theorem h0_plus_neg_eq_zero_of_z_eq_zero {n : ℕ} {h0_plus : (Fin n → ℝ) → EReal} (hzero : h0_plus 0 = 0) (z : Fin n → ℝ) : z = 0 → h0_plus (-z) = 0

If z = 0 and h0_plus 0 = 0, then h0_plus (-z) = 0.

def sumLinearMapFun {n m : ℕ} : (Fin m → Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ

The coordinate-sum linear map on function blocks.

Equations

• sumLinearMapFun = { toFun := fun (x : Fin m → Fin n → ℝ) => ∑ i : Fin m, x i, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def blockEquivFun {n m : ℕ} : (Fin (m * n) → ℝ) ≃ₗ[ℝ] Fin m → Fin n → ℝ

Linear equivalence between Fin (m * n) → Real and block functions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def blockSumLinearMapFun {n m : ℕ} : (Fin (m * n) → ℝ) →ₗ[ℝ] Fin n → ℝ

Block-sum linear map on function spaces.

Equations

• blockSumLinearMapFun = sumLinearMapFun ∘ₗ ↑blockEquivFun

theorem linearMap_infimum_hypothesis_trivial_of_no_recession_direction {n m : ℕ} {h0_plus : (Fin n → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hno : ∀ (z : Fin n → ℝ), z ≠ 0 → h0_plus z > 0) (hzero : h0_plus 0 = 0) (z : Fin n → ℝ) : h0_plus z ≤ 0 → h0_plus (-z) > 0 → A z ≠ 0

Remark 9.2.0.2. The hypothesis of Theorem 9.2 concerning h0_plus is trivially satisfied if h has no directions of recession, in particular if dom h is bounded; the example at the beginning of this section violates this hypothesis.