Convex bifunctions and generalized convex programs

A bifunction F : U → X → EReal is a family of minimisation problems indexed by a perturbation parameter u. The generalized convex program (P) associated with F is "minimise F 0 over X, with the perturbations F u on offer"; its perturbation function is inf F : u ↦ ⨅ x, F u x, and its Kuhn–Tucker vectors are the prices at which no perturbation is worth buying.

Everything rests on one identification: inf F is a partial minimisation of the graph function, hence convex, and v is a Kuhn–Tucker vector exactly when -v ∈ ∂(inf F)(0). The Kuhn–Tucker set is a reflected subdifferential, so the whole subgradient theory transfers wholesale: existence under strong consistency, compactness under strict consistency, the directional-derivative formulas, the polyhedral case.

Main definitions

• Bifun U X — a bifunction; graphFn F is the same data on U × X, ConvexBifun F and PolyhedralBifun F are convexity and polyhedrality of it.
• infBifun F, domBifun F — the perturbation function and the effective domain {u | F u ≢ ⊤}.
• KuhnTucker B F — the v for which ⨅ u (⟨u, v⟩ + inf F u) is finite and equal to inf F 0.
• Consistent, StronglyConsistent, StrictlyConsistent — 0 ∈ dom F, 0 ∈ ri (dom F), 0 ∈ int (dom F).

Main results

• convexFn_infBifun, dom_infBifun, mem_kuhnTucker_iff_neg_mem_subgradient — inf F is convex with effective domain dom F, and ∂(inf F)(0) is the reflected Kuhn–Tucker set (Theorem 29.1 in [^1]).
• kuhnTucker_eq_neg_subgradient, convex_kuhnTucker, isClosed_kuhnTucker, supportFn_kuhnTucker — the Kuhn–Tucker set is closed convex with a computable support function; kuhnTucker_eq_empty_iff — when it is empty; kuhnTucker_eq_singleton_of_hasGradientAt — when it is one vector; kuhnTucker_nonempty_of_stronglyConsistent, dirDeriv_infBifun_eq — existence and the directional-derivative formula.
• isCompact_kuhnTucker_of_strictlyConsistent, continuousOn_infBifun_interior — what strict consistency buys; infBifun_eq_bot_of_mem_relint — an improper inf F is -∞ on ri (dom F).
• PolyhedralBifun.polyhedralFn_infBifun, kuhnTucker_nonempty_of_polyhedralBifun, argmin_nonempty_of_polyhedralBifun and companions — the polyhedral case (Theorem 29.2 in [^1]).

Implementation notes

KuhnTucker is the book's own definition, not the subdifferential characterisation: the inequality form inf F 0 ≤ ⟨u, v⟩ + inf F u is a consequence, and defining KuhnTucker by it would have made that characterisation an Iff.rfl. The boundedness clause under strict consistency is finite-dimensional in V: pairing-boundedness is all a general dual pair supports, and a norm bound needs a coordinate estimate against a finite basis.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §29.

Bifunctions and the perturbation function

@[reducible, inline]

abbrev Tdaf.ConvexAnalysis.Bifun (U : Type u_3) (X : Type u_4) : Type (max u_3 u_4)

A bifunction from U to X: a family of EReal-valued functions on X indexed by a perturbation parameter in U. The program (P) is identified with F itself.

Equations

• Tdaf.ConvexAnalysis.Bifun U X = (U → X → EReal)

def Tdaf.ConvexAnalysis.graphFn {U : Type u_1} {X : Type u_2} (F : Bifun U X) : U × X → EReal

The graph function of a bifunction: the same data as a function on U × X. Every convexity statement about F is one about graphFn F.

Equations

• Tdaf.ConvexAnalysis.graphFn F p = F p.1 p.2

@[simp]

theorem Tdaf.ConvexAnalysis.graphFn_apply {U : Type u_1} {X : Type u_2} (F : Bifun U X) (u : U) (x : X) : graphFn F (u, x) = F u x

noncomputable def Tdaf.ConvexAnalysis.inverseBifun {U : Type u_1} {X : Type u_2} (F : Bifun U X) : Bifun X U

The inverse F_* of a bifunction: (F_* x) u = -(F u)(x). Unlike flipBifun it also changes the sign, so it carries convex bifunctions to concave ones and back; it is involutory, and composition of bifunctions is built on it. The sign flip is what makes (Ff)(x) = ⨅ (f - F_* x) agree with ⨅ u, f u + (F u)(x).

Equations

• Tdaf.ConvexAnalysis.inverseBifun F x u = -F u x

@[simp]

