theorem section16_fenchelConjugate_precomp_eq_adjoint_image_of_exists_mem_ri_effectiveDomain {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (g : (Fin m → ℝ) → EReal) (hg : ConvexFunction g) (hri : ∃ (x : EuclideanSpace ℝ (Fin n)), A x ∈ euclideanRelativeInterior m ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' effectiveDomain Set.univ g)) : have Aadj := LinearMap.adjoint A; ((fenchelConjugate n fun (x : Fin n → ℝ) => g (A (WithLp.toLp 2 x)).ofLp) = fun (xStar : Fin n → ℝ) => sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => fenchelConjugate m g yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar})) ∧ ∀ (xStar : Fin n → ℝ), sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => fenchelConjugate m g yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar}) = ⊤ ∨ ∃ (yStar : EuclideanSpace ℝ (Fin m)), Aadj yStar = WithLp.toLp 2 xStar ∧ fenchelConjugate m g yStar.ofLp = sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => fenchelConjugate m g yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar})

Theorem 16.3.3: Let A : ℝ^n →ₗ[ℝ] ℝ^m be a linear transformation. For a convex function g on ℝ^m, if there exists x with A x ∈ ri (dom g), then the closure operation in Theorem 16.3.2 can be omitted, i.e. (g ∘ A)^* = A^* g^*.

Equivalently, for each xStar, one has

(g ∘ A)^*(xStar) = inf { g^*(yStar) | A^* yStar = xStar },

and the infimum is attained (or the value is +∞ if the affine fiber is empty).

theorem section16_fenchelConjugate_sum_inner_precomp_of_exists_mem_ri_effectiveDomain {n m : ℕ} (a : Fin m → EuclideanSpace ℝ (Fin n)) (g1 : Fin m → ℝ → EReal) (hg : ConvexFunction fun (y : Fin m → ℝ) => ∑ i : Fin m, g1 i (y i)) (hri : ∃ (x : EuclideanSpace ℝ (Fin n)), (↑(WithLp.linearEquiv 2 ℝ (Fin m → ℝ)).symm ∘ₗ LinearMap.pi fun (i : Fin m) => ↑((innerSL ℝ) (a i))) x ∈ euclideanRelativeInterior m ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' effectiveDomain Set.univ fun (y : Fin m → ℝ) => ∑ i : Fin m, g1 i (y i))) : have g := fun (y : Fin m → ℝ) => ∑ i : Fin m, g1 i (y i); have A := ↑(WithLp.linearEquiv 2 ℝ (Fin m → ℝ)).symm ∘ₗ LinearMap.pi fun (i : Fin m) => ↑((innerSL ℝ) (a i)); have h := fun (x : Fin n → ℝ) => g (A (WithLp.toLp 2 x)).ofLp; have Aadj := LinearMap.adjoint A; (fenchelConjugate n h = fun (xStar : Fin n → ℝ) => sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => fenchelConjugate m g yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar})) ∧ ∀ (xStar : Fin n → ℝ), sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => fenchelConjugate m g yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar}) = ⊤ ∨ ∃ (yStar : EuclideanSpace ℝ (Fin m)), Aadj yStar = WithLp.toLp 2 xStar ∧ fenchelConjugate m g yStar.ofLp = sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => fenchelConjugate m g yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar})

Text 16.0.4: Example of the conjugate of a function built from one-dimensional convex functions and linear functionals.

Let h : ℝⁿ → ℝ ∪ {±∞} be given by h(x) = g₁(⟪a₁, x⟫) + ⋯ + gₘ(⟪aₘ, x⟫), where each gᵢ is closed proper convex on ℝ and a₁, …, aₘ ∈ ℝⁿ. Writing h = g ∘ A where A x = (⟪a₁, x⟫, …, ⟪aₘ, x⟫) and g(η₁, …, ηₘ) = g₁(η₁) + ⋯ + gₘ(ηₘ), one has g^*(η₁⋆, …, ηₘ⋆) = g₁^*(η₁⋆) + ⋯ + gₘ^*(ηₘ⋆). Therefore (A^* g^*)(x⋆) is the infimum of g₁^*(η₁⋆) + ⋯ + gₘ^*(ηₘ⋆) over all (η₁⋆, …, ηₘ⋆) such that η₁⋆ a₁ + ⋯ + ηₘ⋆ aₘ = x⋆.

The conjugate h^* is the closure of A^* g^* (Theorem 16.3.2). If there exists x with ⟪aᵢ, x⟫ ∈ ri (dom gᵢ) for i = 1, …, m, then the infimum is attained and h^* = A^* g^* (Theorem 16.3.3).

theorem section16_sup_dotProduct_sub_precomp_eq_sInf_fenchelConjugate_fiber {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (g : (Fin m → ℝ) → EReal) (xStar : Fin n → ℝ) (hEq : have Aadj := LinearMap.adjoint A; (fenchelConjugate n fun (x : Fin n → ℝ) => g (A (WithLp.toLp 2 x)).ofLp) = fun (xStar : Fin n → ℝ) => sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => fenchelConjugate m g yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar})) : have Aadj := LinearMap.adjoint A; sSup (Set.range fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - g (A (WithLp.toLp 2 x)).ofLp) = sInf ((fun (yStar : EuclideanSpace ℝ (Fin m)) => fenchelConjugate m g yStar.ofLp) '' {yStar : EuclideanSpace ℝ (Fin m) | Aadj yStar = WithLp.toLp 2 xStar})

Text 16.0.5: Interpreting the identity (g ∘ A)^* = A^* g^* (in the case where no closure is needed) as a sup/inf formula.

For any xStar ∈ ℝⁿ, one has

sup {⟪x, xStar⟫ - g (A x) | x ∈ ℝⁿ} = inf {g^* yStar | A^* yStar = xStar}.

theorem section16_sum_ne_bot_of_ne_bot {ι : Type u_1} (s : Finset ι) (b : ι → EReal) (hb : ∀ i ∈ s, b i ≠ ⊥) : s.sum b ≠ ⊥

A finite sum of EReal values is not ⊥ if all terms are not ⊥.

theorem section16_neg_sum_eq_sum_neg {ι : Type u_1} (s : Finset ι) (b : ι → EReal) (hb : ∀ i ∈ s, b i ≠ ⊥) : -s.sum b = ∑ i ∈ s, -b i

Negation distributes over finite sums of non-⊥ EReal values.

theorem section16_iSup_add_iSup_eq_iSup_prod {α : Type u_1} {β : Type u_2} (u : α → EReal) (v : β → EReal) : iSup u + iSup v = ⨆ (p : α × β), u p.1 + v p.2

Supremum of a sum of independent variables equals the sum of suprema.

theorem section16_iSup_fin_sum_eq_sum_iSup {n m : ℕ} (g : Fin m → (Fin n → ℝ) → EReal) : ⨆ (x' : Fin m → Fin n → ℝ), ∑ i : Fin m, g i (x' i) = ∑ i : Fin m, ⨆ (x : Fin n → ℝ), g i x

Supremum over a Fin-indexed sum equals the sum of suprema.

theorem section16_coe_finset_sum {ι : Type u_1} (s : Finset ι) (b : ι → ℝ) : ↑(s.sum b) = ∑ i ∈ s, ↑(b i)

Coercion of a real finite sum into EReal equals the finite sum of coercions.

theorem section16_coe_sum_dotProduct_eq_sum_coe_dotProduct {n m : ℕ} (x' : Fin m → Fin n → ℝ) (xStar : Fin n → ℝ) : ↑(∑ i : Fin m, x' i ⬝ᵥ xStar) = ∑ i : Fin m, ↑(x' i ⬝ᵥ xStar)

Coercion of a dot-product sum into EReal equals the sum of coerced dot products.

theorem section16_sum_dotProduct_sub_sum_eq_sum_sub {n m : ℕ} (x' : Fin m → Fin n → ℝ) (xStar : Fin n → ℝ) (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : ↑((∑ i : Fin m, x' i) ⬝ᵥ xStar) - ∑ i : Fin m, f i (x' i) = ∑ i : Fin m, (↑(x' i ⬝ᵥ xStar) - f i (x' i))

Rewrite a dot-product minus a sum as a sum of dot-product differences.

theorem section16_fenchelConjugate_infimalConvolutionFamily {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : fenchelConjugate n (infimalConvolutionFamily f) = fun (xStar : Fin n → ℝ) => ∑ i : Fin m, fenchelConjugate n (f i) xStar

Theorem 16.4.1: Let f₁, …, fₘ be proper convex functions on ℝⁿ. Then the Fenchel conjugate of their infimal convolution is the sum of their Fenchel conjugates:

(f₁ □ ⋯ □ fₘ)^* = f₁^* + ⋯ + fₘ^*.

In this development, f₁ □ ⋯ □ fₘ is infimalConvolutionFamily f, and fᵢ^* is fenchelConjugate n (f i).

theorem section16_infimalConvolutionFamily_indicatorFunction_eq_indicatorFunction_sum {n m : ℕ} (C : Fin m → Set (Fin n → ℝ)) : (infimalConvolutionFamily fun (i : Fin m) => indicatorFunction (C i)) = indicatorFunction (∑ i : Fin m, C i)

The infimal convolution of indicator functions is the indicator of the Minkowski sum.

theorem section16_deltaStar_sum {n m : ℕ} (C : Fin m → Set (Fin n → ℝ)) (hC : ∀ (i : Fin m), Convex ℝ (C i)) (hCne : ∀ (i : Fin m), (C i).Nonempty) : supportFunctionEReal (∑ i : Fin m, C i) = fun (xStar : Fin n → ℝ) => ∑ i : Fin m, supportFunctionEReal (C i) xStar

Corollary 16.4.1.1: Let C₁, …, Cₘ be non-empty convex sets in ℝⁿ. Then the support function δ^*(· | C) sends Minkowski sums to pointwise sums:

δ^*(· | C₁ + ⋯ + Cₘ) = δ^*(· | C₁) + ⋯ + δ^*(· | Cₘ).

theorem section16_convexFunctionClosure_indicatorFunction_eq_indicatorFunction_closure {n : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hCne : C.Nonempty) : convexFunctionClosure (indicatorFunction C) = indicatorFunction (closure C)

The convex-function closure of an indicator function is the indicator of the set closure.

theorem section16_sum_indicatorFunction_eq_indicatorFunction_iInter {n m : ℕ} (C : Fin m → Set (Fin n → ℝ)) : (fun (x : Fin n → ℝ) => ∑ i : Fin m, indicatorFunction (C i) x) = indicatorFunction (⋂ (i : Fin m), C i)

The sum of indicator functions is the indicator of the intersection.

theorem section16_supportFunctionEReal_iInter_closure_eq_convexFunctionClosure_infimalConvolutionFamily {n m : ℕ} (C : Fin m → Set (Fin n → ℝ)) (hC : ∀ (i : Fin m), Convex ℝ (C i)) (hCne : ∀ (i : Fin m), (C i).Nonempty) : supportFunctionEReal (⋂ (i : Fin m), closure (C i)) = convexFunctionClosure (infimalConvolutionFamily fun (i : Fin m) => supportFunctionEReal (C i))

Corollary 16.4.1.2. Let C₁, …, Cₘ be non-empty convex sets in ℝⁿ. Then the support function of the intersection of their closures is the convex-function closure of the infimal convolution of the support functions:

δ^*(· | cl C₁ ∩ ⋯ ∩ cl Cₘ) = cl (δ^*(· | C₁) ⊕ ⋯ ⊕ δ^*(· | Cₘ)).

In this development, δ^* is supportFunctionEReal, cl is convexFunctionClosure, and ⊕ is modeled by infimalConvolutionFamily.

theorem section16_fenchelConjugate_infimalConvolutionFamily_conjugates_eq_sum_closure {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : fenchelConjugate n (infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i)) = fun (xStar : Fin n → ℝ) => ∑ i : Fin m, convexFunctionClosure (f i) xStar

The conjugate of the infimal convolution of conjugates is the sum of closures.

theorem section16_convexFunction_infimalConvolutionFamily_conjugates {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : ConvexFunction (infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i))

The infimal convolution of conjugates is a convex function.

theorem section16_fenchelConjugate_sum_convexFunctionClosure_eq_convexFunctionClosure_infimalConvolutionFamily_proof_step {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : (fenchelConjugate n fun (x : Fin n → ℝ) => ∑ i : Fin m, convexFunctionClosure (f i) x) = convexFunctionClosure (infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i))

Conjugating the sum-closure identity yields the closure statement.

theorem section16_fenchelConjugate_sum_convexFunctionClosure_eq_convexFunctionClosure_infimalConvolutionFamily {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : (fenchelConjugate n fun (x : Fin n → ℝ) => ∑ i : Fin m, convexFunctionClosure (f i) x) = convexFunctionClosure (infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i))

Theorem 16.4.2: Let f₁, …, fₘ be proper convex functions on ℝⁿ. Then

(cl f₁ + ⋯ + cl fₘ)^* = cl (f₁^* □ ⋯ □ fₘ^*).

Here cl is the convex-function closure convexFunctionClosure, ^* is the Fenchel conjugate fenchelConjugate n, the sum is pointwise (written as ∑ i), and □ is the infimal convolution family infimalConvolutionFamily.

theorem section16_sum_convexFunctionClosure_eq_convexFunctionClosure_sum_of_nonempty_iInter_ri_effectiveDomain {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hri : (⋂ (i : Fin m), euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (f i))).Nonempty) : (fun (x : Fin n → ℝ) => ∑ i : Fin m, convexFunctionClosure (f i) x) = convexFunctionClosure fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x

Under a common relative-interior point, the sum of closures equals the closure of the sum.