@[reducible, inline]

noncomputable abbrev deltaStar {n : ℕ} (C : Set (Fin n → ℝ)) : (Fin n → ℝ) → ℝ

Text 13.0.1: Let C be a convex set. The support function δ^*(· | C) of C is defined by

δ^*(x^* | C) = sup { ⟪x, x^*⟫ | x ∈ C }.

Equations

• deltaStar C = supportFunction C

theorem supportFunction_eq_sSup_image_dotProduct {n : ℕ} (C : Set (Fin n → ℝ)) (x : Fin n → ℝ) : supportFunction C x = sSup ((fun (y : Fin n → ℝ) => x ⬝ᵥ y) '' C)

Rewrite supportFunction as an sSup over an image.

theorem image_dotProduct_neg_left_eq_neg_smul_image_dotProduct {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) : (fun (y : Fin n → ℝ) => -xStar ⬝ᵥ y) '' C = -1 • (fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C

The dot-product image-set at -xStar is the (-1)-scaled dot-product image-set at xStar.

theorem sSup_neg_one_smul_eq_neg_sInf (S : Set ℝ) : sSup (-1 • S) = -sInf S

Scaling a real set by -1 swaps sSup and sInf.

theorem sInf_dotProduct_eq_neg_deltaStar {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (_hC : Convex ℝ C) : sInf ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C) = -deltaStar C (-xStar)

Text 13.0.2: Let C be a convex set. Then

inf { ⟪x, x^*⟫ | x ∈ C } = -δ^*(-x^* | C),

where δ^*(· | C) is the support function of C.

theorem deltaStar_eq_sSup_image_dotProduct_right {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) : deltaStar C xStar = sSup ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C)

Rewrite deltaStar as an sSup of dotProduct x xStar over x ∈ C.

theorem forall_image_dotProduct_le_iff_subset_halfspace {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (β : ℝ) : (∀ r ∈ (fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C, r ≤ β) ↔ C ⊆ {x : Fin n → ℝ | x ⬝ᵥ xStar ≤ β}

Convert the pointwise bound on the dot-product image-set to a halfspace inclusion.

theorem csSup_image_dotProduct_le_iff {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (β : ℝ) (hCne : C.Nonempty) (hbdd : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C)) : sSup ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C) ≤ β ↔ ∀ r ∈ (fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C, r ≤ β

A csSup inequality over the dot-product image-set is equivalent to a pointwise bound.

theorem subset_halfspace_iff_ge_deltaStar {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (β : ℝ) (_hC : Convex ℝ C) (hCne : C.Nonempty) (hbdd : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C)) : C ⊆ {x : Fin n → ℝ | x ⬝ᵥ xStar ≤ β} ↔ β ≥ deltaStar C xStar

Text 13.0.3: Let C be a convex set. Then

C ⊆ { x | ⟪x, x^*⟫ ≤ β } if and only if β ≥ δ^*(x^* | C).

noncomputable def barrierCone13 {n : ℕ} (C : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Text 13.0.4: Let C ⊆ ℝ^n be a nonempty convex set. The barrier cone of C, equivalently the effective domain of the support function δ^*(· | C), is

bar C = dom (δ^*(· | C)) = {x^* | sup {⟪x, x^*⟫ | x ∈ C} < +∞ }.

Equations

• barrierCone13 C = effectiveDomain Set.univ fun (xStar : Fin n → ℝ) => sSup {z : EReal | ∃ x ∈ C, z = ↑(x ⬝ᵥ xStar)}

theorem deltaStar_eq_deltaStar_closure {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) : deltaStar C xStar = deltaStar (closure C) xStar

The support function is unchanged by taking the (topological) closure of the set.

theorem closure_intrinsicInterior_eq_closure_of_convex {n : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) : closure (intrinsicInterior ℝ C) = closure C

For a convex set, the closure of its intrinsic (relative) interior equals its closure.

theorem deltaStar_eq_closure_eq_intrinsicInterior {n : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (xStar : Fin n → ℝ) : deltaStar C xStar = deltaStar (closure C) xStar ∧ deltaStar (closure C) xStar = deltaStar (intrinsicInterior ℝ C) xStar

Text 13.0.5: For any convex set C, one has

δ^*(x^* | C) = δ^*(x^* | cl C) = δ^*(x^* | ri C) for all x^*, where cl denotes closure and ri denotes relative (intrinsic) interior.

theorem section13_dotProduct_le_deltaStar_of_mem {n : ℕ} {C : Set (Fin n → ℝ)} {xStar y : Fin n → ℝ} (hbdd : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C)) (hy : y ∈ C) : y ⬝ᵥ xStar ≤ deltaStar C xStar

If the dot-product image is bounded above, any member of C satisfies the supporting inequality.

theorem section13_bddBelow_image_dotProduct_of_bddAbove_image_dotProduct_neg {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (hbdd : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ -xStar) '' C)) : BddBelow ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C)

A bound on the dot-product image at -xStar gives a lower bound on the dot-product image at xStar.

theorem section13_isMaxOn_dotProduct_iff_eq_deltaStar_of_mem {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (xStar x : Fin n → ℝ) (hxC : x ∈ C) (hbdd : BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C)) : IsMaxOn (fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) C x ↔ x ⬝ᵥ xStar = deltaStar C xStar

For a point x ∈ C, being a maximizer of dotProduct · xStar is equivalent to equality with deltaStar.

theorem section13_exists_lt_dotProduct_of_ne_neg_deltaStar {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) (x xStar : Fin n → ℝ) (hxC : x ∈ C) (hxEq : x ⬝ᵥ xStar = deltaStar C xStar) (hne : -deltaStar C (-xStar) ≠ deltaStar C xStar) (hbdd : BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C)) : ∃ y ∈ C, y ⬝ᵥ xStar < x ⬝ᵥ xStar

