Rockafellar, §28: Ordinary Convex Programs and Lagrange Multipliers

The ordinary convex program (P), its Kuhn–Tucker coefficients, its Lagrangian L, and the equivalence between solving (P) and finding a saddle-point of L.

All nine numbered results of §28 are formalized: Theorems 28.1, 28.2, 28.3 and 28.4 and Corollaries 28.1.1, 28.2.1, 28.2.2, 28.3.1 and 28.4.1, together with the three Kuhn–Tucker conditions (a), (b), (c) of Theorem 28.3, the decomposition principle, and the section's two counterexamples ex1 and ex2.

Implementation notes

A program is the tuple, not the objective function. OrdinaryConvexProgram n m carries Rockafellar's (m + 3)-tuple (C, f₀, f₁, …, f_m, r) and his two blanket assumptions on it, because two programs with the same objective f₀ + δ(· | C₀) can have different Kuhn–Tucker coefficients. eq_of_programLagrangian_eq recovers the whole tuple from the Lagrangian alone.

r counts the inequality constraints, not the equalities: f₁ ≤ 0, …, f_r ≤ 0 and f_{r+1} = 0, …, f_m = 0.

lagrangeFn u is Rockafellar's h = f₀ + λ₁f₁ + ⋯ + λ_m f_m, which is not the Lagrangian: that is programLagrangian, and saddleFn is the same function read on ℝᵐ × ℝⁿ, the shape IsSaddlePoint, maximin and minimax take. activeIndices u is {i | λᵢ ≠ 0}, the book's "(Omit terms with λᵢ = 0.)" — an omission that is not cosmetic, since ∂fᵢ(x̄) can be empty at a boundary point of dom fᵢ and 0 · ∅ = ∅ ≠ {0}.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §28 (pp. 273–290). Corollaries 28.2.2, 28.3.1 and 28.4.1 are stated there with no printed proof.

The ordinary convex program

structure Rockafellar.OrdinaryConvexProgram (n m : ℕ) : Type

Rockafellar's ordinary convex program (§28): the (m + 3)-tuple (C, f₀, f₁, …, f_m, r).

• C : Set (TdafSurface.Rn n)

  The non-empty convex set C over which the objective is minimised.

• f₀ : TdafSurface.Rn n → EReal

  The objective f₀, a proper convex function with dom f₀ = C.

• f : Fin m → TdafSurface.Rn n → EReal

  The constraint functions f₁, …, f_m.

• r : ℕ

  The number of inequality constraints: f₁ ≤ 0, …, f_r ≤ 0 and f_{r+1} = 0, …, f_m = 0.

• r_le : self.r ≤ m

  0 ≤ r ≤ m.

• convexFn_f₀ : Tdaf.ConvexAnalysis.ConvexFn self.f₀

  f₀ is convex.

• proper_f₀ : Tdaf.ConvexAnalysis.Proper self.f₀

  f₀ is proper.

• dom_f₀ : Tdaf.ConvexAnalysis.dom self.f₀ = self.C

  Rockafellar's extension convention (a): dom f₀ = C.

• convexFn_f (i : Fin m) : ↑i < self.r → Tdaf.ConvexAnalysis.ConvexFn (self.f i)

  The inequality constraints are convex.

• proper_f (i : Fin m) : ↑i < self.r → Tdaf.ConvexAnalysis.Proper (self.f i)

  The inequality constraints are proper.

• subset_dom_f (i : Fin m) : ↑i < self.r → self.C ⊆ Tdaf.ConvexAnalysis.dom (self.f i)

  Rockafellar's extension convention (b), first half: dom fᵢ ⊇ C.

• relint_subset (i : Fin m) : ↑i < self.r → intrinsicInterior ℝ self.C ⊆ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.dom (self.f i))

  Rockafellar's extension convention (b), second half: ri (dom fᵢ) ⊇ ri C.

• exists_affine (i : Fin m) : self.r ≤ ↑i → ∃ (a : TdafSurface.Rn n →ᵃ[ℝ] ℝ), ∀ (x : TdafSurface.Rn n), self.f i x = ↑(a x)

  Rockafellar's extension convention (c): the equality constraints are affine on all of ℝⁿ.

theorem Rockafellar.OrdinaryConvexProgram.convex_C {m n : ℕ} (P : OrdinaryConvexProgram n m) : Convex ℝ P.C

C is convex: it is the effective domain of a convex function.

theorem Rockafellar.OrdinaryConvexProgram.nonempty_C {m n : ℕ} (P : OrdinaryConvexProgram n m) : P.C.Nonempty

C is non-empty: it is the effective domain of a proper function.

theorem Rockafellar.OrdinaryConvexProgram.relint_C_nonempty {m n : ℕ} (P : OrdinaryConvexProgram n m) : (intrinsicInterior ℝ P.C).Nonempty

A non-empty convex set in ℝⁿ has a non-empty relative interior (Theorem 6.2).

@[simp]

theorem Rockafellar.OrdinaryConvexProgram.mem_C_iff {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} : x ∈ P.C ↔ P.f₀ x < ⊤

theorem Rockafellar.OrdinaryConvexProgram.f₀_eq_top_of_notMem {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} (hx : x ∉ P.C) : P.f₀ x = ⊤

theorem Rockafellar.OrdinaryConvexProgram.f_ne_bot {m n : ℕ} (P : OrdinaryConvexProgram n m) (i : Fin m) (x : TdafSurface.Rn n) : P.f i x ≠ ⊥

No constraint function ever takes the value -∞: those with i ≤ r are proper and those with i > r are real-valued.

theorem Rockafellar.OrdinaryConvexProgram.exists_coe_f {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} (hx : x ∈ P.C) (i : Fin m) : ∃ (c : ℝ), P.f i x = ↑c

Every constraint function is finite on C: Rockafellar's convention (b) is exactly what makes the Lagrangian an inequality between real numbers.

Feasible solutions, the objective function and the optimal value

def Rockafellar.OrdinaryConvexProgram.feasibleSet {m n : ℕ} (P : OrdinaryConvexProgram n m) : Set (TdafSurface.Rn n)

§28: the set C₀ of feasible solutions to (P).

Equations

• P.feasibleSet = {x : TdafSurface.Rn n | x ∈ P.C ∧ (∀ (i : Fin m), ↑i < P.r → P.f i x ≤ 0) ∧ ∀ (i : Fin m), P.r ≤ ↑i → P.f i x = 0}

@[simp]

theorem Rockafellar.OrdinaryConvexProgram.mem_feasibleSet {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} : x ∈ P.feasibleSet ↔ x ∈ P.C ∧ (∀ (i : Fin m), ↑i < P.r → P.f i x ≤ 0) ∧ ∀ (i : Fin m), P.r ≤ ↑i → P.f i x = 0

theorem Rockafellar.OrdinaryConvexProgram.feasibleSet_subset_C {m n : ℕ} (P : OrdinaryConvexProgram n m) : P.feasibleSet ⊆ P.C

def Rockafellar.OrdinaryConvexProgram.constraintSet {m n : ℕ} (P : OrdinaryConvexProgram n m) : Set (TdafSurface.Rn n)

§28: the intersection C₁ ∩ ⋯ ∩ C_m of the sets cut out by the m constraints, with Cᵢ = {x | fᵢ x ≤ 0} for i ≤ r and Cᵢ = {x | fᵢ x = 0} for i > r. The feasible set is C ∩ C₁ ∩ ⋯ ∩ C_m.

Equations

• P.constraintSet = {x : TdafSurface.Rn n | (∀ (i : Fin m), ↑i < P.r → P.f i x ≤ 0) ∧ ∀ (i : Fin m), P.r ≤ ↑i → P.f i x = 0}

theorem Rockafellar.OrdinaryConvexProgram.feasibleSet_eq_inter {m n : ℕ} (P : OrdinaryConvexProgram n m) : P.feasibleSet = P.C ∩ P.constraintSet

