Normality of a dual pair of convex programs

A convex program (P) is normal when its perturbation function is closed at the origin,

(cl (inf F))(0) = (inf F)(0),

and this one condition turns out to be equivalent to the absence of a duality gap and to normality of the dual (P*). Ten sufficient conditions for it are collected below, and under normality the Kuhn–Tucker vectors of (P) are precisely the optimal solutions of (P*). Everything rests on Fenchel–Moreau at the origin, (cl f)(0) = ⨆ y, ⨅ x, (⟨x, y⟩ + f x): with f = inf F the inner infimum is the dual objective (F* 0)(y), so (cl (inf F))(0) = sup F* 0.

Main definitions

• Normal F — normality of the convex program associated with F.
• supBifun G, domConcaveBifun G, ConcaveConsistent G, ConcaveStronglyConsistent G, ConcaveNormal G, ConcaveKuhnTucker — the concave counterparts of infBifun, domBifun, Consistent, StronglyConsistent, Normal and KuhnTucker, each the convex notion at -G.

Main results

• clFn_infBifun_zero_eq_iSup_adjointBifun, clConcave_supBifun_adjointBifun_zero_eq — each optimal value is the other program's perturbation function closed at the origin; iSup_adjointBifun_eq_bot_iff and companions — inconsistency of one program as unboundedness of the other; liminf_infBifun_eq_iSup_adjointBifun — the same values as a liminf.
• normal_iff_iSup_adjointBifun_eq, concaveNormal_adjointBifun_iff, normal_iff_concaveNormal_adjointBifun — normality, absence of a duality gap and normality of the dual are one condition (Theorem 30.3 in [^1]).
• StronglyConsistent.normal, normal_of_concaveStronglyConsistent_adjointBifun, normal_of_kuhnTucker_nonempty, normal_of_exists_setOf_le and companions — ten sufficient conditions for normality (Theorem 30.4 in [^1], clauses (a)–(j)).
• mem_kuhnTucker_iff_adjointBifun_zero_eq_iSup, kuhnTucker_eq_setOf_isMax — the Kuhn–Tucker vectors are exactly the dual optimal solutions (Theorem 30.5 in [^1]), with mem_concaveKuhnTucker_adjointBifun_iff_mem_argmin for the dual assertion; exists_infBifun_eq_of_concaveStronglyConsistent — attainment of the primal infimum.

Implementation notes

The first formula for (cl (inf F))(0) needs only convexity of F, not closedness: it is Fenchel–Moreau for inf F, and the adjoint does not distinguish F from cl F. So normality and the absence of a duality gap agree for every convex bifunction, and only normality of the dual needs ClosedBifun F. A Kuhn–Tucker vector is made to imply normality through weak duality rather than through subgradients, so needs no finite dimension.

References

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

The closure of a convex function at the origin