If -deltaStar (-xStar) ≠ deltaStar xStar, then a maximizer of dotProduct · xStar is not a minimizer.

theorem mem_closure_iff_forall_dotProduct_le_deltaStar {n : ℕ} (C : Set (Fin n → ℝ)) (x : Fin n → ℝ) (hC : Convex ℝ C) (hCne : C.Nonempty) (hCbd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C)) : x ∈ closure C ↔ ∀ (xStar : Fin n → ℝ), x ⬝ᵥ xStar ≤ deltaStar C xStar

Theorem 13.1: Let C be a convex set. Then x ∈ cl C if and only if ⟪x, x^*⟫ ≤ δ^*(x^* | C) for every x^*. Moreover, x ∈ ri C if and only if the same condition holds, but with strict inequality for each x^* such that -δ^*(-x^* | C) ≠ δ^*(x^* | C). One has x ∈ int C if and only if ⟪x, x^*⟫ < δ^*(x^* | C) for every x^*.

theorem mem_intrinsicInterior_iff_forall_dotProduct_le_deltaStar_and_forall_of_ne {n : ℕ} (C : Set (Fin n → ℝ)) (x : Fin n → ℝ) (hC : Convex ℝ C) (hCne : C.Nonempty) (hCbd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C)) : x ∈ intrinsicInterior ℝ C ↔ x ∈ C ∧ (∀ (xStar : Fin n → ℝ), x ⬝ᵥ xStar ≤ deltaStar C xStar) ∧ ∀ (xStar : Fin n → ℝ), -deltaStar C (-xStar) ≠ deltaStar C xStar → x ⬝ᵥ xStar < deltaStar C xStar

Theorem 13.1 (relative interior characterization): for convex C, membership in the relative (intrinsic) interior is equivalent to the supporting-inequality condition, with strict inequality for each x^* such that -δ^*(-x^* | C) ≠ δ^*(x^* | C).

theorem mem_interior_iff_forall_dotProduct_lt_deltaStar {n : ℕ} (C : Set (Fin n → ℝ)) (x : Fin n → ℝ) (hC : Convex ℝ C) (hCbd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C)) : x ∈ interior C ↔ x ∈ C ∧ ∀ (xStar : Fin n → ℝ), xStar ≠ 0 → x ⬝ᵥ xStar < deltaStar C xStar

Theorem 13.1 (interior characterization): for convex C, membership in the (topological) interior is equivalent to strict supporting inequalities ⟪x, x^*⟫ < δ^*(x^* | C) for all x^*.

theorem section13_bddAbove_image_dotProduct_closure {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (hbdd : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C)) : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' closure C)

If the dot-product image of C is bounded above, then so is the dot-product image of closure C.

theorem section13_deltaStar_le_of_subset {n : ℕ} {C₁ C₂ : Set (Fin n → ℝ)} (xStar : Fin n → ℝ) (hsub : C₁ ⊆ C₂) (hC₁ne : C₁.Nonempty) (hC₂bd : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₂)) : deltaStar C₁ xStar ≤ deltaStar C₂ xStar

Monotonicity of deltaStar under set inclusion (assuming nonempty domain and bounded range).

theorem closure_subset_iff_deltaStar_le {n : ℕ} (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ : Convex ℝ C₁) (hC₂ : Convex ℝ C₂) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hC₁bd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C₁)) (hC₂bd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C₂)) : closure C₁ ⊆ closure C₂ ↔ deltaStar C₁ ≤ deltaStar C₂

Corollary 13.1.1. For convex sets C₁ and C₂ in ℝ^n, one has cl C₁ ⊆ cl C₂ if and only if δ^*(· | C₁) ≤ δ^*(· | C₂).

theorem section13_setOf_forall_dotProduct_le_deltaStar_eq_closure {n : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hCne : C.Nonempty) (hCbd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C)) : {x : Fin n → ℝ | ∀ (xStar : Fin n → ℝ), x ⬝ᵥ xStar ≤ deltaStar C xStar} = closure C

For a convex set C with well-defined support function, the set of points satisfying all supporting inequalities is the closure of C.