theorem Rockafellar.OrdinaryConvexProgram.convex_constraintSet {m n : ℕ} (P : OrdinaryConvexProgram n m) : Convex ℝ P.constraintSet

C₁ ∩ ⋯ ∩ C_m is convex: the inequality constraints are convex and the equality constraints are affine.

noncomputable def Rockafellar.OrdinaryConvexProgram.objective {m n : ℕ} (P : OrdinaryConvexProgram n m) : TdafSurface.Rn n → EReal

§28: the objective function f = f₀ + δ(· ∣ C₀).

Equations

• P.objective x = P.f₀ x + Tdaf.ConvexAnalysis.indicatorFn P.feasibleSet x

@[simp]

theorem Rockafellar.OrdinaryConvexProgram.objective_of_mem {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} (hx : x ∈ P.feasibleSet) : P.objective x = P.f₀ x

@[simp]

theorem Rockafellar.OrdinaryConvexProgram.objective_of_notMem {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} (hx : x ∉ P.feasibleSet) : P.objective x = ⊤

theorem Rockafellar.OrdinaryConvexProgram.objective_eq_restrict {m n : ℕ} (P : OrdinaryConvexProgram n m) : P.objective = Tdaf.ConvexAnalysis.restrict P.constraintSet P.f₀

The objective function is f₀ restricted to C₁ ∩ ⋯ ∩ C_m: the constraint x ∈ C is automatic, because f₀ is already +∞ off C. This is the form in which convexity and closedness of the objective are read off.

theorem Rockafellar.OrdinaryConvexProgram.convexFn_objective {m n : ℕ} (P : OrdinaryConvexProgram n m) : Tdaf.ConvexAnalysis.ConvexFn P.objective

theorem Rockafellar.OrdinaryConvexProgram.closedFn_objective {m n : ℕ} (P : OrdinaryConvexProgram n m) (hcl₀ : Tdaf.ConvexAnalysis.ClosedFn P.f₀) (hcl : ∀ (i : Fin m), ↑i < P.r → Tdaf.ConvexAnalysis.ClosedFn (P.f i)) : Tdaf.ConvexAnalysis.ClosedFn P.objective

§28: the objective function is closed when f₀, f₁, …, f_r are.

theorem Rockafellar.OrdinaryConvexProgram.objective_ne_bot {m n : ℕ} (P : OrdinaryConvexProgram n m) (x : TdafSurface.Rn n) : P.objective x ≠ ⊥

noncomputable def Rockafellar.OrdinaryConvexProgram.optimalValue {m n : ℕ} (P : OrdinaryConvexProgram n m) : EReal

§28: the optimal value in (P) is the infimum of the objective function.

Equations

• P.optimalValue = ⨅ (x : TdafSurface.Rn n), P.objective x

theorem Rockafellar.OrdinaryConvexProgram.optimalValue_eq_biInf {m n : ℕ} (P : OrdinaryConvexProgram n m) : P.optimalValue = ⨅ x ∈ P.feasibleSet, P.f₀ x

The optimal value is the infimum of f₀ over the feasible solutions.

theorem Rockafellar.OrdinaryConvexProgram.optimalValue_le {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} (hx : x ∈ P.feasibleSet) : P.optimalValue ≤ P.f₀ x

def Rockafellar.OrdinaryConvexProgram.optimalSolutions {m n : ℕ} (P : OrdinaryConvexProgram n m) : Set (TdafSurface.Rn n)

§28: the optimal solutions are the points at which the objective function attains its infimum. The book adds the proviso "provided that f is not identically +∞"; where that fails — no feasible solution at all — argmin is all of ℝⁿ rather than empty, and every theorem below that speaks of optimal solutions carries a hypothesis ruling the degenerate case out.

Equations

• P.optimalSolutions = Tdaf.ConvexAnalysis.argmin P.objective

theorem Rockafellar.OrdinaryConvexProgram.mem_optimalSolutions_iff {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} : x ∈ P.optimalSolutions ↔ P.objective x = P.optimalValue

theorem Rockafellar.OrdinaryConvexProgram.mem_optimalSolutions_iff_of_ne_top {m n : ℕ} (P : OrdinaryConvexProgram n m) (h : P.optimalValue ≠ ⊤) {x : TdafSurface.Rn n} : x ∈ P.optimalSolutions ↔ x ∈ P.feasibleSet ∧ P.f₀ x = P.optimalValue

An optimal solution at which the optimal value is not +∞ is feasible and attains it.

Kuhn–Tucker vectors

noncomputable def Rockafellar.OrdinaryConvexProgram.lagrangeFn {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) : TdafSurface.Rn n → EReal

Rockafellar's h = f₀ + λ₁f₁ + ⋯ + λ_m f_m (§28), the function whose infimum a vector of Kuhn–Tucker coefficients is required to bring down to the optimal value.

Equations

• P.lagrangeFn u x = P.f₀ x + ∑ i : Fin m, ↑(u.ofLp i) * P.f i x

theorem Rockafellar.OrdinaryConvexProgram.lagrangeFn_apply {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) (x : TdafSurface.Rn n) : P.lagrangeFn u x = P.f₀ x + ∑ i : Fin m, ↑(u.ofLp i) * P.f i x

structure Rockafellar.OrdinaryConvexProgram.IsKuhnTuckerVector {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) : Prop

§28: (λ₁, …, λ_m) is a vector of Kuhn–Tucker coefficients for (P) — a Kuhn–Tucker vector — when λᵢ ≥ 0 for i = 1, …, r and the infimum of f₀ + λ₁f₁ + ⋯ + λ_m f_m is finite and equal to the optimal value in (P). This is the book's own definition, not the perturbational inequality of §29 it is equivalent to; mem_kuhnTucker_ineqBifun_iff is the bridge.

• nonneg (i : Fin m) : ↑i < P.r → 0 ≤ u.ofLp i

  The multipliers of the inequality constraints are non-negative.

• ne_bot : ⨅ (x : TdafSurface.Rn n), P.lagrangeFn u x ≠ ⊥

  The infimum of h is not -∞.

• ne_top : ⨅ (x : TdafSurface.Rn n), P.lagrangeFn u x ≠ ⊤

  The infimum of h is not +∞.

• iInf_eq : ⨅ (x : TdafSurface.Rn n), P.lagrangeFn u x = P.optimalValue

  The infimum of h is the optimal value in (P).

h as a finite sum, and its convexity, properness and closedness

noncomputable def Rockafellar.OrdinaryConvexProgram.lagrangeSummand {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) (i : Option (Fin m)) : TdafSurface.Rn n → EReal

The m + 1 summands of h = f₀ + λ₁f₁ + ⋯ + λ_m f_m, indexed by Option (Fin m) with the objective in the none slot. Theorem 23.8 is stated for a finite family, so this is the shape in which the subgradient of h is computed.

Equations

• P.lagrangeSummand u i = i.elim P.f₀ fun (j : Fin m) (x : TdafSurface.Rn n) => ↑(u.ofLp j) * P.f j x

@[simp]

theorem Rockafellar.OrdinaryConvexProgram.lagrangeSummand_none {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) : P.lagrangeSummand u none = P.f₀

@[simp]

theorem Rockafellar.OrdinaryConvexProgram.lagrangeSummand_some {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) (j : Fin m) : P.lagrangeSummand u (some j) = fun (x : TdafSurface.Rn n) => ↑(u.ofLp j) * P.f j x

theorem Rockafellar.OrdinaryConvexProgram.lagrangeFn_eq_finsetSum {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) : P.lagrangeFn u = ∑ i : Option (Fin m), P.lagrangeSummand u i

theorem Rockafellar.OrdinaryConvexProgram.convexFn_lagrangeSummand {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) (i : Option (Fin m)) : Tdaf.ConvexAnalysis.ConvexFn (P.lagrangeSummand u i)

theorem Rockafellar.OrdinaryConvexProgram.proper_lagrangeSummand {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) (i : Option (Fin m)) : Tdaf.ConvexAnalysis.Proper (P.lagrangeSummand u i)