theorem Tdaf.ConvexAnalysis.clFn_zero_eq_iSup_iInf {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {f : E → EReal} (hf : ConvexFn f) : clFn f 0 = ⨆ (y : F), ⨅ (x : E), ↑((B x) y) + f x

Fenchel–Moreau at the origin. For a convex f, the closure at 0 is the supremum over the dual variable of the infimum of x ↦ ⟨x, y⟩ + f x. Everything below rests on this computation.

Normality

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

A convex program is normal when its perturbation function is closed at the origin, (cl (inf F))(0) = (inf F)(0). When 0 ∈ cl (dom F) this is lower semicontinuity of u ↦ inf F u at u = 0.

Equations

• Tdaf.ConvexAnalysis.Normal F = (Tdaf.ConvexAnalysis.clFn (Tdaf.ConvexAnalysis.infBifun F) 0 = Tdaf.ConvexAnalysis.infBifun F 0)

theorem Tdaf.ConvexAnalysis.normal_iff {U : Type u_1} {X : Type u_2} [AddCommGroup U] [TopologicalSpace U] {F : Bifun U X} : Normal F ↔ clFn (infBifun F) 0 = infBifun F 0

The concave counterparts of the convex vocabulary

noncomputable def Tdaf.ConvexAnalysis.supBifun {V : Type u_1} {Y : Type u_2} (G : Bifun Y V) : Y → EReal

The optimal value of the concave program G y, as a function of the perturbation y: the mirror of infBifun. Rockafellar writes sup G.

Equations

• Tdaf.ConvexAnalysis.supBifun G y = ⨆ (v : V), G y v

theorem Tdaf.ConvexAnalysis.supBifun_apply {V : Type u_1} {Y : Type u_2} (G : Bifun Y V) (y : Y) : supBifun G y = ⨆ (v : V), G y v

def Tdaf.ConvexAnalysis.domConcaveBifun {V : Type u_1} {Y : Type u_2} (G : Bifun Y V) : Set Y

The mirror of domBifun: the perturbations for which the concave program is consistent.

Equations

• Tdaf.ConvexAnalysis.domConcaveBifun G = {y : Y | ∃ (v : V), G y v ≠ ⊥}

theorem Tdaf.ConvexAnalysis.mem_domConcaveBifun {V : Type u_1} {Y : Type u_2} {G : Bifun Y V} {y : Y} : y ∈ domConcaveBifun G ↔ ∃ (v : V), G y v ≠ ⊥

theorem Tdaf.ConvexAnalysis.neg_supBifun {V : Type u_1} {Y : Type u_2} (G : Bifun Y V) : (fun (y : Y) => -supBifun G y) = infBifun fun (y : Y) (v : V) => -G y v

Negating a concave bifunction turns its sup into the inf of the negation.

theorem Tdaf.ConvexAnalysis.domBifun_neg {V : Type u_1} {Y : Type u_2} (G : Bifun Y V) : (domBifun fun (y : Y) (v : V) => -G y v) = domConcaveBifun G

The effective domain of -G is the concave effective domain of G: -(G y v) ≠ ⊤ and G y v ≠ ⊥ are the same condition. This turns every consistency hypothesis about a concave program into the corresponding hypothesis about the convex program -G.

theorem Tdaf.ConvexAnalysis.domConcave_supBifun {V : Type u_1} {Y : Type u_2} (G : Bifun Y V) : domConcave (supBifun G) = domConcaveBifun G

The mirror of dom_infBifun.

def Tdaf.ConvexAnalysis.ConcaveConsistent {V : Type u_1} {Y : Type u_2} [AddCommGroup Y] (G : Bifun Y V) : Prop

The mirror of Consistent: the unperturbed concave program has a point where it is not -∞.

Equations

• Tdaf.ConvexAnalysis.ConcaveConsistent G = (0 ∈ Tdaf.ConvexAnalysis.domConcaveBifun G)

theorem Tdaf.ConvexAnalysis.concaveConsistent_iff {V : Type u_1} {Y : Type u_2} [AddCommGroup Y] {G : Bifun Y V} : ConcaveConsistent G ↔ ∃ (v : V), G 0 v ≠ ⊥

def Tdaf.ConvexAnalysis.ConcaveNormal {V : Type u_1} {Y : Type u_2} [AddCommGroup Y] [TopologicalSpace Y] (G : Bifun Y V) : Prop

The mirror of Normal for a concave program: (cl (sup G))(0) = (sup G)(0), the closure taken in the concave sense.

Equations

• Tdaf.ConvexAnalysis.ConcaveNormal G = (Tdaf.ConvexAnalysis.clConcave (Tdaf.ConvexAnalysis.supBifun G) 0 = Tdaf.ConvexAnalysis.supBifun G 0)

theorem Tdaf.ConvexAnalysis.concaveNormal_iff {V : Type u_1} {Y : Type u_2} [AddCommGroup Y] [TopologicalSpace Y] {G : Bifun Y V} : ConcaveNormal G ↔ clConcave (supBifun G) 0 = supBifun G 0

theorem Tdaf.ConvexAnalysis.concaveNormal_iff_normal_neg {V : Type u_1} {Y : Type u_2} [AddCommGroup Y] [TopologicalSpace Y] {G : Bifun Y V} : ConcaveNormal G ↔ Normal fun (y : Y) (v : V) => -G y v

Concave normality of G is ordinary normality of -G. This is what makes each concave sufficient condition free: it is the corresponding convex one read at -F*, pairings flipped.

def Tdaf.ConvexAnalysis.ConcaveStronglyConsistent {V : Type u_1} {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] (G : Bifun Y V) : Prop

The mirror of StronglyConsistent.

Equations

• Tdaf.ConvexAnalysis.ConcaveStronglyConsistent G = (0 ∈ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.domConcaveBifun G))