theorem setOf_forall_dotProduct_le_deltaStar_eq_of_isClosed {n : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hCclosed : IsClosed C) (hCne : C.Nonempty) (hCbd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C)) : {x : Fin n → ℝ | ∀ (xStar : Fin n → ℝ), x ⬝ᵥ xStar ≤ deltaStar C xStar} = C

Text 13.1.2: Let C ⊆ ℝ^n be a closed convex set. Define

D := { x | ∀ x^*, ⟪x, x^*⟫ ≤ δ^*(x^* | C) }.

Then D = C. In particular, C is completely determined by its support function.

theorem eq_of_isClosed_of_convex_of_deltaStar_eq {n : ℕ} {C₁ C₂ : Set (Fin n → ℝ)} (hC₁ : Convex ℝ C₁) (hC₂ : Convex ℝ C₂) (hC₁closed : IsClosed C₁) (hC₂closed : IsClosed C₂) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hC₁bd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C₁)) (hC₂bd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (y : Fin n → ℝ) => y ⬝ᵥ xStar) '' C₂)) (hδ : deltaStar C₁ = deltaStar C₂) : C₁ = C₂

Text 13.1.2 (support function determines a closed convex set): if two closed convex sets have the same (finite) support function, then they are equal.

theorem section13_image_dotProduct_add_eq {n : ℕ} (C₁ C₂ : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) : (fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' (C₁ + C₂) = (fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₁ + (fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₂

The dot-product image of a Minkowski sum is the pointwise sum of the dot-product images.

theorem section13_sSup_image_dotProduct_add {n : ℕ} (C₁ C₂ : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hbdd₁ : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₁)) (hbdd₂ : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₂)) : sSup ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₁ + (fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₂) = sSup ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₁) + sSup ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₂)

If both dot-product image-sets are bounded above, then the supremum over their sum splits.

theorem section13_deltaStar_add_of_bddAbove {n : ℕ} (C₁ C₂ : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hbdd₁ : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₁)) (hbdd₂ : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₂)) : deltaStar (C₁ + C₂) xStar = deltaStar C₁ xStar + deltaStar C₂ xStar

Boundedness in direction xStar makes the Real-valued support function additive under sums.

theorem deltaStar_add {n : ℕ} (C₁ C₂ : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (_hC₁ : Convex ℝ C₁) (_hC₂ : Convex ℝ C₂) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hbdd₁ : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₁)) (hbdd₂ : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C₂)) : deltaStar (C₁ + C₂) xStar = deltaStar C₁ xStar + deltaStar C₂ xStar

Text 13.1.3: The support function of the sum of two non-empty convex sets C₁ and C₂ is given by

δ^*(x^* | C₁ + C₂) = δ^*(x^* | C₁) + δ^*(x^* | C₂).

theorem section13_fenchelConjugate_indicatorFunction_eq_sSup_image_dotProduct {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) : fenchelConjugate n (indicatorFunction C) xStar = sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar)) '' C)

For indicator functions, points outside the set contribute ⊥ to the Fenchel conjugate.

theorem section13_sSup_image_coe_real_eq_coe_sSup (S : Set ℝ) (hne : S.Nonempty) (hbdd : BddAbove S) : sSup ((fun (r : ℝ) => ↑r) '' S) = ↑(sSup S)

Coercion commutes with sSup for a nonempty, bounded-above set of reals.

theorem fenchelConjugate_indicatorFunction_eq_deltaStar {n : ℕ} (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (hCne : C.Nonempty) (hbdd : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C)) : fenchelConjugate n (indicatorFunction C) xStar = ↑(deltaStar C xStar)

Text 13.1.4: Let C ⊆ ℝ^n be a convex set, and let δ(· | C) be its indicator function, δ(x | C) = 0 for x ∈ C and δ(x | C) = +∞ for x ∉ C.

Then the convex conjugate of δ(· | C) is the support function of C. More precisely, for every xStar,

δ*(xStar | C) = sup_x (⟪x, xStar⟫ - δ(x | C)) = sup_{x ∈ C} ⟪x, xStar⟫.

theorem section13_fenchelConjugate_indicatorFunction_eq_deltaStar_fun {n : ℕ} (C : Set (Fin n → ℝ)) (hCne : C.Nonempty) (hCbd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C)) : fenchelConjugate n (indicatorFunction C) = fun (xStar : Fin n → ℝ) => ↑(deltaStar C xStar)

Under directional boundedness, the Fenchel conjugate of the indicator function equals the Real-valued support function (coerced to EReal).

theorem section13_affine_le_indicatorFunction_le_zero_on_closure {n : ℕ} {C : Set (Fin n → ℝ)} (h : (Fin n → ℝ) →ᵃ[ℝ] ℝ) (hh : ∀ (y : Fin n → ℝ), ↑(h y) ≤ indicatorFunction C y) (x : Fin n → ℝ) : x ∈ closure C → h x ≤ 0

If x ∈ closure C, then any affine map majorized by indicatorFunction C is nonpositive at x.