theorem Rockafellar.OrdinaryConvexProgram.closedFn_lagrangeSummand {m n : ℕ} (P : OrdinaryConvexProgram n m) (hcl₀ : Tdaf.ConvexAnalysis.ClosedFn P.f₀) (hcl : ∀ (i : Fin m), ↑i < P.r → Tdaf.ConvexAnalysis.ClosedFn (P.f i)) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) (i : Option (Fin m)) : Tdaf.ConvexAnalysis.ClosedFn (P.lagrangeSummand u i)

theorem Rockafellar.OrdinaryConvexProgram.mem_dom_lagrangeSummand {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) {x : TdafSurface.Rn n} (hx : x ∈ P.C) (i : Option (Fin m)) : x ∈ Tdaf.ConvexAnalysis.dom (P.lagrangeSummand u i)

theorem Rockafellar.OrdinaryConvexProgram.relint_mem_dom_lagrangeSummand {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) {x₀ : TdafSurface.Rn n} (hx₀ : x₀ ∈ intrinsicInterior ℝ P.C) (i : Option (Fin m)) : x₀ ∈ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.dom (P.lagrangeSummand u i))

A relative interior point of C is a relative interior point of the effective domain of every summand of h — which is the constraint qualification Theorem 23.8 asks for. This is exactly Rockafellar's blanket assumption (b), used.

theorem Rockafellar.OrdinaryConvexProgram.convexFn_lagrangeFn {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) : Tdaf.ConvexAnalysis.ConvexFn (P.lagrangeFn u)

theorem Rockafellar.OrdinaryConvexProgram.proper_lagrangeFn {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) : Tdaf.ConvexAnalysis.Proper (P.lagrangeFn u)

theorem Rockafellar.OrdinaryConvexProgram.closedProperConvexFn_lagrangeFn {m n : ℕ} (P : OrdinaryConvexProgram n m) (hcl₀ : Tdaf.ConvexAnalysis.ClosedFn P.f₀) (hcl : ∀ (i : Fin m), ↑i < P.r → Tdaf.ConvexAnalysis.ClosedFn (P.f i)) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) : Tdaf.ConvexAnalysis.ClosedProperConvexFn (P.lagrangeFn u)

Corollary 28.1.1, first step: h is closed when f₀, f₁, …, f_r are.

Elementary properties of h

theorem Rockafellar.OrdinaryConvexProgram.sum_coe_mul_f_ne_bot {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) (x : TdafSurface.Rn n) : ∑ i : Fin m, ↑(u.ofLp i) * P.f i x ≠ ⊥

theorem Rockafellar.OrdinaryConvexProgram.lagrangeFn_ne_bot {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) (x : TdafSurface.Rn n) : P.lagrangeFn u x ≠ ⊥

theorem Rockafellar.OrdinaryConvexProgram.lagrangeFn_eq_top_of_notMem_C {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) {x : TdafSurface.Rn n} (hx : x ∉ P.C) : P.lagrangeFn u x = ⊤

theorem Rockafellar.OrdinaryConvexProgram.lagrangeFn_eq_coe {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} {x : TdafSurface.Rn n} {c₀ : ℝ} (h₀ : P.f₀ x = ↑c₀) {c : Fin m → ℝ} (hc : ∀ (i : Fin m), P.f i x = ↑(c i)) : P.lagrangeFn u x = ↑(c₀ + ∑ i : Fin m, u.ofLp i * c i)

h at a point of C, read as a single real number.

theorem Rockafellar.OrdinaryConvexProgram.lagrangeFn_eq_f₀ {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} {x : TdafSurface.Rn n} (h : ∀ (i : Fin m), ↑(u.ofLp i) * P.f i x = 0) : P.lagrangeFn u x = P.f₀ x

When every multiplier term vanishes, h agrees with the objective f₀.

theorem Rockafellar.OrdinaryConvexProgram.lagrangeFn_le_f₀ {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) {x : TdafSurface.Rn n} (hx : x ∈ P.feasibleSet) : P.lagrangeFn u x ≤ P.f₀ x

Theorem 28.1, the inequality the proof rests on: on the feasible set every constraint term is non-positive, so h ≤ f₀.

theorem Rockafellar.OrdinaryConvexProgram.lagrangeFn_le_objective {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) (x : TdafSurface.Rn n) : P.lagrangeFn u x ≤ P.objective x

h ≤ f everywhere: below the feasible set by lagrangeFn_le_f₀, and off it because the objective function is +∞ there.

theorem Rockafellar.OrdinaryConvexProgram.iInf_lagrangeFn_le_optimalValue {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) : ⨅ (x : TdafSurface.Rn n), P.lagrangeFn u x ≤ P.optimalValue

theorem Rockafellar.OrdinaryConvexProgram.IsKuhnTuckerVector.optimalValue_ne_top {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : P.IsKuhnTuckerVector u) : P.optimalValue ≠ ⊤

theorem Rockafellar.OrdinaryConvexProgram.IsKuhnTuckerVector.optimalValue_ne_bot {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : P.IsKuhnTuckerVector u) : P.optimalValue ≠ ⊥

Theorem 28.1: solving (P) by minimising h

theorem Rockafellar.theorem_28_1 {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : P.IsKuhnTuckerVector u) : {x : TdafSurface.Rn n | x ∈ Tdaf.ConvexAnalysis.argmin (P.lagrangeFn u) ∧ (∀ (i : Fin m), ↑i < P.r ∧ u.ofLp i = 0 → P.f i x ≤ 0) ∧ ∀ (i : Fin m), ¬(↑i < P.r ∧ u.ofLp i = 0) → P.f i x = 0} = P.optimalSolutions

Theorem 28.1. Let (λ₁, …, λ_m) be a Kuhn–Tucker vector for (P), let D be the set of minimisers of h = f₀ + λ₁f₁ + ⋯ + λ_m f_m over ℝⁿ, let I be the set of i ≤ r with λᵢ = 0 and J its complement in {1, …, m}. Then the optimal solutions of (P) are exactly the x̄ ∈ D with fᵢ(x̄) = 0 for i ∈ J and fᵢ(x̄) ≤ 0 for i ∈ I.

Rockafellar's summary "h ≤ f everywhere, with equality if and only if x is a feasible solution such that λᵢfᵢ(x) = 0" is very slightly too strong: outside C both functions are +∞, so equality holds there too although the point is infeasible. Nothing is lost, because inf h is finite and so no such point lies in either minimum set.

theorem Rockafellar.corollary_28_1_1 {m n : ℕ} (P : OrdinaryConvexProgram n m) (hcl₀ : Tdaf.ConvexAnalysis.ClosedFn P.f₀) (hcl : ∀ (i : Fin m), ↑i < P.r → Tdaf.ConvexAnalysis.ClosedFn (P.f i)) {u : TdafSurface.Rn m} (hu : P.IsKuhnTuckerVector u) {w : TdafSurface.Rn n} (hmin : Tdaf.ConvexAnalysis.argmin (P.lagrangeFn u) = {w}) : P.optimalSolutions = {w}

Corollary 28.1.1. If the fᵢ are all closed and the infimum of h is attained at a unique point w, then w is the unique optimal solution to (P). Uniqueness is Theorem 28.1; the content is existence, which follows because epi f ⊆ epi h gives the objective no direction of recession either, so Theorem 27.2 applies.

The perturbation function and the bifunction of (P)

noncomputable def Rockafellar.OrdinaryConvexProgram.ineqBifun {m n : ℕ} (P : OrdinaryConvexProgram n m) : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)

The bifunction of an ordinary convex program, which is what makes (P) a generalized convex program in the sense of §29: F u x is f₀ x when x satisfies the constraints of the perturbed program (P_u) — fᵢ x ≤ vᵢ for i ≤ r and fᵢ x = vᵢ for i > r — and +∞ otherwise. The constraint x ∈ C is not imposed: f₀ is already +∞ off C.

Equations

