Lagrangians of generalized convex programs

The Lagrangian of the program associated with a bifunction F is L(v, x) = ⨅ u (⟨u, v⟩ + F u x), the partial concave conjugate of F in the perturbation variable. Identifying it as such is the design of this file: concavity of L(·, x), its closedness and the biconjugation L** = cl L are concave-conjugate lemmas applied pointwise in x. The one step with content is the exchange ⨅ x L(v, x) = ⨅ u (⟨u, v⟩ + inf F u), which turns the definition of a Kuhn–Tucker vector into a statement about L.

Main definitions

• lagrangian B F — the Lagrangian L of the program associated with F.

Main results

• lagrangian_eq_concaveConj — L(·, x) is the concave conjugate of -F(·)(x).
• iInf_lagrangian — ⨅ x L(v, x) = ⨅ u (⟨u, v⟩ + inf F u).
• mem_kuhnTucker_iff_iInf_lagrangian — v is a Kuhn–Tucker vector exactly when ⨅ x L(v, x) is finite and equal to the optimal value.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §29.

noncomputable def Tdaf.ConvexAnalysis.lagrangian {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 → X → EReal

The Lagrangian of the generalized convex program associated with F: L(v, x) = ⨅ u (⟨u, v⟩ + F u x).

Equations

• Tdaf.ConvexAnalysis.lagrangian B F v x = ⨅ (u : U), ↑((B u) v) + F u x

theorem Tdaf.ConvexAnalysis.lagrangian_apply {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) (x : X) : lagrangian B F v x = ⨅ (u : U), ↑((B u) v) + F u x

theorem Tdaf.ConvexAnalysis.lagrangian_eq_concaveConj {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) (x : X) : lagrangian B F v x = concaveConj B (fun (u : U) => -F u x) v

For each fixed x, L(·, x) is the concave conjugate of u ↦ -(F u x).

theorem Tdaf.ConvexAnalysis.lagrangian_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) (x : X) : lagrangian B F v x ≤ F 0 x

The Lagrangian is never above the objective it comes from, taken at u = 0.

theorem Tdaf.ConvexAnalysis.iInf_lagrangian {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) : ⨅ (x : X), lagrangian B F v x = ⨅ (u : U), ↑((B u) v) + infBifun F u

Minimising the Lagrangian over x is the same as pricing the perturbations: ⨅ x L(v, x) = ⨅ u (⟨u, v⟩ + inf F u).

theorem Tdaf.ConvexAnalysis.mem_kuhnTucker_iff_iInf_lagrangian {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 ≠ ⊥ ∧ ⨅ (x : X), lagrangian B F v x = infBifun F 0

The Lagrangian description of Kuhn–Tucker vectors: v is one exactly when ⨅ x L(v, x) is finite and equal to the optimal value.

theorem Tdaf.ConvexAnalysis.iInf_lagrangian_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) : ⨅ (x : X), lagrangian B F v x ≤ infBifun F 0

Weak duality: ⨅ x L(v, x) is never above the optimal value, whatever the price v.

theorem Tdaf.ConvexAnalysis.concaveFn_lagrangian {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) (x : X) : ConcaveFn fun (v : V) => lagrangian B F v x

The Lagrangian is concave in the price variable, with no hypothesis on F.