theorem Tdaf.ConvexAnalysis.ConcaveStronglyConsistent.concaveConsistent {V : Type u_1} {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] {G : Bifun Y V} (h : ConcaveStronglyConsistent G) : ConcaveConsistent G

theorem Tdaf.ConvexAnalysis.concaveStronglyConsistent_iff_stronglyConsistent_neg {V : Type u_1} {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] {G : Bifun Y V} : ConcaveStronglyConsistent G ↔ StronglyConsistent fun (y : Y) (v : V) => -G y v

Strong consistency of the concave program G is strong consistency of -G; this is what lets the concave consistency statements be read off the convex ones.

Concavity of the dual perturbation function

theorem Tdaf.ConvexAnalysis.concaveFn_supBifun {V : Type u_1} {Y : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] {G : Bifun Y V} (hG : ConcaveBifun G) : ConcaveFn (supBifun G)

The mirror of convexFn_infBifun: the optimal value of a concave program is a concave function of the perturbation.

The two optimal values

theorem Tdaf.ConvexAnalysis.clFn_infBifun_zero_eq_iSup_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) : clFn (infBifun F) 0 = ⨆ (v : V), adjointBifun Bu Bx F 0 v

The optimal value of the dual program: (cl (inf F))(0) = sup F* 0. Closedness of F is not needed — the formula is Fenchel–Moreau for inf F, and F* does not see the closure.

theorem Tdaf.ConvexAnalysis.normal_iff_iSup_adjointBifun_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) : Normal F ↔ ⨆ (v : V), adjointBifun Bu Bx F 0 v = infBifun F 0

Normality is exactly the absence of a duality gap: sup F* 0 = inf F 0.

theorem Tdaf.ConvexAnalysis.clConcave_supBifun_zero_eq_infBifun_concaveAdjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx.flip] {G : Bifun Y V} (hG : ConcaveBifun G) : clConcave (supBifun G) 0 = infBifun (concaveAdjointBifun Bu Bx G) 0

The dual of clFn_infBifun_zero_eq_iSup_adjointBifun: the concave closure of the dual perturbation function at the origin is the optimal value of the doubly-adjoint program.

Normality of (P), of (P*), and the absence of a duality gap

theorem Tdaf.ConvexAnalysis.clConcave_supBifun_adjointBifun_zero_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) : clConcave (supBifun (adjointBifun Bu Bx F)) 0 = infBifun F 0

The optimal value of the primal program: (cl (sup F*))(0) = inf F 0 for a closed convex bifunction. Closedness is what turns F** back into F.

theorem Tdaf.ConvexAnalysis.concaveNormal_adjointBifun_iff {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) : ConcaveNormal (adjointBifun Bu Bx F) ↔ ⨆ (v : V), adjointBifun Bu Bx F 0 v = infBifun F 0

The dual program is normal exactly when there is no duality gap.

theorem Tdaf.ConvexAnalysis.normal_iff_concaveNormal_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) : Normal F ↔ ConcaveNormal (adjointBifun Bu Bx F)

A closed convex program is normal exactly when its dual program is.

Sufficient conditions for normality

theorem Tdaf.ConvexAnalysis.normal_of_kuhnTucker_nonempty {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) (h : (KuhnTucker Bu F).Nonempty) : Normal F

If a Kuhn–Tucker vector exists then normality holds. Such a vector is a point at which the dual objective reaches inf F 0, and weak duality says it can never exceed it. (Finiteness of the optimal value is already part of KuhnTucker.)