• P.ineqBifun u = Tdaf.ConvexAnalysis.restrict {y : TdafSurface.Rn n | (∀ (i : Fin m), ↑i < P.r → P.f i y ≤ ↑(u.ofLp i)) ∧ ∀ (i : Fin m), P.r ≤ ↑i → P.f i y = ↑(u.ofLp i)} P.f₀

theorem Rockafellar.OrdinaryConvexProgram.ineqBifun_of_mem {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} {x : TdafSurface.Rn n} (h : (∀ (i : Fin m), ↑i < P.r → P.f i x ≤ ↑(u.ofLp i)) ∧ ∀ (i : Fin m), P.r ≤ ↑i → P.f i x = ↑(u.ofLp i)) : P.ineqBifun u x = P.f₀ x

theorem Rockafellar.OrdinaryConvexProgram.ineqBifun_of_notMem {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} {x : TdafSurface.Rn n} (h : ¬((∀ (i : Fin m), ↑i < P.r → P.f i x ≤ ↑(u.ofLp i)) ∧ ∀ (i : Fin m), P.r ≤ ↑i → P.f i x = ↑(u.ofLp i))) : P.ineqBifun u x = ⊤

theorem Rockafellar.OrdinaryConvexProgram.ineqBifun_eq_top_of_notMem_C {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} (hx : x ∉ P.C) (u : TdafSurface.Rn m) : P.ineqBifun u x = ⊤

@[simp]

theorem Rockafellar.OrdinaryConvexProgram.ineqBifun_zero {m n : ℕ} (P : OrdinaryConvexProgram n m) : P.ineqBifun 0 = P.objective

At the unperturbed parameter the bifunction is the objective function of (P).

noncomputable def Rockafellar.OrdinaryConvexProgram.perturbFn {m n : ℕ} (P : OrdinaryConvexProgram n m) : TdafSurface.Rn m → EReal

§28: the perturbation function p of (P). p u is the optimal value of the perturbed program (P_u), and p 0 is the optimal value of (P).

Equations

• P.perturbFn = Tdaf.ConvexAnalysis.infBifun P.ineqBifun

theorem Rockafellar.OrdinaryConvexProgram.perturbFn_apply {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) : P.perturbFn u = ⨅ (x : TdafSurface.Rn n), P.ineqBifun u x

@[simp]

theorem Rockafellar.OrdinaryConvexProgram.perturbFn_zero {m n : ℕ} (P : OrdinaryConvexProgram n m) : P.perturbFn 0 = P.optimalValue

§28: "of course, p(0) is the optimal value in (P)".

Theorem 28.2: existence of Kuhn–Tucker vectors

theorem Rockafellar.OrdinaryConvexProgram.optimalValue_eq_biInf_constraintSet {m n : ℕ} (P : OrdinaryConvexProgram n m) : P.optimalValue = ⨅ x ∈ P.constraintSet, P.f₀ x

The optimal value read as an infimum over C₁ ∩ ⋯ ∩ C_m rather than over C₀: f₀ is +∞ off C, so the two infima agree. This is the form the backbone's optimalValue takes.

theorem Rockafellar.theorem_28_2 {m n : ℕ} (P : OrdinaryConvexProgram n m) {I : Finset (Fin m)} (hIr : ∀ (i : Fin m), P.r ≤ ↑i → i ∉ I) (hIaff : ∀ (i : Fin m), ↑i < P.r → i ∉ I → ∃ (a : TdafSurface.Rn n →ᵃ[ℝ] ℝ), ∀ (x : TdafSurface.Rn n), P.f i x = ↑(a x)) (hbot : P.optimalValue ≠ ⊥) (hslater : ∃ x ∈ intrinsicInterior ℝ P.C, (∀ i ∈ I, P.f i x < 0) ∧ x ∈ P.constraintSet) : ∃ (u : TdafSurface.Rn m), P.IsKuhnTuckerVector u

Theorem 28.2. Let I be a set of indices containing every i at which fᵢ fails to be affine — so I contains no equality constraint. If the optimal value in (P) is not -∞ and (P) has a feasible solution in ri C satisfying with strict inequality all the inequality constraints for i ∈ I, then (P) has a Kuhn–Tucker vector.

I is taken as a Finset (Fin m) with the book's condition split into its two halves. The proof translates the book's single family split at r into the backbone's role-split families of exists_isKuhnTuckerVector_of_slater: an equality constraint becomes two weak inequalities, and its multiplier is recovered as their difference — Rockafellar's own reduction.

theorem Rockafellar.corollary_28_2_1 {m n : ℕ} (P : OrdinaryConvexProgram n m) (hrm : P.r = m) (hbot : P.optimalValue ≠ ⊥) (hslater : ∃ x ∈ P.C, ∀ (i : Fin m), P.f i x < 0) : ∃ (u : TdafSurface.Rn m), P.IsKuhnTuckerVector u

Corollary 28.2.1. For a program with only inequality constraints the Slater point need not lie in ri C: some x ∈ C with f₁(x) < 0, …, f_m(x) < 0 is enough. It is a special case of Theorem 28.2 and not a substitute for it, since it needs r = m and a point satisfying every constraint strictly.

noncomputable def Rockafellar.linConstraint {n : ℕ} (v : TdafSurface.Rn n) (α : ℝ) : TdafSurface.Rn n →ᵃ[ℝ] ℝ

The book's linear constraint ⟨a, x⟩ - α, read as an affine function on ℝⁿ.

Equations

• Rockafellar.linConstraint v α = (↑(TdafSurface.linFn v)).toAffineMap - AffineMap.const ℝ (TdafSurface.Rn n) α

@[simp]

theorem Rockafellar.linConstraint_apply {n : ℕ} (v : TdafSurface.Rn n) (α : ℝ) (x : TdafSurface.Rn n) : (linConstraint v α) x = ((TdafSurface.pairing n) x) v - α

theorem Rockafellar.corollary_28_2_2 {m n : ℕ} (P : OrdinaryConvexProgram n m) (hlin : ∀ (i : Fin m), ∃ (v : TdafSurface.Rn n) (α : ℝ), ∀ (x : TdafSurface.Rn n), P.f i x = ↑(((TdafSurface.pairing n) x) v - α)) (hbot : P.optimalValue ≠ ⊥) (hfeas : ∃ x ∈ intrinsicInterior ℝ P.C, x ∈ P.constraintSet) : ∃ (u : TdafSurface.Rn m), P.IsKuhnTuckerVector u

Corollary 28.2.2, stated in the book with no proof. A program whose constraints are all linear, fᵢ(x) = ⟨aᵢ, x⟩ - αᵢ, needs nothing beyond a feasible solution in ri C. It is Theorem 28.2 at I = ∅: with no non-affine constraint there is nothing to satisfy strictly.

The Lagrangian of an ordinary convex program

def Rockafellar.OrdinaryConvexProgram.multiplierCone {m n : ℕ} (P : OrdinaryConvexProgram n m) : Set (TdafSurface.Rn m)

§28: the cone E_r = {u* = (v₁*, …, v_m*) ∈ ℝᵐ | vᵢ* ≥ 0, i = 1, …, r} of admissible Lagrange multiplier vectors. vᵢ* is the Lagrange multiplier associated with the i-th constraint of (P).

Equations

• P.multiplierCone = {u : TdafSurface.Rn m | ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i}

@[simp]

theorem Rockafellar.OrdinaryConvexProgram.mem_multiplierCone {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} : u ∈ P.multiplierCone ↔ ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i

theorem Rockafellar.OrdinaryConvexProgram.zero_mem_multiplierCone {m n : ℕ} (P : OrdinaryConvexProgram n m) : 0 ∈ P.multiplierCone

noncomputable def Rockafellar.OrdinaryConvexProgram.unitVec (m : ℕ) (i : Fin m) : TdafSurface.Rn m

eᵢ, the i-th row of the m × m identity matrix (§28).

Equations

• Rockafellar.OrdinaryConvexProgram.unitVec m i = EuclideanSpace.single i 1

@[simp]

