theorem section16_diag_mem_ri_effectiveDomain_blockSum_iff {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : have g := fun (x : Fin (m * n) → ℝ) => ∑ i : Fin m, f i ((section16_blockLinearMap i) x); (∃ (x : EuclideanSpace ℝ (Fin n)), section16_diagLinearMapE x ∈ euclideanRelativeInterior (m * n) ((fun (z : EuclideanSpace ℝ (Fin (m * n))) => z.ofLp) ⁻¹' effectiveDomain Set.univ g)) ↔ (⋂ (i : Fin m), euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (f i))).Nonempty

Diagonal points in the relative interior of a block-sum domain.

theorem section16_nonempty_iInter_ri_effectiveDomain_iff_not_exists_sum_eq_zero_recession_ineq {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : (¬∃ (xStar : Fin m → Fin n → ℝ), ∑ i : Fin m, xStar i = 0 ∧ ∑ i : Fin m, recessionFunction (fenchelConjugate n (f i)) (xStar i) ≤ 0 ∧ ∑ i : Fin m, recessionFunction (fenchelConjugate n (f i)) (-xStar i) > 0) ↔ (⋂ (i : Fin m), euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (f i))).Nonempty

Corollary 16.2.2. Let f₁, …, fₘ be proper convex functions on ℝⁿ. Then there do not exist vectors x₁⋆, …, xₘ⋆ such that

• x₁⋆ + ⋯ + xₘ⋆ = 0,
• (f₁⋆0⁺)(x₁⋆) + ⋯ + (fₘ⋆0⁺)(xₘ⋆) ≤ 0,
• (f₁⋆0⁺)(-x₁⋆) + ⋯ + (fₘ⋆0⁺)(-xₘ⋆) > 0,

if and only if ri (dom f₁) ∩ ⋯ ∩ ri (dom fₘ) ≠ ∅.

Here dom fᵢ is the effective domain effectiveDomain univ (f i), ri is euclideanRelativeInterior, and (fᵢ⋆0⁺) is represented as recessionFunction (fenchelConjugate n (f i)).

theorem section16_coe_sub_eq_bot_iff_eq_top {a : ℝ} {x : EReal} : ↑a - x = ⊥ → x = ⊤

If (a : EReal) - x = ⊥ with a real, then x = ⊤.

theorem section16_coeReal_sub_sInf_image_eq_sSup_image {α : Type u_1} (S : Set α) (φ : α → EReal) (a : ℝ) : ↑a - sInf (φ '' S) = sSup ((fun (x : α) => ↑a - φ x) '' S)

Subtracting an infimum equals the supremum of the translated values.

theorem section16_sSup_range_sSup_fiber_image_eq_sSup_range_total {α : Type u_1} {β : Type u_2} (A : α → β) (g : α → EReal) : sSup (Set.range fun (y : β) => sSup (g '' {x : α | A x = y})) = sSup (Set.range g)

Collapsing the sup over fibers to a sup over the total space.

theorem section16_dotProduct_map_eq_dotProduct_adjoint {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (x : Fin n → ℝ) (yStar : Fin m → ℝ) : (A (WithLp.toLp 2 x)).ofLp ⬝ᵥ yStar = x ⬝ᵥ ((LinearMap.adjoint A) (WithLp.toLp 2 yStar)).ofLp

Dot product with a linear map equals dot product with the adjoint.

theorem section16_dotProduct_adjoint_map_comm {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (x : Fin n → ℝ) (yStar : Fin m → ℝ) : yStar ⬝ᵥ (A (WithLp.toLp 2 x)).ofLp = ((LinearMap.adjoint A) (WithLp.toLp 2 yStar)).ofLp ⬝ᵥ x

Dot-product identity with swapped arguments, to match support-function conventions.

theorem section16_image_dotProduct_linearImage_eq_image_dotProduct_adjoint {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (C : Set (Fin n → ℝ)) (yStar : Fin m → ℝ) : (fun (y : Fin m → ℝ) => yStar ⬝ᵥ y) '' ((fun (x : Fin n → ℝ) => (A (WithLp.toLp 2 x)).ofLp) '' C) = (fun (x : Fin n → ℝ) => ((LinearMap.adjoint A) (WithLp.toLp 2 yStar)).ofLp ⬝ᵥ x) '' C

The dot-product image of a linear image is reindexed by the adjoint.

theorem section16_range_euclideanSpace_toLp_eq_range {n : ℕ} (g : EuclideanSpace ℝ (Fin n) → EReal) : Set.range g = Set.range fun (x : Fin n → ℝ) => g (WithLp.toLp 2 x)

Reindexing a Set.range along WithLp.toLp does not change the range.

theorem section16_fenchelConjugate_linearImage {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (f : (Fin n → ℝ) → EReal) : (fenchelConjugate m fun (y : Fin m → ℝ) => sInf ((fun (x : EuclideanSpace ℝ (Fin n)) => f x.ofLp) '' {x : EuclideanSpace ℝ (Fin n) | (A x).ofLp = y})) = fun (yStar : Fin m → ℝ) => fenchelConjugate n f ((LinearMap.adjoint A) (WithLp.toLp 2 yStar)).ofLp

Theorem 16.3.1: Let A : ℝ^n →ₗ[ℝ] ℝ^m be a linear transformation. For any convex function f on ℝ^n, the Fenchel conjugate of the direct image A f satisfies

(A f)^* = f^* ∘ A^*,

where (A f) y = inf {f x | A x = y} and A^* is the adjoint of A.

def section16_projFirstLinearMap : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 1)

The first-coordinate projection ℝ² → ℝ as a linear map.

Equations

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

theorem section16_image_fiber_projFirst_eq_range (f : (Fin 2 → ℝ) → EReal) (ξ1 : Fin 1 → ℝ) : (fun (x : EuclideanSpace ℝ (Fin 2)) => f x.ofLp) '' {x : EuclideanSpace ℝ (Fin 2) | (section16_projFirstLinearMap x).ofLp = ξ1} = Set.range fun (ξ2 : ℝ) => f ![ξ1 0, ξ2]

The fiber image of the first-coordinate projection equals the range over the second coordinate.

theorem section16_adjoint_projFirst_to_pair (ξ1Star : Fin 1 → ℝ) : ((LinearMap.adjoint section16_projFirstLinearMap) (WithLp.toLp 2 ξ1Star)).ofLp = ![ξ1Star 0, 0]

The adjoint of the first-coordinate projection sends ξ1Star to (ξ1Star, 0).

theorem section16_fenchelConjugate_inf_over_second_coordinate (f : (Fin 2 → ℝ) → EReal) : have h := fun (ξ1 : Fin 1 → ℝ) => sInf (Set.range fun (ξ2 : ℝ) => f ![ξ1 0, ξ2]); fenchelConjugate 1 h = fun (ξ1Star : Fin 1 → ℝ) => fenchelConjugate 2 f ![ξ1Star 0, 0]

Text 16.0.3: As an illustration of Theorem 16.3.1, let f be a convex function on ℝ² and define h : ℝ → ℝ ∪ {±∞} by

h(ξ₁) = inf_{ξ₂} f(ξ₁, ξ₂).

Equivalently, h is the direct image A f for the projection A : (ξ₁, ξ₂) ↦ ξ₁. The adjoint map A^* sends ξ₁^* to (ξ₁^*, 0), hence

h^*(ξ₁^*) = f^*(ξ₁^*, 0).

theorem section16_deltaStar_linearImage {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (C : Set (Fin n → ℝ)) : deltaStar ((fun (x : Fin n → ℝ) => (A (WithLp.toLp 2 x)).ofLp) '' C) = fun (yStar : Fin m → ℝ) => deltaStar C ((LinearMap.adjoint A) (WithLp.toLp 2 yStar)).ofLp

Corollary 16.3.1.1: Let A be a linear transformation from ℝ^n to ℝ^m. For any convex set C ⊆ ℝ^n, one has δ^*(y^* | A C) = δ^*(A^* y^* | C) for all y^* ∈ ℝ^m.

theorem section16_fenchelConjugate_supportFunctionEReal_eq_indicatorFunction_closure {m : ℕ} (D : Set (Fin m → ℝ)) (hD : Convex ℝ D) : fenchelConjugate m (supportFunctionEReal D) = indicatorFunction (closure D)

The conjugate of the support function is the indicator of the closure.

theorem section16_fiber_set_eq_toLp_fiber_set {n m : ℕ} (Aadj : EuclideanSpace ℝ (Fin m) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)) (xStar : Fin n → ℝ) : {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar} = {yStar : EuclideanSpace ℝ (Fin m) | (Aadj yStar).ofLp = xStar}

Rewriting the adjoint fiber using WithLp.toLp.

theorem section16_convexFunction_linearImage_sInf_part3 {n m : ℕ} (Aadj : EuclideanSpace ℝ (Fin m) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)) (f : (Fin m → ℝ) → EReal) (hf : ConvexFunction f) : ConvexFunction fun (xStar : Fin n → ℝ) => sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => f yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | (Aadj yStar).ofLp = xStar})

Linear images of convex functions via fiberwise sInf are convex.

theorem section16_fenchelConjugate_biconjugate_eq_convexFunctionClosure_part3 {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) : fenchelConjugate n (fenchelConjugate n f) = convexFunctionClosure f

The Fenchel biconjugate of a convex function agrees with its convex-function closure.

theorem section16_supportFunctionEReal_preimage_closure_eq_convexFunctionClosure_adjoint_image {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (D : Set (Fin m → ℝ)) (hD : Convex ℝ D) : supportFunctionEReal ((fun (x : Fin n → ℝ) => (A (WithLp.toLp 2 x)).ofLp) ⁻¹' closure D) = convexFunctionClosure fun (xStar : Fin n → ℝ) => sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => supportFunctionEReal D yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | (LinearMap.adjoint A) yStar = WithLp.toLp 2 xStar})

Corollary 16.3.1.2: Let A be a linear transformation from ℝ^n to ℝ^m. For any convex set D ⊆ ℝ^m, one has

δ^*(· | A⁻¹ (cl D)) = cl (A^* δ^*(· | D)).

Here δ^*(·|D) is the support function, cl D is the topological closure of the set D, and A^* is the adjoint of A. In this development, the closure cl of a function is represented by convexFunctionClosure, and A^* δ^*(·|D) is modeled via an sInf over the affine fiber {yStar | A^* yStar = xStar}.