theorem section16_fenchelConjugate_biconjugate_eq_convexFunctionClosure {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_convexFunction_linearImage_sInf {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (f : (Fin n → ℝ) → EReal) (hf : ConvexFunction f) : ConvexFunction fun (y : Fin m → ℝ) => sInf ((fun (x : EuclideanSpace ℝ (Fin n)) => f x.ofLp) '' {x : EuclideanSpace ℝ (Fin n) | (A x).ofLp = y})

Linear images of convex functions via fiberwise sInf are convex.

theorem section16_fenchelConjugate_adjoint_image_eq_precomp_biconjugate {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (g : (Fin m → ℝ) → EReal) : have gStar := fenchelConjugate m g; have h := fun (xStar : Fin n → ℝ) => sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => gStar yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | (LinearMap.adjoint A) yStar = WithLp.toLp 2 xStar}); fenchelConjugate n h = fun (x : Fin n → ℝ) => fenchelConjugate m gStar (A (WithLp.toLp 2 x)).ofLp

Applying Theorem 16.3.1 to the adjoint gives a biconjugate identity.

theorem section16_fenchelConjugate_adjoint_image_eq_precomp_convexFunctionClosure {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (g : (Fin m → ℝ) → EReal) (hg : ConvexFunction g) : have gStar := fenchelConjugate m g; have h := fun (xStar : Fin n → ℝ) => sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => gStar yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | (LinearMap.adjoint A) yStar = WithLp.toLp 2 xStar}); fenchelConjugate n h = fun (x : Fin n → ℝ) => convexFunctionClosure g (A (WithLp.toLp 2 x)).ofLp

The adjoint-image conjugate equals precomposition by A of the convex-function closure.

theorem section16_fenchelConjugate_precomp_convexFunctionClosure_eq_convexFunctionClosure_adjoint_image {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (g : (Fin m → ℝ) → EReal) (hg : ConvexFunction g) : (fenchelConjugate n fun (x : Fin n → ℝ) => convexFunctionClosure g (A (WithLp.toLp 2 x)).ofLp) = convexFunctionClosure fun (xStar : Fin n → ℝ) => sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => fenchelConjugate m g yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | (LinearMap.adjoint A) yStar = WithLp.toLp 2 xStar})

Theorem 16.3.2: Let A : ℝ^n →ₗ[ℝ] ℝ^m be a linear transformation. For any convex function g on ℝ^m, one has

((cl g)A)^* = cl (A^* g^*).

Here cl denotes the convex-function closure (modeled as convexFunctionClosure), g^* is the Fenchel conjugate fenchelConjugate m g, and A^* g^* is the direct image of g^* under the adjoint of A (modeled by an sInf over the affine fiber {yStar | A^* yStar = xStar}).

theorem section16_polar_linearImage {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (C : Set (Fin n → ℝ)) : {yStar : Fin m → ℝ | ∀ y ∈ (fun (x : Fin n → ℝ) => (A (WithLp.toLp 2 x)).ofLp) '' C, y ⬝ᵥ yStar ≤ 1} = (fun (yStar : Fin m → ℝ) => ((LinearMap.adjoint A) (WithLp.toLp 2 yStar)).ofLp) ⁻¹' {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1}

Corollary 16.3.2.1. Let A : ℝ^n →ₗ[ℝ] ℝ^m be a linear transformation. For any convex set C ⊆ ℝ^n, one has

(A C)^* = A^{*-1} (C^*),

where C^* denotes the polar set and A^{*-1} denotes the preimage under the adjoint A^*.

theorem section16_closure_sublevel_eq_sublevel_convexFunctionClosure_one {n : ℕ} {h : (Fin n → ℝ) → EReal} (hh : ProperConvexFunctionOn Set.univ h) (hInf : ⨅ (x : Fin n → ℝ), h x < 1) : closure {x : EuclideanSpace ℝ (Fin n) | h x.ofLp ≤ 1} = {x : EuclideanSpace ℝ (Fin n) | convexFunctionClosure h x.ofLp ≤ 1}

Closure of a ≤ 1 sublevel set matches the ≤ 1 sublevel of the convex-function closure.

theorem section16_image_adjoint_polar_subset_sublevel_sInf {n m : ℕ} (Aadj : EuclideanSpace ℝ (Fin m) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)) (D : Set (Fin m → ℝ)) : (fun (yStar : Fin m → ℝ) => (Aadj (WithLp.toLp 2 yStar)).ofLp) '' {yStar : Fin m → ℝ | supportFunctionEReal D yStar ≤ 1} ⊆ {xStar : Fin n → ℝ | sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => supportFunctionEReal D yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar}) ≤ 1}