theorem Rockafellar.OrdinaryConvexProgram.unitVec_apply (m : ℕ) (i j : Fin m) : (unitVec m i).ofLp j = if j = i then 1 else 0

theorem Rockafellar.OrdinaryConvexProgram.unitVec_mem_multiplierCone {m n : ℕ} (P : OrdinaryConvexProgram n m) (i : Fin m) : unitVec m i ∈ P.multiplierCone

theorem Rockafellar.OrdinaryConvexProgram.exists_coe_f₀ {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} (hx : x ∈ P.C) : ∃ (c : ℝ), P.f₀ x = ↑c

f₀ is finite on C.

theorem Rockafellar.OrdinaryConvexProgram.exists_coe_lagrangeFn {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) {x : TdafSurface.Rn n} (hx : x ∈ P.C) : ∃ (c : ℝ), P.lagrangeFn u x = ↑c

h = f₀ + λ₁f₁ + ⋯ + λ_m f_m is finite at every point of C, whatever the multipliers.

@[simp]

theorem Rockafellar.OrdinaryConvexProgram.lagrangeFn_zero {m n : ℕ} (P : OrdinaryConvexProgram n m) (x : TdafSurface.Rn n) : P.lagrangeFn 0 x = P.f₀ x

theorem Rockafellar.OrdinaryConvexProgram.lagrangeFn_unitVec {m n : ℕ} (P : OrdinaryConvexProgram n m) (i : Fin m) (x : TdafSurface.Rn n) : P.lagrangeFn (unitVec m i) x = P.f₀ x + P.f i x

noncomputable def Rockafellar.OrdinaryConvexProgram.programLagrangian {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) (x : TdafSurface.Rn n) : EReal

§28: the Lagrangian L of (P), a function on ℝᵐ × ℝⁿ: h(x) when u* ∈ E_r and x ∈ C, -∞ when u* ∉ E_r and x ∈ C, +∞ when x ∉ C.

Equations

• P.programLagrangian u x = ⨅ (_ : x ∈ P.C), ⨆ (_ : u ∈ P.multiplierCone), P.lagrangeFn u x

theorem Rockafellar.OrdinaryConvexProgram.programLagrangian_eq_lagrangeFn {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} {x : TdafSurface.Rn n} (hx : x ∈ P.C) (hu : u ∈ P.multiplierCone) : P.programLagrangian u x = P.lagrangeFn u x

theorem Rockafellar.OrdinaryConvexProgram.programLagrangian_eq_bot {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} {x : TdafSurface.Rn n} (hx : x ∈ P.C) (hu : u ∉ P.multiplierCone) : P.programLagrangian u x = ⊥

theorem Rockafellar.OrdinaryConvexProgram.programLagrangian_eq_top {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} (hx : x ∉ P.C) (u : TdafSurface.Rn m) : P.programLagrangian u x = ⊤

noncomputable def Rockafellar.OrdinaryConvexProgram.saddleFn {m n : ℕ} (P : OrdinaryConvexProgram n m) : TdafSurface.Rn m × TdafSurface.Rn n → EReal

The Lagrangian read as a saddle-function on ℝᵐ × ℝⁿ, which is the shape §36's minimax theory and the backbone's IsSaddlePoint, maximin and minimax are stated in.

Equations

• P.saddleFn q = P.programLagrangian q.1 q.2

theorem Rockafellar.OrdinaryConvexProgram.saddleFn_apply {m n : ℕ} (P : OrdinaryConvexProgram n m) (q : TdafSurface.Rn m × TdafSurface.Rn n) : P.saddleFn q = P.programLagrangian q.1 q.2

The program is recovered from its Lagrangian

"L reflects all the structure of (P), because the (m + 3)-tuple (C, f₀, …, f_m, r) can be recovered completely from L" — stated here as three theorems and one consequence.

theorem Rockafellar.OrdinaryConvexProgram.mem_C_iff_programLagrangian_ne_top {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} : x ∈ P.C ↔ P.programLagrangian 0 x ≠ ⊤

C is where L is not +∞.

theorem Rockafellar.OrdinaryConvexProgram.mem_multiplierCone_iff_programLagrangian_ne_bot {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} {x : TdafSurface.Rn n} (hx : x ∈ P.C) : u ∈ P.multiplierCone ↔ P.programLagrangian u x ≠ ⊥

E_r is where L(·, x) is not -∞, for any x ∈ C.

theorem Rockafellar.OrdinaryConvexProgram.setOf_programLagrangian_finite {m n : ℕ} (P : OrdinaryConvexProgram n m) : {q : TdafSurface.Rn m × TdafSurface.Rn n | P.programLagrangian q.1 q.2 ≠ ⊥ ∧ P.programLagrangian q.1 q.2 ≠ ⊤} = P.multiplierCone ×ˢ P.C

§28: "the set of points where L is finite is E_r × C".

theorem Rockafellar.OrdinaryConvexProgram.f₀_eq_programLagrangian {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} (hx : x ∈ P.C) : P.f₀ x = P.programLagrangian 0 x

§28: f₀(x) = L(0, x) for x ∈ C.

theorem Rockafellar.OrdinaryConvexProgram.f_eq_programLagrangian_sub {m n : ℕ} (P : OrdinaryConvexProgram n m) {x : TdafSurface.Rn n} (hx : x ∈ P.C) (i : Fin m) : P.f i x = P.programLagrangian (unitVec m i) x - P.programLagrangian 0 x

§28: fᵢ(x) = L(eᵢ, x) - L(0, x) for x ∈ C.

theorem Rockafellar.OrdinaryConvexProgram.r_eq_of_multiplierCone_eq {m n : ℕ} {P₁ P₂ : OrdinaryConvexProgram n m} (h : P₁.multiplierCone = P₂.multiplierCone) : P₁.r = P₂.r

r is recovered from L as well, because E_r is.

theorem Rockafellar.OrdinaryConvexProgram.eq_of_programLagrangian_eq {m n : ℕ} {P₁ P₂ : OrdinaryConvexProgram n m} (h : P₁.programLagrangian = P₂.programLagrangian) : P₁.C = P₂.C ∧ P₁.r = P₂.r ∧ (∀ x ∈ P₁.C, P₁.f₀ x = P₂.f₀ x) ∧ ∀ x ∈ P₁.C, ∀ (i : Fin m), P₁.f i x = P₂.f i x

§28: "There is thus a one-to-one correspondence between ordinary convex programs and their Lagrangians." Two ordinary convex programs with the same Lagrangian have the same C, the same r, and the same f₀, f₁, …, f_m on C — which is all the data the tuple carries, the values of fᵢ off C being irrelevant to (P).

The Lagrangian is the §29 Lagrangian of ineqBifun

Rockafellar's L(u*, x) = inf {f₀(x) + v₁*v₁ + ⋯ + v_m*v_m | u ∈ U_x} is the §29 definition of the Lagrangian of the bifunction of (P), so programLagrangian agrees with the backbone's lagrangian and everything §29 proves about the latter applies.

theorem Rockafellar.OrdinaryConvexProgram.lagrangian_ineqBifun {m n : ℕ} (P : OrdinaryConvexProgram n m) : Tdaf.ConvexAnalysis.lagrangian (TdafSurface.pairing m) P.ineqBifun = P.programLagrangian

§28: the Lagrangian of (P) is the §29 Lagrangian of the bifunction of (P), taken with the Euclidean pairing on ℝᵐ.

theorem Rockafellar.OrdinaryConvexProgram.saddleLagrangian_ineqBifun {m n : ℕ} (P : OrdinaryConvexProgram n m) : Tdaf.ConvexAnalysis.saddleLagrangian (TdafSurface.pairing m) P.ineqBifun = fun (q : TdafSurface.Rn m × TdafSurface.Rn n) => P.programLagrangian q.1 q.2

The §29 saddle-Lagrangian of (P)'s bifunction, read on ℝᵐ × ℝⁿ, is L.