theorem Tdaf.ConvexAnalysis.mem_kuhnTucker_iff_adjointBifun_zero_eq_iSup {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} {v : V} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) (hn : Normal F) (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : v ∈ KuhnTucker Bu F ↔ adjointBifun Bu Bx F 0 v = ⨆ (w : V), adjointBifun Bu Bx F 0 w

Under normality, and with the optimal value finite, the Kuhn–Tucker vectors of (P) are exactly the optimal solutions of (P*).

theorem Tdaf.ConvexAnalysis.kuhnTucker_eq_setOf_isMax {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) (hn : Normal F) (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : KuhnTucker Bu F = {v : V | adjointBifun Bu Bx F 0 v = ⨆ (w : V), adjointBifun Bu Bx F 0 w}

The same as an equation between sets: the Kuhn–Tucker set is the set of dual maximisers.

theorem Tdaf.ConvexAnalysis.isGreatest_adjointBifun_zero_of_mem_kuhnTucker {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} {v : V} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hv : v ∈ KuhnTucker Bu F) : IsGreatest (Set.range (adjointBifun Bu Bx F 0)) (infBifun F 0)

A Kuhn–Tucker vector is a dual optimal solution, with common optimal value inf F 0. This half needs no normality hypothesis — the vector's existence supplies it.

theorem Tdaf.ConvexAnalysis.StronglyConsistent.normal {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hs : StronglyConsistent F) (hF : ConvexBifun F) : Normal F

A strongly consistent convex program is normal: a convex function agrees with its closure throughout the relative interior of its effective domain, which here contains the origin.

theorem Tdaf.ConvexAnalysis.StrictlyConsistent.normal {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup X] [Module ℝ X] {F : Bifun U X} (hs : StrictlyConsistent F) (hF : ConvexBifun F) : Normal F

A strictly consistent convex program is normal.

Strong consistency of the dual program

theorem Tdaf.ConvexAnalysis.ConcaveStronglyConsistent.concaveNormal {V : Type u_1} {Y : Type u_2} [AddCommGroup V] [Module ℝ V] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {G : Bifun Y V} (hs : ConcaveStronglyConsistent G) (hG : ConcaveBifun G) : ConcaveNormal G

The concave mirror: a strongly consistent concave program is normal.

theorem Tdaf.ConvexAnalysis.normal_of_concaveStronglyConsistent_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hs : ConcaveStronglyConsistent (adjointBifun Bu Bx F)) : Normal F

If the dual program is strongly consistent then normality holds for the pair.

Bounded level sets and bounded sets of optimal solutions

noncomputable def Tdaf.ConvexAnalysis.shiftBifun {U : Type u_1} {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) (y : Y) : Bifun U X

F with a linear function of x subtracted off; its optimal value at u is -(F u)*(y), so the dual-value formula applied to it computes the whole y-slice sup (F* y) of the adjoint.

Equations

• Tdaf.ConvexAnalysis.shiftBifun Bx F y u x = F u x - ↑((Bx x) y)

@[simp]

theorem Tdaf.ConvexAnalysis.shiftBifun_apply {U : Type u_1} {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) (y : Y) (u : U) (x : X) : shiftBifun Bx F y u x = F u x - ↑((Bx x) y)

theorem Tdaf.ConvexAnalysis.infBifun_shiftBifun {U : Type u_1} {X : Type u_3} {Y : Type u_4} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) (y : Y) (u : U) : infBifun (shiftBifun Bx F y) u = -conj Bx (F u) y

The optimal value of the shifted program is the conjugate of the slice, negated.

theorem Tdaf.ConvexAnalysis.convexBifun_shiftBifun {U : Type u_1} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {F : Bifun U X} (hF : ConvexBifun F) (y : Y) : ConvexBifun (shiftBifun Bx F y)

Subtracting a linear function of x keeps a convex bifunction convex.