theorem Tdaf.ConvexAnalysis.inverseBifun_apply {U : Type u_1} {X : Type u_2} (F : Bifun U X) (x : X) (u : U) : inverseBifun F x u = -F u x

@[simp]

theorem Tdaf.ConvexAnalysis.inverseBifun_inverseBifun {U : Type u_1} {X : Type u_2} (F : Bifun U X) : inverseBifun (inverseBifun F) = F

The inverse operation is involutory: (F_*)_* = F.

theorem Tdaf.ConvexAnalysis.graphFn_inverseBifun {U : Type u_1} {X : Type u_2} (F : Bifun U X) (q : X × U) : graphFn (inverseBifun F) q = -graphFn F (q.2, q.1)

noncomputable def Tdaf.ConvexAnalysis.infBifun {U : Type u_1} {X : Type u_2} (F : Bifun U X) : U → EReal

The perturbation function inf F; its value at 0 is the optimal value of (P).

Equations

• Tdaf.ConvexAnalysis.infBifun F u = ⨅ (x : X), F u x

theorem Tdaf.ConvexAnalysis.infBifun_apply {U : Type u_1} {X : Type u_2} (F : Bifun U X) (u : U) : infBifun F u = ⨅ (x : X), F u x

def Tdaf.ConvexAnalysis.domBifun {U : Type u_1} {X : Type u_2} (F : Bifun U X) : Set U

The effective domain of a bifunction: the perturbations for which F u is not identically ⊤.

Equations

• Tdaf.ConvexAnalysis.domBifun F = {u : U | ∃ (x : X), F u x ≠ ⊤}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_domBifun {U : Type u_1} {X : Type u_2} {F : Bifun U X} {u : U} : u ∈ domBifun F ↔ ∃ (x : X), F u x ≠ ⊤

theorem Tdaf.ConvexAnalysis.dom_infBifun {U : Type u_1} {X : Type u_2} (F : Bifun U X) : dom (infBifun F) = domBifun F

The effective domain of the perturbation function is the effective domain of F.

Convexity

def Tdaf.ConvexAnalysis.ConvexBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] (F : Bifun U X) : Prop

A bifunction is convex when its graph function is a convex function on U × X.

Equations

• Tdaf.ConvexAnalysis.ConvexBifun F = Tdaf.ConvexAnalysis.ConvexFn (Tdaf.ConvexAnalysis.graphFn F)

theorem Tdaf.ConvexAnalysis.convexBifun_iff {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} : ConvexBifun F ↔ ConvexFn (graphFn F)

theorem Tdaf.ConvexAnalysis.convexFn_infBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hF : ConvexBifun F) : ConvexFn (infBifun F)

The perturbation function of a convex bifunction is convex: a partial minimisation of the jointly convex graph function along the projection (u, x) ↦ u.

theorem Tdaf.ConvexAnalysis.ConvexBifun.convexFn_apply {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (u : U) : ConvexFn (F u)

Each image F u of a convex bifunction is a convex function: a slice of a jointly convex function, since a * u + b * u = u when a + b = 1.

theorem Tdaf.ConvexAnalysis.convex_domBifun {U : Type u_1} {X : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hF : ConvexBifun F) : Convex ℝ (domBifun F)

The effective domain of a convex bifunction is convex — it is dom (inf F).

Consistency

def Tdaf.ConvexAnalysis.Consistent {U : Type u_1} {X : Type u_2} [AddCommGroup U] (F : Bifun U X) : Prop

(P) is consistent when it has a feasible solution, i.e. when its optimal value is < ⊤.

Equations

• Tdaf.ConvexAnalysis.Consistent F = (0 ∈ Tdaf.ConvexAnalysis.domBifun F)

theorem Tdaf.ConvexAnalysis.consistent_iff {U : Type u_1} {X : Type u_2} [AddCommGroup U] {F : Bifun U X} : Consistent F ↔ ∃ (x : X), F 0 x ≠ ⊤

def Tdaf.ConvexAnalysis.StronglyConsistent {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] (F : Bifun U X) : Prop

(P) is strongly consistent when 0 is a relative interior point of dom F: the qualification behind the existence of Kuhn–Tucker vectors.

Equations

• Tdaf.ConvexAnalysis.StronglyConsistent F = (0 ∈ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.domBifun F))

def Tdaf.ConvexAnalysis.StrictlyConsistent {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] (F : Bifun U X) : Prop

(P) is strictly consistent when 0 is an interior point of dom F.

Equations

• Tdaf.ConvexAnalysis.StrictlyConsistent F = (0 ∈ interior (Tdaf.ConvexAnalysis.domBifun F))