theorem Rockafellar.OrdinaryConvexProgram.concaveFn_programLagrangian {m n : ℕ} (P : OrdinaryConvexProgram n m) (x : TdafSurface.Rn n) : Tdaf.ConvexAnalysis.ConcaveFn fun (u : TdafSurface.Rn m) => P.programLagrangian u x

§28: "L is concave in u* for each x". Free from §29: the Lagrangian of a bifunction is a concave conjugate in the price variable.

Theorem 28.3: saddle-points of the Lagrangian and the Kuhn–Tucker conditions

noncomputable def Rockafellar.activeIndices {m : ℕ} (u : TdafSurface.Rn m) : Finset (Fin m)

The indices i with λᵢ ≠ 0: Rockafellar's parenthesis "(Omit terms with λᵢ = 0.)" in condition (c) of Theorem 28.3. The omission is not cosmetic — ∂fᵢ(x̄) can be empty at a boundary point of dom fᵢ, and then 0 · ∂fᵢ(x̄) would be empty rather than {0}.

Equations

• Rockafellar.activeIndices u = {i : Fin m | u.ofLp i ≠ 0}

theorem Rockafellar.mem_activeIndices {m : ℕ} {u : TdafSurface.Rn m} {i : Fin m} : i ∈ activeIndices u ↔ u.ofLp i ≠ 0

theorem Rockafellar.OrdinaryConvexProgram.iSup_programLagrangian {m n : ℕ} (P : OrdinaryConvexProgram n m) (x : TdafSurface.Rn n) : ⨆ (u : TdafSurface.Rn m), P.programLagrangian u x = P.objective x

§28: sup_{u*} L(u*, x) = f₀(x) + δ(x | C₀), the objective function of (P), whatever x is.

theorem Rockafellar.OrdinaryConvexProgram.iInf_programLagrangian_of_mem {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : u ∈ P.multiplierCone) : ⨅ (x : TdafSurface.Rn n), P.programLagrangian u x = ⨅ (x : TdafSurface.Rn n), P.lagrangeFn u x

§28, the case ū* ∈ E_r: the infimum of L(ū*, ·) is the infimum of h.

theorem Rockafellar.OrdinaryConvexProgram.iInf_programLagrangian_of_notMem {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : u ∉ P.multiplierCone) : ⨅ (x : TdafSurface.Rn n), P.programLagrangian u x = ⊥

§28, the case ū* ∉ E_r: the infimum of L(ū*, ·) is -∞.

theorem Rockafellar.OrdinaryConvexProgram.iInf_lagrangeFn_ne_top {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) : ⨅ (z : TdafSurface.Rn n), P.lagrangeFn u z ≠ ⊤

inf h is never +∞: h is finite at every point of the non-empty set C.

theorem Rockafellar.OrdinaryConvexProgram.isSaddlePoint_programLagrangian_iff {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} {x : TdafSurface.Rn n} : Tdaf.ConvexAnalysis.IsSaddlePoint P.saddleFn (u, x) ↔ u ∈ P.multiplierCone ∧ x ∈ P.feasibleSet ∧ ⨅ (z : TdafSurface.Rn n), P.lagrangeFn u z = P.f₀ x

§28, condition (d): (ū*, x̄) is a saddle-point of L exactly when ū* ∈ E_r, x̄ is a feasible solution, and inf h = f₀(x̄).

theorem Rockafellar.OrdinaryConvexProgram.theorem_28_3 {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} {x : TdafSurface.Rn n} : P.IsKuhnTuckerVector u ∧ x ∈ P.optimalSolutions ↔ Tdaf.ConvexAnalysis.IsSaddlePoint P.saddleFn (u, x)

Theorem 28.3. In order that ū* be a Kuhn–Tucker vector for (P) and x̄ be an optimal solution to (P), it is necessary and sufficient that (ū*, x̄) be a saddle-point of the Lagrangian L of (P).

The Kuhn–Tucker conditions (a), (b), (c)

theorem Rockafellar.OrdinaryConvexProgram.subgradient_lagrangeFn {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : u ∈ P.multiplierCone) (x : TdafSurface.Rn n) : Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) (P.lagrangeFn u) x = Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) P.f₀ x + ∑ i ∈ activeIndices u, u.ofLp i • Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) (P.f i) x

§28, the subgradient of h decomposed by Theorem 23.8. The multiplier terms with λᵢ = 0 contribute {0} and are omitted, exactly as the book's parenthesis in condition (c) says.

theorem Rockafellar.OrdinaryConvexProgram.theorem_28_3_kuhnTucker {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} {x : TdafSurface.Rn n} : P.IsKuhnTuckerVector u ∧ x ∈ P.optimalSolutions ↔ (∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i ∧ P.f i x ≤ 0 ∧ ↑(u.ofLp i) * P.f i x = 0) ∧ (∀ (i : Fin m), P.r ≤ ↑i → P.f i x = 0) ∧ 0 ∈ Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) P.f₀ x + ∑ i ∈ activeIndices u, u.ofLp i • Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) (P.f i) x

Theorem 28.3, second half: the saddle-point condition holds if and only if x̄ and the multipliers λᵢ satisfy the Kuhn–Tucker conditions

• (a) λᵢ ≥ 0, fᵢ(x̄) ≤ 0 and λᵢfᵢ(x̄) = 0 for i = 1, …, r;
• (b) fᵢ(x̄) = 0 for i = r + 1, …, m;
• (c) 0 ∈ ∂f₀(x̄) + λ₁∂f₁(x̄) + ⋯ + λ_m∂f_m(x̄) (terms with λᵢ = 0 omitted).

x̄ ∈ C is not a separate clause: it follows from (c), because ∂f₀(x̄) is non-empty there and dom f₀ = C.

theorem Rockafellar.OrdinaryConvexProgram.corollary_28_3_1 {m n : ℕ} (P : OrdinaryConvexProgram n m) (hkt : ∃ (u : TdafSurface.Rn m), P.IsKuhnTuckerVector u) {x : TdafSurface.Rn n} : x ∈ P.optimalSolutions ↔ ∃ (u : TdafSurface.Rn m), Tdaf.ConvexAnalysis.IsSaddlePoint P.saddleFn (u, x)

Corollary 28.3.1, the Kuhn–Tucker Theorem. For a program with at least one Kuhn–Tucker vector, x̄ is an optimal solution if and only if some ū* makes (ū*, x̄) a saddle-point of L. No proof is printed in the book. The book's hypothesis is "satisfying the hypothesis of Theorem 28.2"; only its conclusion is used, so that is the hypothesis carried here.

theorem Rockafellar.OrdinaryConvexProgram.corollary_28_3_1_kuhnTucker {m n : ℕ} (P : OrdinaryConvexProgram n m) (hkt : ∃ (u : TdafSurface.Rn m), P.IsKuhnTuckerVector u) {x : TdafSurface.Rn n} : x ∈ P.optimalSolutions ↔ ∃ (u : TdafSurface.Rn m), (∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i ∧ P.f i x ≤ 0 ∧ ↑(u.ofLp i) * P.f i x = 0) ∧ (∀ (i : Fin m), P.r ≤ ↑i → P.f i x = 0) ∧ 0 ∈ Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) P.f₀ x + ∑ i ∈ activeIndices u, u.ofLp i • Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) (P.f i) x

Corollary 28.3.1, second form: optimality is equivalent to the existence of Lagrange multiplier values satisfying the Kuhn–Tucker conditions.

Theorem 28.4: the optimal value as a saddle-value

noncomputable def Rockafellar.OrdinaryConvexProgram.dualFn {m n : ℕ} (P : OrdinaryConvexProgram n m) : TdafSurface.Rn m → EReal

§28: g(u*) = inf_x L(u*, x), the concave function whose maximisation over ℝᵐ is dual to (P).

Equations

• P.dualFn u = ⨅ (x : TdafSurface.Rn n), P.programLagrangian u x

theorem Rockafellar.OrdinaryConvexProgram.dualFn_apply {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) : P.dualFn u = ⨅ (x : TdafSurface.Rn n), P.programLagrangian u x