The adjoint image of the support-function sublevel lies in the fiberwise sInf sublevel.

Helper lemmas for the polar/sublevel closure correspondence.

theorem section16_sInf_fiber_zero_le {n m : ℕ} (Aadj : EuclideanSpace ℝ (Fin m) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)) (D : Set (Fin m → ℝ)) : sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => supportFunctionEReal D yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 0}) ≤ 0

The fiberwise sInf at the origin is bounded by 0.

theorem section16_closure_image_adjoint_polar_eq_closure_sublevel_sInf_reverse {n m : ℕ} (Aadj : EuclideanSpace ℝ (Fin m) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)) (D : Set (Fin m → ℝ)) : {xStar : Fin n → ℝ | sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => supportFunctionEReal D yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar}) ≤ 1} ⊆ closure ((fun (yStar : Fin m → ℝ) => (Aadj (WithLp.toLp 2 yStar)).ofLp) '' {yStar : Fin m → ℝ | supportFunctionEReal D yStar ≤ 1})

Reverse inclusion for section16_closure_image_adjoint_polar_eq_closure_sublevel_sInf.

theorem section16_closure_image_adjoint_polar_eq_closure_sublevel_sInf {n m : ℕ} (Aadj : EuclideanSpace ℝ (Fin m) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)) (D : Set (Fin m → ℝ)) : closure ((fun (yStar : Fin m → ℝ) => (Aadj (WithLp.toLp 2 yStar)).ofLp) '' {yStar : Fin m → ℝ | supportFunctionEReal D yStar ≤ 1}) = closure {xStar : Fin n → ℝ | sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => supportFunctionEReal D yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar}) ≤ 1}

The closure of the adjoint image of the polar sublevel equals the closure of the sInf sublevel.

theorem section16_properConvexFunctionOn_h_of_zero_mem_closure {n m : ℕ} (Aadj : EuclideanSpace ℝ (Fin m) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)) (D : Set (Fin m → ℝ)) (hD : Convex ℝ D) (h0D : 0 ∈ closure D) : ProperConvexFunctionOn Set.univ fun (xStar : Fin n → ℝ) => sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => supportFunctionEReal D yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar})

Properness of the fiberwise sInf under 0 ∈ closure D.

theorem section16_iInf_h_lt_one_of_zero_mem_closure {n m : ℕ} (Aadj : EuclideanSpace ℝ (Fin m) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)) (D : Set (Fin m → ℝ)) : ⨅ (xStar : Fin n → ℝ), sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => supportFunctionEReal D yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar}) < 1

The fiberwise infimum is strictly below 1 under 0 ∈ closure D.

theorem section16_polar_preimage_closure_eq_closure_adjoint_image {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (D : Set (Fin m → ℝ)) (hD : Convex ℝ D) (h0D : 0 ∈ closure D) : {xStar : Fin n → ℝ | ∀ x ∈ (fun (x : Fin n → ℝ) => (A (WithLp.toLp 2 x)).ofLp) ⁻¹' closure D, x ⬝ᵥ xStar ≤ 1} = closure ((fun (yStar : Fin m → ℝ) => ((LinearMap.adjoint A) (WithLp.toLp 2 yStar)).ofLp) '' {yStar : Fin m → ℝ | ∀ y ∈ D, y ⬝ᵥ yStar ≤ 1})

Corollary 16.3.2.2. Let A be a linear transformation from ℝ^n to ℝ^m. For any convex set D ⊆ ℝ^m with 0 ∈ cl D, one has

(A⁻¹ (cl D))^* = cl (A^* (D^*)),

where cl is the topological closure of sets, D^* is the polar set, and A^* is the adjoint of A.

theorem section16_sInf_image_fiber_eq_sInf_exists {α : Type u_1} (φ : α → EReal) (S : Set α) : sInf (φ '' S) = sInf {z : EReal | ∃ y ∈ S, z = φ y}

Rewriting sInf of an image by an explicit existential description.

theorem section16_recessionFunction_eq_sSup_unrestricted {n : ℕ} {f : (Fin n → ℝ) → EReal} (y : Fin n → ℝ) : recessionFunction f y = sSup {r : EReal | ∃ (x : Fin n → ℝ), r = f (x + y) - f x}

For a proper function, the recession function agrees with the unrestricted formula.