theorem Tdaf.ConvexAnalysis.StrictlyConsistent.stronglyConsistent {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {F : Bifun U X} (h : StrictlyConsistent F) : StronglyConsistent F

theorem Tdaf.ConvexAnalysis.StronglyConsistent.consistent {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] {F : Bifun U X} (h : StronglyConsistent F) : Consistent F

Kuhn–Tucker vectors

def Tdaf.ConvexAnalysis.KuhnTucker {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (F : Bifun U X) : Set V

Kuhn–Tucker vectors for the program associated with F: the prices v at which ⨅ u (⟨u, v⟩ + inf F u) is finite and equal to the optimal value inf F 0.

Equations

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

theorem Tdaf.ConvexAnalysis.iInf_add_infBifun_le {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (F : Bifun U X) (v : V) : ⨅ (u : U), ↑((B u) v) + infBifun F u ≤ infBifun F 0

Evaluating at u = 0: the infimum defining a Kuhn–Tucker vector never exceeds inf F 0.

theorem Tdaf.ConvexAnalysis.mem_kuhnTucker_iff_forall_le {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} {v : V} : v ∈ KuhnTucker B F ↔ infBifun F 0 ≠ ⊤ ∧ infBifun F 0 ≠ ⊥ ∧ ∀ (u : U), infBifun F 0 ≤ ↑((B u) v) + infBifun F u

A Kuhn–Tucker vector is a price at which every perturbation costs at least what it saves.

theorem Tdaf.ConvexAnalysis.mem_kuhnTucker_iff_neg_mem_subgradient {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} {v : V} (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : v ∈ KuhnTucker B F ↔ -v ∈ subgradient B (infBifun F) 0

When the optimal value is finite, the Kuhn–Tucker vectors are exactly the v with -v ∈ ∂(inf F)(0). The subgradient inequality at 0 in the direction -v says precisely that no perturbation is worth buying at the price v.

theorem Tdaf.ConvexAnalysis.kuhnTucker_eq_neg_subgradient {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : KuhnTucker B F = -subgradient B (infBifun F) 0

The same as an equation between sets: the Kuhn–Tucker set is the reflected subdifferential of the perturbation function at the origin.

theorem Tdaf.ConvexAnalysis.convex_kuhnTucker {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : Convex ℝ (KuhnTucker B F)

The Kuhn–Tucker vectors form a convex set.

Closedness and existence

theorem Tdaf.ConvexAnalysis.isClosed_kuhnTucker {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} [IsContinuousPairing B.flip] (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : IsClosed (KuhnTucker B F)

The Kuhn–Tucker vectors form a closed set.

theorem Tdaf.ConvexAnalysis.kuhnTucker_nonempty_of_stronglyConsistent {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [AddCommGroup X] [Module ℝ X] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} [IsCompatiblePairing B] (hF : ConvexBifun F) (hp : Proper (infBifun F)) (hs : StronglyConsistent F) (ht : infBifun F 0 ≠ ⊤) : (KuhnTucker B F).Nonempty

A strongly consistent convex program whose perturbation function is proper has a Kuhn–Tucker vector: inf F is subdifferentiable at the origin, a relative-interior point of its domain.

The directional derivative of the perturbation function

theorem Tdaf.ConvexAnalysis.supportFn_neg_set {U : Type u_1} {V : Type u_2} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (s : Set U) (v : V) : supportFn B (-s) v = supportFn B s (-v)

The support function of a reflected set is the support function read at the reflected point.

theorem Tdaf.ConvexAnalysis.posHomogeneous_dirDeriv_infBifun {U : Type u_1} {X : Type u_3} [AddCommGroup U] [Module ℝ U] (F : Bifun U X) : PosHomogeneous (dirDeriv (infBifun F) 0)

(inf F)'(0; ·) is positively homogeneous, for every bifunction.

theorem Tdaf.ConvexAnalysis.convexFn_dirDeriv_infBifun {U : Type u_1} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : ConvexFn (dirDeriv (infBifun F) 0)

(inf F)'(0; ·) is convex in the direction when inf F 0 is finite.

theorem Tdaf.ConvexAnalysis.supportFn_kuhnTucker {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {F : Bifun U X} (hF : ConvexBifun F) (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) (u : U) : supportFn B.flip (KuhnTucker B F) u = clFn (dirDeriv (infBifun F) 0) (-u)

The support function of the Kuhn–Tucker set is the closure of u ↦ (inf F)'(0; -u): the support function of a subdifferential, composed with the reflection.

The improper and the empty case

theorem Tdaf.ConvexAnalysis.infBifun_eq_top_of_notMem_domBifun {U : Type u_1} {X : Type u_3} {F : Bifun U X} {u : U} (hu : u ∉ domBifun F) : infBifun F u = ⊤

Off dom F the optimal value is +∞.

theorem Tdaf.ConvexAnalysis.infBifun_eq_bot_of_mem_relint {U : Type u_1} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (h : ∃ (u : U), infBifun F u = ⊥) {u : U} (hu : u ∈ intrinsicInterior ℝ (domBifun F)) : infBifun F u = ⊥

If some perturbation drives the optimal value to -∞, so does every perturbation in ri (dom F): an improper convex function is -∞ throughout the relative interior of its domain.

theorem Tdaf.ConvexAnalysis.kuhnTucker_eq_empty_iff {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {F : Bifun U X} (hF : ConvexBifun F) (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : KuhnTucker B F = ∅ ↔ ∃ (u : U), dirDeriv (infBifun F) 0 u = ⊥ ∧ dirDeriv (infBifun F) 0 (-u) = ⊤

A convex program with a finite optimal value has no Kuhn–Tucker vector exactly when some direction of perturbation makes the two-sided directional derivative -∞, (inf F)'(0; u) = -(inf F)'(0; -u) = -∞. Forwards: an empty subdifferential makes cl (inf F)'(0; ·) the constant -∞, and the closure of a proper convex function is proper.

What consistency and differentiability buy

theorem Tdaf.ConvexAnalysis.proper_infBifun_of_stronglyConsistent {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (hs : StronglyConsistent F) (hb : infBifun F 0 ≠ ⊥) : Proper (infBifun F)

A strongly consistent convex program whose optimal value is > -∞ has a proper perturbation function: an improper inf F would be -∞ throughout ri (dom F).

theorem Tdaf.ConvexAnalysis.continuousOn_infBifun_interior {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hF : ConvexBifun F) (hp : Proper (infBifun F)) : ContinuousOn (infBifun F) (interior (domBifun F))

Under strict consistency the optimal value is finite and continuous on int (dom F), a neighbourhood of the origin.

theorem Tdaf.ConvexAnalysis.infBifun_ne_top_of_mem_domBifun {U : Type u_1} {X : Type u_2} {F : Bifun U X} {u : U} (hu : u ∈ domBifun F) : infBifun F u ≠ ⊤

The optimal value is finite at every point of dom F.

theorem Tdaf.ConvexAnalysis.dirDeriv_infBifun_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {F : Bifun U X} (hF : ConvexBifun F) (hp : Proper (infBifun F)) (hs : StronglyConsistent F) (u : U) : dirDeriv (infBifun F) 0 u = supportFn B.flip (KuhnTucker B F) (-u)

The derivative formula: for a strongly consistent program with a proper perturbation function, (inf F)'(0; u) = δ*(-u | U*), the support function of the Kuhn–Tucker set read at the reflected direction.

theorem Tdaf.ConvexAnalysis.bddAbove_kuhnTucker_of_strictlyConsistent {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {F : Bifun U X} (hF : ConvexBifun F) (hp : Proper (infBifun F)) (hs : StrictlyConsistent F) (u : U) : ∃ (c : ℝ), ∀ v ∈ KuhnTucker B F, (B u) v ≤ c

Under strict consistency the Kuhn–Tucker set is bounded in the pairing sense: every ⟨u, ·⟩ is bounded above on it.

theorem Tdaf.ConvexAnalysis.isBounded_kuhnTucker_of_strictlyConsistent {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [AddCommGroup X] [Module ℝ X] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] {F : Bifun U X} (hF : ConvexBifun F) (hp : Proper (infBifun F)) (hs : StrictlyConsistent F) : Bornology.IsBounded (KuhnTucker B F)

Under strict consistency the Kuhn–Tucker set is bounded in the norm. The upgrade from pairing-boundedness is finite-dimensional.

theorem Tdaf.ConvexAnalysis.isCompact_kuhnTucker_of_strictlyConsistent {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [AddCommGroup X] [Module ℝ X] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] {F : Bifun U X} (hF : ConvexBifun F) (hp : Proper (infBifun F)) (hs : StrictlyConsistent F) (ht : infBifun F 0 ≠ ⊤) : IsCompact (KuhnTucker B F)

Under strict consistency the Kuhn–Tucker set is compact — closed and bounded, hence compact by Heine–Borel. With nonemptiness and convexity this is the book's "non-empty closed bounded convex set".

theorem Tdaf.ConvexAnalysis.kuhnTucker_nonempty_of_strictlyConsistent {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [AddCommGroup X] [Module ℝ X] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {F : Bifun U X} (hF : ConvexBifun F) (hp : Proper (infBifun F)) (hs : StrictlyConsistent F) (ht : infBifun F 0 ≠ ⊤) : (KuhnTucker B F).Nonempty

A strictly consistent program is strongly consistent, so it has a Kuhn–Tucker vector.

theorem Tdaf.ConvexAnalysis.kuhnTucker_eq_singleton_of_dirDeriv_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} (hsep : Function.Injective ⇑B.flip) (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) {v₀ : V} (h : ∀ (u : U), dirDeriv (infBifun F) 0 u = ↑((B u) (-v₀))) : KuhnTucker B F = {v₀}

Algebraic form: if (inf F)'(0; ·) is the linear function ⟨·, -v₀⟩ then v₀ is the unique Kuhn–Tucker vector.

theorem Tdaf.ConvexAnalysis.kuhnTucker_eq_singleton_of_hasGradientAt {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hF : ConvexBifun F) {f' : StrongDual ℝ U} (h : HasGradientAt (infBifun F) f' 0) (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : KuhnTucker (topDualPairing ℝ U).flip F = {-f'}

Fréchet form: where the perturbation function is differentiable, the program has exactly one Kuhn–Tucker vector, namely -∇(inf F)(0).

Polyhedral convex programs

theorem Tdaf.ConvexAnalysis.PolyhedralFn.clFn_eq_of_mem_dom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : PolyhedralFn f) {x : E} (hx : x ∈ dom f) : clFn f x = f x

A polyhedral convex function agrees with its closure throughout its effective domain: if proper it is closed, and otherwise both are -∞ there.

def Tdaf.ConvexAnalysis.PolyhedralBifun {U : Type u_1} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] (F : Bifun U X) : Prop

A convex bifunction is polyhedral when its graph function is; the associated program is then a polyhedral convex program.

Equations

• Tdaf.ConvexAnalysis.PolyhedralBifun F = Tdaf.ConvexAnalysis.PolyhedralFn (Tdaf.ConvexAnalysis.graphFn F)

theorem Tdaf.ConvexAnalysis.polyhedralBifun_iff {U : Type u_1} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {F : Bifun U X} : PolyhedralBifun F ↔ PolyhedralFn (graphFn F)

theorem Tdaf.ConvexAnalysis.PolyhedralBifun.convexBifun {U : Type u_1} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {F : Bifun U X} (hF : PolyhedralBifun F) : ConvexBifun F

theorem Tdaf.ConvexAnalysis.PolyhedralBifun.polyhedralFn_apply {U : Type u_1} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] {F : Bifun U X} (hF : PolyhedralBifun F) (u : U) : PolyhedralFn (F u)

Every image F u of a polyhedral convex bifunction — the objective F 0 in particular — is a polyhedral convex function.

theorem Tdaf.ConvexAnalysis.PolyhedralBifun.polyhedralFn_infBifun {U : Type u_1} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : PolyhedralBifun F) : PolyhedralFn (infBifun F)

The perturbation function of a polyhedral convex program is polyhedral: a partial minimisation of a polyhedral function along the projection (u, x) ↦ u.

theorem Tdaf.ConvexAnalysis.kuhnTucker_nonempty_of_polyhedralBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} [IsCompatiblePairing B] (hF : PolyhedralBifun F) (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : (KuhnTucker B F).Nonempty

A polyhedral convex program with a finite optimal value has a Kuhn–Tucker vector: a polyhedral convex function is subdifferentiable throughout its effective domain.

theorem Tdaf.ConvexAnalysis.polyhedral_kuhnTucker_of_polyhedralBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {B : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} (hF : PolyhedralBifun F) (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : Polyhedral (KuhnTucker B F)

The Kuhn–Tucker vectors of a polyhedral convex program with a finite optimal value form a polyhedral convex set.

theorem Tdaf.ConvexAnalysis.argmin_nonempty_of_polyhedralBifun {U : Type u_1} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : PolyhedralBifun F) (hb : infBifun F 0 ≠ ⊥) : (argmin (F 0)).Nonempty

A polyhedral convex program whose optimal value is not -∞ has an optimal solution. The book assumes the optimal value finite; only inf F 0 ≠ -∞ is used here, an optimal value of +∞ meaning every point is optimal. Finiteness is what the polyhedrality of the minimum set below needs.

theorem Tdaf.ConvexAnalysis.polyhedral_argmin_of_polyhedralBifun {U : Type u_1} {X : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : PolyhedralBifun F) (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : Polyhedral (argmin (F 0))

The optimal solutions of a polyhedral convex program with a finite optimal value form a polyhedral convex set — a sublevel set of F 0 at the optimal value.