theorem Rockafellar.OrdinaryConvexProgram.minimax_saddleFn {m n : ℕ} (P : OrdinaryConvexProgram n m) : Tdaf.ConvexAnalysis.minimax P.saddleFn = P.optimalValue

§28: inf_x sup_{u*} L(u*, x) is the optimal value in (P).

theorem Rockafellar.OrdinaryConvexProgram.maximin_saddleFn_eq_iSup_dualFn {m n : ℕ} (P : OrdinaryConvexProgram n m) : Tdaf.ConvexAnalysis.maximin P.saddleFn = ⨆ (u : TdafSurface.Rn m), P.dualFn u

theorem Rockafellar.OrdinaryConvexProgram.maximin_saddleFn_le {m n : ℕ} (P : OrdinaryConvexProgram n m) : Tdaf.ConvexAnalysis.maximin P.saddleFn ≤ P.optimalValue

Weak duality: sup inf ≤ inf sup = α.

theorem Rockafellar.OrdinaryConvexProgram.theorem_28_4_saddleValue {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} {x : TdafSurface.Rn n} (hu : P.IsKuhnTuckerVector u) (hx : x ∈ P.optimalSolutions) : P.programLagrangian u x = P.optimalValue

Theorem 28.4, first sentence: at a Kuhn–Tucker vector and an optimal solution the saddle-value L(ū*, x̄) is the optimal value in (P).

theorem Rockafellar.OrdinaryConvexProgram.theorem_28_4 {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} : P.IsKuhnTuckerVector u ↔ ⊥ < ⨅ (x : TdafSurface.Rn n), P.programLagrangian u x ∧ ⨅ (x : TdafSurface.Rn n), P.programLagrangian u x = Tdaf.ConvexAnalysis.maximin P.saddleFn ∧ Tdaf.ConvexAnalysis.maximin P.saddleFn = Tdaf.ConvexAnalysis.minimax P.saddleFn

Theorem 28.4. ū* is a Kuhn–Tucker vector for (P) if and only if -∞ < inf_x L(ū*, x) = sup_{u*} inf_x L(u*, x) = inf_x sup_{u*} L(u*, x), and the common extremum value is then the optimal value in (P).

theorem Rockafellar.OrdinaryConvexProgram.theorem_28_4_value {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : P.IsKuhnTuckerVector u) : Tdaf.ConvexAnalysis.maximin P.saddleFn = P.optimalValue ∧ Tdaf.ConvexAnalysis.minimax P.saddleFn = P.optimalValue

The common value in Theorem 28.4 is the optimal value in (P).

theorem Rockafellar.OrdinaryConvexProgram.dualFn_eq_concaveConj {m n : ℕ} (P : OrdinaryConvexProgram n m) : P.dualFn = Tdaf.ConvexAnalysis.concaveConj (TdafSurface.pairing m) fun (w : TdafSurface.Rn m) => -P.perturbFn w

g is the concave conjugate of -p, which is Rockafellar's remark in the form the backbone states it.

theorem Rockafellar.OrdinaryConvexProgram.concaveFn_dualFn {m n : ℕ} (P : OrdinaryConvexProgram n m) : Tdaf.ConvexAnalysis.ConcaveFn P.dualFn

§28: "The concavity of g … is immediate." Here it is immediate from §29 instead: g is a concave conjugate.

theorem Rockafellar.OrdinaryConvexProgram.dualFn_eq_neg_conj_perturbFn {m n : ℕ} (P : OrdinaryConvexProgram n m) (u : TdafSurface.Rn m) : P.dualFn u = -Tdaf.ConvexAnalysis.conj (TdafSurface.pairing m) P.perturbFn (-u)

§28: g(u*) = -p*(-u*), where p is the perturbation function of (P).

theorem Rockafellar.OrdinaryConvexProgram.corollary_28_4_1 {m n : ℕ} (P : OrdinaryConvexProgram n m) (hkt : ∃ (u : TdafSurface.Rn m), P.IsKuhnTuckerVector u) {u : TdafSurface.Rn m} : P.IsKuhnTuckerVector u ↔ u ∈ Tdaf.ConvexAnalysis.argmax P.dualFn

Corollary 28.4.1. For a program with at least one Kuhn–Tucker vector, the Kuhn–Tucker vectors are precisely the points where the concave function g(u*) = inf_x L(u*, x) attains its supremum over ℝᵐ. No proof is printed in the book: weak duality gives g ≤ α everywhere, the assumed Kuhn–Tucker vector gives a point where g = α, and g(ū*) = α with α finite is the definition of a Kuhn–Tucker vector.

The decomposition principle

Suppose the coordinates of ℝⁿ split as x = (x₁, …, x_s) with x_k ∈ ℝ^{n_k} and every fᵢ separable in that splitting. Once a Kuhn–Tucker vector has reduced (P) to minimising h = f₀ + λ₁f₁ + ⋯ + λ_m f_m over C (Theorem 28.1), h is separable too, and the problem splits into the s independent problems "minimise h_k over C^k", C^k = dom h_k.

The splitting is hypothesised as a linear equivalence e from ℝ^{n₁} × ⋯ × ℝ^{n_s} to ℝⁿ: linearity is what carries n₁ + ⋯ + n_s = n, since a bare bijection between these two types exists whatever the n_k are. Separability of h is hypothesised in the form the book asserts it rather than derived from separability of each fᵢ, because distributing λᵢ · ∑ₖ fᵢₖ(xₖ) over the sum would need EReal to be a semiring.

theorem Rockafellar.OrdinaryConvexProgram.dom_lagrangeFn {m n : ℕ} (P : OrdinaryConvexProgram n m) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) : Tdaf.ConvexAnalysis.dom (P.lagrangeFn u) = P.C

The effective domain of the Lagrangian h = f₀ + λ₁f₁ + ⋯ + λ_m f_m is C.

Off C it is +∞ because f₀ is and the multipliers of the inequality constraints are non-negative; on C it is a real number, because Rockafellar's convention (b) makes every fᵢ finite there. This is the sense in which "minimise h over C" is an unconstrained problem.

theorem Rockafellar.OrdinaryConvexProgram.decomposition_C {m n : ℕ} (P : OrdinaryConvexProgram n m) {s : ℕ} {nk : Fin s → ℕ} (e : ((k : Fin s) → TdafSurface.Rn (nk k)) ≃ₗ[ℝ] TdafSurface.Rn n) {u : TdafSurface.Rn m} (hu : ∀ (i : Fin m), ↑i < P.r → 0 ≤ u.ofLp i) {h : (k : Fin s) → TdafSurface.Rn (nk k) → EReal} (hb : ∀ (k : Fin s) (z : TdafSurface.Rn (nk k)), h k z ≠ ⊥) (hsep : ∀ (x : (k : Fin s) → TdafSurface.Rn (nk k)), P.lagrangeFn u (e x) = ∑ k : Fin s, h k (x k)) : ⇑e ⁻¹' P.C = Set.univ.pi fun (k : Fin s) => Tdaf.ConvexAnalysis.dom (h k)

§28: in the coordinates x = (x₁, …, x_s) the set C is the product of the sets C^k = dom h_k.

This is dom_sepSum read through e, on the strength of dom_lagrangeFn. Properness of the h_k is not needed — only that none of them takes the value −∞, which is automatic for the h_k the principle produces.

theorem Rockafellar.OrdinaryConvexProgram.decomposition_argmin_lagrangeFn {m n : ℕ} (P : OrdinaryConvexProgram n m) {s : ℕ} {nk : Fin s → ℕ} (e : ((k : Fin s) → TdafSurface.Rn (nk k)) ≃ₗ[ℝ] TdafSurface.Rn n) {u : TdafSurface.Rn m} {h : (k : Fin s) → TdafSurface.Rn (nk k) → EReal} (hp : ∀ (k : Fin s), Tdaf.ConvexAnalysis.Proper (h k)) (hsep : ∀ (x : (k : Fin s) → TdafSurface.Rn (nk k)), P.lagrangeFn u (e x) = ∑ k : Fin s, h k (x k)) : ⇑e ⁻¹' Tdaf.ConvexAnalysis.argmin (P.lagrangeFn u) = Set.univ.pi fun (k : Fin s) => Tdaf.ConvexAnalysis.argmin (h k)