theorem Tdaf.ConvexAnalysis.adjointBifun_shiftBifun_zero {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (F : Bifun U X) (y : Y) (v : V) : adjointBifun Bu Bx (shiftBifun Bx F y) 0 v = adjointBifun Bu Bx F y v

Shifting by y and reading the adjoint at the origin is the adjoint at y.

theorem Tdaf.ConvexAnalysis.supBifun_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [AddCommGroup V] [Module ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {F : Bifun U X} (hF : ConvexBifun F) (y : Y) : supBifun (adjointBifun Bu Bx F) y = clFn (infBifun (shiftBifun Bx F y)) 0

The dual objective at an arbitrary y: the supremum defining it is the closure, at the origin, of the optimal value of the shifted program.

theorem Tdaf.ConvexAnalysis.mem_domConcaveBifun_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} {F : Bifun U X} {y : Y} (hF : ConvexBifun F) (hc : Consistent F) (h : ∀ (u : U), conj Bx (F u) y ≠ ⊤) : y ∈ domConcaveBifun (adjointBifun Bu Bx F)

If the perturbed objective F u - ⟨·, y⟩ is bounded below for every perturbation u, then y belongs to the effective domain of the dual program.

domConcaveBifun F* asks for sup (F* y) ≠ -∞, which is cl (inf (F - ⟨·, y⟩)) 0 ≠ -∞, strictly stronger than the inf (F - ⟨·, y⟩) 0 ≠ -∞ that y ∈ dom ((F 0)*) says. What bridges them is that a proper convex function has a proper closure. This is the one statement here needing FiniteDimensional ℝ U.

theorem Tdaf.ConvexAnalysis.normal_of_exists_setOf_le {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (h : ∃ (α : ℝ), {x : X | F 0 x ≤ ↑α}.Nonempty ∧ Bornology.IsBounded {x : X | F 0 x ≤ ↑α}) : Normal F

If some level set {x | (F 0)(x) ≤ α} is non-empty and bounded, then normality holds for (P) and (P*).

A bounded level set gives 0 ∈ int (dom ((F 0)*)), but strict consistency of (P*) is 0 ∈ int (domConcaveBifun F*), an intersection over all perturbations u of the sets dom ((F u)*), and openness of an intersection is not automatic. What makes it open is that all slices of a closed convex bifunction have the same recession function, so every int (dom ((F u)*)) is described by the same inequality and they are all equal. No properness is assumed: an improper closed convex bifunction has inf F 0 = -∞, where normality is trivial.

theorem Tdaf.ConvexAnalysis.normal_of_argmin_nonempty_and_isBounded {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hp : Proper (F 0)) (hne : (argmin (F 0)).Nonempty) (hbd : Bornology.IsBounded (argmin (F 0))) : Normal F

If the optimal solutions to (P) form a non-empty bounded set — in particular if there is exactly one — then normality holds. With F 0 proper this is the level-set criterion, since argmin (F 0) is then a level set at the minimum value. Properness is not removable: for F 0 ≡ ⊤ over a zero-dimensional X the optimal solutions are non-empty and bounded while no level set is.

Bounded level sets of the dual objective

theorem Tdaf.ConvexAnalysis.normal_of_exists_setOf_ge_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (h : ∃ (α : ℝ), {v : V | ↑α ≤ adjointBifun Bu Bx F 0 v}.Nonempty ∧ Bornology.IsBounded {v : V | ↑α ≤ adjointBifun Bu Bx F 0 v}) : Normal F

If some superlevel set {v | α ≤ (F* 0)(v)} of the dual objective is non-empty and bounded, then normality holds for (P) and (P*).

This is the level-set criterion read for the convex program associated with -F*, which is convex and closed with no hypothesis on F: its objective is -(F* 0) and its sublevel set at -α is the superlevel set of F* 0 at α. Normality of that program is concave normality of F*, hence normality of (P). Going this way needs no concave mirror of the level-set and recession machinery on V.

theorem Tdaf.ConvexAnalysis.normal_of_argmax_adjointBifun_nonempty_and_isBounded {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] [IsCompatiblePairing Bu.flip] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hp : Proper fun (v : V) => -adjointBifun Bu Bx F 0 v) (hne : (argmax (adjointBifun Bu Bx F 0)).Nonempty) (hbd : Bornology.IsBounded (argmax (adjointBifun Bu Bx F 0))) : Normal F

If the optimal solutions to (P*) form a non-empty bounded set — in particular if there is exactly one — then normality holds. The bounded-argmin criterion read for the convex program associated with -F*; properness of the objective is not removable there either.

Consistency of the two programs

theorem Tdaf.ConvexAnalysis.forall_conj_eq_top_iff {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup G] [Module ℝ G] {B : E →ₗ[ℝ] G →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {f : E → EReal} (hf : ConvexFn f) : (∀ (y : G), conj B f y = ⊤) ↔ ∃ (x : E), f x = ⊥

A dichotomy for conjugates: the conjugate of a convex function is identically ⊤ exactly when the function takes the value ⊥ somewhere. One direction is free; the other uses that a proper convex function has a proper closure, whose conjugate is proper, and (cl f)* = f*.

theorem Tdaf.ConvexAnalysis.neg_adjointBifun_zero_apply {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (v : V) : -adjointBifun Bu Bx F 0 v = conj Bu (infBifun F) (-v)

The dual objective, negated, is the conjugate of the perturbation function at the reflected point: -(F* 0)(v) = (inf F)*(-v).

theorem Tdaf.ConvexAnalysis.adjointBifun_zero_eq_bot_iff {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (v : V) : adjointBifun Bu Bx F 0 v = ⊥ ↔ conj Bu (infBifun F) (-v) = ⊤

The dual objective is -∞ at v exactly when the conjugate of the perturbation function is +∞ at -v.

theorem Tdaf.ConvexAnalysis.not_concaveConsistent_adjointBifun_iff {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) : ¬ConcaveConsistent (adjointBifun Bu Bx F) ↔ ∃ (u : U), infBifun F u = ⊥

Inconsistency of the dual: (P*) is inconsistent exactly when some perturbation of (P) is unbounded below. Closedness of F is not needed, because F* never sees the difference between F and cl F.

theorem Tdaf.ConvexAnalysis.concaveConsistent_adjointBifun_iff {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) : ConcaveConsistent (adjointBifun Bu Bx F) ↔ ∀ (u : U), infBifun F u ≠ ⊥

The positive form: (P*) is consistent exactly when no perturbation of (P) is unbounded below.

The objective of the doubly-adjoint program

Three algebraic facts about G* 0 for a concave G. They carried the whole instance context of the consistency section with an omit list per declaration; none of them uses any of it, so they sit in their own section at the weakest layer instead.

theorem Tdaf.ConvexAnalysis.concaveAdjointBifun_zero_apply {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (G : Bifun Y V) (x : X) : concaveAdjointBifun Bu Bx G 0 x = ⨆ (y : Y), ↑((Bx x) y) + supBifun G y

The mirror of adjointBifun_zero_apply: the objective of the program associated with the concave adjoint is (G* 0)(x) = ⨆ y (⟨x, y⟩ + sup G y).

theorem Tdaf.ConvexAnalysis.concaveAdjointBifun_zero_eq_conj {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (G : Bifun Y V) : concaveAdjointBifun Bu Bx G 0 = conj Bx.flip fun (y : Y) => -supBifun G y

The doubly-adjoint objective is the conjugate of -sup G: (-sup G)* = G* 0.

theorem Tdaf.ConvexAnalysis.convexFn_neg_supBifun {V : Type u_2} {Y : Type u_4} [AddCommGroup V] [Module ℝ V] [AddCommGroup Y] [Module ℝ Y] {G : Bifun Y V} (hG : ConcaveBifun G) : ConvexFn fun (y : Y) => -supBifun G y

-sup G is convex when G is a concave bifunction: it is inf (-G).

theorem Tdaf.ConvexAnalysis.not_consistent_iff_exists_supBifun_eq_top {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) : ¬Consistent F ↔ ∃ (y : Y), supBifun (adjointBifun Bu Bx F) y = ⊤

Inconsistency of the primal: (P) is inconsistent exactly when some perturbation of (P*) is unbounded above. Unlike the dual half this does need F closed: it is that half read for the dual pair, and F** = F identifies the objective of (P).

theorem Tdaf.ConvexAnalysis.consistent_iff_forall_supBifun_ne_top {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) : Consistent F ↔ ∀ (y : Y), supBifun (adjointBifun Bu Bx F) y ≠ ⊤

The positive form: (P) is consistent exactly when no perturbation of (P*) is unbounded above.

Kuhn–Tucker vectors of the dual program

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

Kuhn–Tucker vectors for a concave program, the mirror of KuhnTucker: the x for which ⨆ y (⟨y, x⟩ + sup G y) is finite and equal to the optimal value sup G 0.

Equations

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

theorem Tdaf.ConvexAnalysis.mem_concaveKuhnTucker_iff_neg_mem_kuhnTucker {V : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] {B : Y →ₗ[ℝ] X →ₗ[ℝ] ℝ} {G : Bifun Y V} {x : X} : x ∈ ConcaveKuhnTucker B G ↔ -x ∈ KuhnTucker B fun (y : Y) (v : V) => -G y v

The concave mirror is the reflection of the convex notion: x is a Kuhn–Tucker vector of the concave program G exactly when -x is one of the convex program -G.

theorem Tdaf.ConvexAnalysis.concaveNormal_of_concaveKuhnTucker_nonempty {V : Type u_1} {X : Type u_2} {Y : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {B : Y →ₗ[ℝ] X →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {G : Bifun Y V} (hG : ConcaveBifun G) (h : (ConcaveKuhnTucker B G).Nonempty) : ConcaveNormal G

The concave mirror: a concave program possessing a Kuhn–Tucker vector is normal. Such a vector is a supergradient of sup G at the origin, and a convex function agrees with its closure wherever it is subdifferentiable.

theorem Tdaf.ConvexAnalysis.normal_of_concaveKuhnTucker_adjointBifun_nonempty {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (h : (ConcaveKuhnTucker Bx.flip (adjointBifun Bu Bx F)).Nonempty) : Normal F

If the dual program has a Kuhn–Tucker vector (its optimal value being finite, which is part of ConcaveKuhnTucker), then normality holds for the pair.

Polyhedral programs

theorem Tdaf.ConvexAnalysis.PolyhedralBifun.normal {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {F : Bifun U X} (hF : PolyhedralBifun F) (hc : Consistent F) : Normal F

A polyhedral convex program that is merely consistent is normal: inf F is then polyhedral, and a polyhedral convex function agrees with its closure throughout its effective domain, which consistency places the origin in.

def Tdaf.ConvexAnalysis.ConcavePolyhedralBifun {V : Type u_1} {Y : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (G : Bifun Y V) : Prop

A concave bifunction is polyhedral when its negative is: the mirror of PolyhedralBifun.

Equations

• Tdaf.ConvexAnalysis.ConcavePolyhedralBifun G = Tdaf.ConvexAnalysis.PolyhedralBifun fun (y : Y) (v : V) => -G y v

theorem Tdaf.ConvexAnalysis.ConcavePolyhedralBifun.concaveNormal {V : Type u_1} {Y : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {G : Bifun Y V} (hG : ConcavePolyhedralBifun G) (hc : ConcaveConsistent G) : ConcaveNormal G

The concave mirror: a consistent polyhedral concave program is normal.

theorem Tdaf.ConvexAnalysis.normal_of_concavePolyhedral_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup X] [Module ℝ X] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hG : ConcavePolyhedralBifun (adjointBifun Bu Bx F)) (hc : ConcaveConsistent (adjointBifun Bu Bx F)) : Normal F

If the dual program is polyhedral and consistent then normality holds for the pair.

The two optimal values as a liminf and a limsup

theorem Tdaf.ConvexAnalysis.le_limsup_nhds {E : Type u_1} [TopologicalSpace E] (g : E → EReal) (x : E) : g x ≤ Filter.limsup g (nhds x)

The mirror of liminf_nhds_le: a function is at most its own limsup along the neighbourhood filter.

theorem Tdaf.ConvexAnalysis.clConcave_eq_limsup_or {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {g : E → EReal} (hg : ConcaveFn g) (x : E) : clConcave g x = Filter.limsup g (nhds x) ∨ clConcave g x = ⊤ ∧ Filter.limsup g (nhds x) = ⊥

The concave mirror of clFn_eq_liminf_or: for concave g the concave closure at x is the limsup of g at x, except when the left side is +∞ and the right -∞.

theorem Tdaf.ConvexAnalysis.liminf_infBifun_eq_iSup_adjointBifun {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {F : Bifun U X} (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (hF : ConvexBifun F) (h : Consistent F ∨ ConcaveConsistent (adjointBifun Bu Bx F)) : Filter.liminf (infBifun F) (nhds 0) = ⨆ (v : V), adjointBifun Bu Bx F 0 v

Unless both programs are inconsistent, liminf_{u → 0} (inf F u) = sup F* 0. The exception is unavoidable: cl (inf F) and liminf (inf F) can differ only when the first is -∞, i.e. the dual is inconsistent, and the second is +∞, which forces inf F 0 = +∞.

theorem Tdaf.ConvexAnalysis.limsup_supBifun_adjointBifun_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul ℝ Y] [LocallyConvexSpace ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (h : Consistent F ∨ ConcaveConsistent (adjointBifun Bu Bx F)) : Filter.limsup (supBifun (adjointBifun Bu Bx F)) (nhds 0) = infBifun F 0

Dually: unless both programs are inconsistent, limsup_{y → 0} (sup F* y) = inf F 0.

The dual assertion, and attainment of the primal infimum

The dual counterpart of "the Kuhn–Tucker vectors are the dual optimal solutions" comes last because it needs both the concave Kuhn–Tucker vocabulary and the second-adjoint computation concaveAdjointBifun_zero_apply introduced for the consistency criteria.

theorem Tdaf.ConvexAnalysis.mem_concaveKuhnTucker_iff_concaveAdjointBifun_zero_eq {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (G : Bifun Y V) (x : X) : x ∈ ConcaveKuhnTucker Bx.flip G ↔ supBifun G 0 ≠ ⊤ ∧ supBifun G 0 ≠ ⊥ ∧ concaveAdjointBifun Bu Bx G 0 x = supBifun G 0

The concave mirror of mem_kuhnTucker_iff_adjointBifun_zero_eq: x is a Kuhn–Tucker vector of the concave program G exactly when sup G 0 is finite and the objective of the doubly-adjoint program attains it at x. Note that ConcaveKuhnTucker pairs with Bx.flip where the adjoint pairs with Bx.

theorem Tdaf.ConvexAnalysis.mem_concaveKuhnTucker_adjointBifun_iff_mem_argmin {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul ℝ X] [LocallyConvexSpace ℝ X] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] {F : Bifun U X} {x : X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hn : Normal F) (ht : infBifun F 0 ≠ ⊤) (hb : infBifun F 0 ≠ ⊥) : x ∈ ConcaveKuhnTucker Bx.flip (adjointBifun Bu Bx F) ↔ x ∈ argmin (F 0)

The dual assertion: under normality, x is a Kuhn–Tucker vector for (P*) exactly when it is an optimal solution to (P). The defining supremum of a concave Kuhn–Tucker vector is the objective of the doubly-adjoint program, and F** = F turns that into (F 0)(x); normality identifies the two optimal values.

theorem Tdaf.ConvexAnalysis.exists_infBifun_eq_of_concaveStronglyConsistent {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [TopologicalSpace U] [IsTopologicalAddGroup U] [ContinuousSMul ℝ U] [LocallyConvexSpace ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] {Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ} [IsCompatiblePairing Bu] {Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ} [IsCompatiblePairing Bx] [IsCompatiblePairing Bx.flip] {F : Bifun U X} (hF : ConvexBifun F) (hcl : ClosedBifun F) (hc : Consistent F) (hbot : infBifun F 0 ≠ ⊥) (hs : ConcaveStronglyConsistent (adjointBifun Bu Bx F)) : ∃ (x : X), F 0 x = infBifun F 0

Attainment of the primal infimum: if (P) is consistent and (P*) is strongly consistent, the infimum of (P) is attained.

The route is through the convex program associated with -F*: that is a convex bifunction with no hypothesis on F, strong consistency of (P*) is strong consistency of it, and its perturbation function -sup F* is proper because the optimal values are finite. Strong consistency then produces a Kuhn–Tucker vector for -F*, which the dual assertion above turns into a minimiser of F 0.