§28, the decomposition principle itself: minimising h over C is the s independent problems "minimise h_k over C^k".

With theorem_28_1 this is the assertion about (P): the optimal solutions of (P) are the points of argmin h that satisfy complementary slackness, and argmin h is now a product. Each factor is a problem in ℝ^{n_k}, while by Corollary 28.4.1 finding u is a problem in ℝᵐ — which is the reduction in dimensionality the passage is about.

Two programs with no Kuhn-Tucker vector

Two unnumbered counterexamples of §28, both justifying the constraint qualification in Theorem 28.2. The first has a unique optimal solution, a finite optimal value and no Kuhn–Tucker vector; the second has only linear constraints, so it satisfies every hypothesis of Corollary 28.2.2 except the feasible point in ri C, and it too has none.

noncomputable def Rockafellar.coordAffine (n : ℕ) (j : Fin n) : TdafSurface.Rn n →ᵃ[ℝ] ℝ

The j-th coordinate of ℝⁿ, as an affine function.

Equations

• Rockafellar.coordAffine n j = { toFun := fun (x : TdafSurface.Rn n) => x.ofLp j, map_add' := ⋯, map_smul' := ⋯ }.toAffineMap

@[simp]

theorem Rockafellar.coordAffine_apply (n : ℕ) (j : Fin n) (x : TdafSurface.Rn n) : (coordAffine n j) x = x.ofLp j

A program with a unique optimal solution and no Kuhn–Tucker vector

noncomputable def Rockafellar.ex1Constraint₁ : TdafSurface.Rn 2 → EReal

The constraint f₁(ξ₁, ξ₂) = ξ₂ of the counterexample.

Equations

• Rockafellar.ex1Constraint₁ x = ↑(x.ofLp 1)

noncomputable def Rockafellar.ex1Constraint₂ : TdafSurface.Rn 2 → EReal

The constraint f₂(ξ₁, ξ₂) = ξ₁² - ξ₂ of the counterexample.

Equations

• Rockafellar.ex1Constraint₂ x = ↑(x.ofLp 0 ^ 2 - x.ofLp 1)

noncomputable def Rockafellar.ex1 : OrdinaryConvexProgram 2 2

§28, first counterexample: the program with C = ℝ², f₀(ξ₁, ξ₂) = ξ₁, f₁(ξ₁, ξ₂) = ξ₂, f₂(ξ₁, ξ₂) = ξ₁² - ξ₂ and r = 2. Its only feasible solution, hence its unique optimal solution, is the origin and its optimal value is 0; but it has no Kuhn–Tucker vector (ex1_not_exists_isKuhnTuckerVector), because no point has f₁ ≤ 0 and f₂ < 0.

Equations

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

@[simp]

theorem Rockafellar.ex1_C : ex1.C = Set.univ

@[simp]

theorem Rockafellar.ex1_r : ex1.r = 2

@[simp]

theorem Rockafellar.ex1_f₀ (x : TdafSurface.Rn 2) : ex1.f₀ x = ↑(x.ofLp 0)

@[simp]

theorem Rockafellar.ex1_f_zero (x : TdafSurface.Rn 2) : ex1.f 0 x = ↑(x.ofLp 1)

@[simp]

theorem Rockafellar.ex1_f_one (x : TdafSurface.Rn 2) : ex1.f 1 x = ↑(x.ofLp 0 ^ 2 - x.ofLp 1)

theorem Rockafellar.ex1_feasibleSet : ex1.feasibleSet = {0}

The only point satisfying ξ₂ ≤ 0 and ξ₁² - ξ₂ ≤ 0 is the origin.

theorem Rockafellar.ex1_optimalValue : ex1.optimalValue = 0

theorem Rockafellar.ex1_optimalSolutions : ex1.optimalSolutions = {0}

§28: the program has (0, 0) as its unique optimal solution.

theorem Rockafellar.ex1_not_exists_isKuhnTuckerVector : ¬∃ (u : TdafSurface.Rn 2), ex1.IsKuhnTuckerVector u

§28: the program has no Kuhn–Tucker vector, although its optimal value is finite and its optimal solution is unique.

If (λ₁, λ₂) were one, then ξ₁ + λ₁ξ₂ + λ₂(ξ₁² - ξ₂) ≥ 0 for every (ξ₁, ξ₂). Taking ξ₁ = 0 and ξ₂ = λ₂ - λ₁ forces λ₁ = λ₂ =: λ; then ξ₁ = -1/(λ + 1), ξ₂ = 0 makes the left side -1/(λ + 1)² < 0.

A program with linear constraints and no Kuhn–Tucker vector

def Rockafellar.ex2Set : Set (TdafSurface.Rn 2)

The set C = {(ξ₁, ξ₂) | ξ₁² - ξ₂ ≤ 0} of the counterexample: a parabolic region whose relative interior misses the whole feasible set {ξ₂ = 0}.

Equations

• Rockafellar.ex2Set = {x : TdafSurface.Rn 2 | x.ofLp 0 ^ 2 - x.ofLp 1 ≤ 0}

theorem Rockafellar.mem_ex2Set {x : TdafSurface.Rn 2} : x ∈ ex2Set ↔ x.ofLp 0 ^ 2 - x.ofLp 1 ≤ 0

theorem Rockafellar.convex_ex2Set : Convex ℝ ex2Set

noncomputable def Rockafellar.ex2 : OrdinaryConvexProgram 2 1

§28, second counterexample: the program with C = {(ξ₁, ξ₂) | ξ₁² - ξ₂ ≤ 0}, f₀(ξ₁, ξ₂) = ξ₁, f₁(ξ₁, ξ₂) = ξ₂ and r = 0. f₀ is linear on C and the single constraint is the linear equation ξ₂ = 0, so every hypothesis of Corollary 28.2.2 holds except the relative-interior one: the feasible set is {0} and 0 ∉ ri C. Again (0, 0) is the unique optimal solution, 0 is the optimal value, and there is no Kuhn–Tucker vector (ex2_not_exists_isKuhnTuckerVector). This is what shows the relative-interior condition in Theorem 28.2 and Corollary 28.2.2 cannot be dropped.

Equations

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

@[simp]

theorem Rockafellar.ex2_C : ex2.C = ex2Set

@[simp]

theorem Rockafellar.ex2_r : ex2.r = 0

@[simp]

theorem Rockafellar.ex2_f (i : Fin 1) (x : TdafSurface.Rn 2) : ex2.f i x = ↑(x.ofLp 1)

theorem Rockafellar.ex2_f₀_of_mem {x : TdafSurface.Rn 2} (hx : x ∈ ex2Set) : ex2.f₀ x = ↑(x.ofLp 0)

theorem Rockafellar.ex2_feasibleSet : ex2.feasibleSet = {0}

The only point of C with ξ₂ = 0 is the origin.

theorem Rockafellar.ex2_optimalValue : ex2.optimalValue = 0

theorem Rockafellar.ex2_optimalSolutions : ex2.optimalSolutions = {0}

§28: (0, 0) is again the unique optimal solution.

theorem Rockafellar.ex2_not_exists_isKuhnTuckerVector : ¬∃ (u : TdafSurface.Rn 1), ex2.IsKuhnTuckerVector u

§28: the program has no Kuhn–Tucker vector, even though its objective is linear on C and its only constraint is a linear equation.

A Kuhn–Tucker vector would be a single λ₁ with 0 ≤ ξ₁ + λ₁ξ₂ for every (ξ₁, ξ₂) ∈ C. The points (-t, t²) lie in C for every t > 0, and there they give t ≤ λ₁t², i.e. λ₁t ≥ 1, which fails at t = 1/(|λ₁| + 1).