Rockafellar, §33: Saddle-Functions

Concave-convex and convex-concave functions on ℝᵐ × ℝⁿ, the partial closures cl₁ and cl₂, and the correspondence — "at the heart of the theory of saddle-functions" — between saddle-functions and convex bifunctions from ℝᵐ to ℝⁿ. All eleven numbered results of §33 are formalized: Theorems 33.1–33.3 and Corollaries 33.1.1, 33.1.2, 33.1.3, 33.2.1, 33.2.2, 33.3.1, 33.3.2, 33.3.3.

Orientation. A concave-convex K (u, v) is concave in the first argument and convex in the second, and the two closures are named after the argument they close, not the sense in which they close it: cl₁ closes the first — concave — argument concavely, cl₂ the second — convex — argument convexly. So K is lower closed when cl₂ (cl₁ K) = K and upper closed when cl₁ (cl₂ K) = K. Reversing any of this silently swaps every statement of §§34–37. A convex-concave K is reached by negation; see convexConcave_lowerClosed_iff.

Implementation notes

Rockafellar overloads ⟨·, ·⟩ for the conjugate of a convex f, of a concave f, and of a slice of a convex or a concave bifunction; these are separate names here. The bifunction brackets are uncurried, as functions of the pair (u, x*), the form every closedness predicate is stated against.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §33, pp. 349–358.

The two partial closures

@[reducible, inline]

noncomputable abbrev Rockafellar.cl₂ {m n : ℕ} (K : TdafSurface.Rn m × TdafSurface.Rn n → EReal) : TdafSurface.Rn m × TdafSurface.Rn n → EReal

Rockafellar's cl₂ K = cl_v K, the convex closure: close K (u, ·) as a convex function of the second argument, for each fixed u. An abbrev for partialCl₂.

Equations

• Rockafellar.cl₂ K = Tdaf.ConvexAnalysis.partialCl₂ K

@[reducible, inline]

noncomputable abbrev Rockafellar.cl₁ {m n : ℕ} (K : TdafSurface.Rn m × TdafSurface.Rn n → EReal) : TdafSurface.Rn m × TdafSurface.Rn n → EReal

Rockafellar's cl₁ K = cl_u K, the concave closure: close K (·, v) as a concave function of the first argument. An abbrev for partialCl₁; it is cl₂ conjugated by negation, not cl₂ with the arguments exchanged.

Equations

• Rockafellar.cl₁ K = Tdaf.ConvexAnalysis.partialCl₁ K

The three brackets

@[reducible, inline]

noncomputable abbrev Rockafellar.conjBracket {n : ℕ} (f : TdafSurface.Rn n → EReal) : TdafSurface.Rn n → EReal

Rockafellar's ⟨f, x*⟩ = f*(x*) for a convex f: the conjugate, as an inner product.

Equations

• Rockafellar.conjBracket f = Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f

@[reducible, inline]

noncomputable abbrev Rockafellar.concaveConjBracket {n : ℕ} (f : TdafSurface.Rn n → EReal) : TdafSurface.Rn n → EReal

Rockafellar's ⟨f, x*⟩ for a concave f: the concave conjugate.

Equations

• Rockafellar.concaveConjBracket f = Tdaf.ConvexAnalysis.concaveConj (TdafSurface.pairing n) f

@[reducible, inline]

noncomputable abbrev Rockafellar.bifunBracket {m n : ℕ} (F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)) : TdafSurface.Rn m × TdafSurface.Rn n → EReal

Rockafellar's ⟨Fu, x*⟩ = (Fu)*(x*) for a convex bifunction F, as a function of the pair (u, x*). This is the K̲ of Corollary 33.3.1.

Equations

• Rockafellar.bifunBracket F = Tdaf.ConvexAnalysis.saddleOfBifun (TdafSurface.pairing n) F

@[reducible, inline]

noncomputable abbrev Rockafellar.concaveBifunBracket {m n : ℕ} (G : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn n) (TdafSurface.Rn m)) : TdafSurface.Rn m × TdafSurface.Rn n → EReal

Rockafellar's ⟨u, Gx*⟩ = (Gx*)*(u) for a concave bifunction G from ℝⁿ to ℝᵐ.

Equations

• Rockafellar.concaveBifunBracket G p = Tdaf.ConvexAnalysis.concaveBracket (TdafSurface.pairing m) G p.1 p.2

@[reducible, inline]

noncomputable abbrev Rockafellar.adjointBracket {m n : ℕ} (F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)) : TdafSurface.Rn m × TdafSurface.Rn n → EReal

Rockafellar's ⟨u, F*x*⟩, the concave bracket of the adjoint F* (§30, dualProgram); the K̄ of Corollary 33.3.1.

Equations

• Rockafellar.adjointBracket F = Rockafellar.concaveBifunBracket (Rockafellar.dualProgram F)

@[reducible, inline]

noncomputable abbrev Rockafellar.bifunOfSaddleFn {m n : ℕ} (K : TdafSurface.Rn m × TdafSurface.Rn n → EReal) : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)

The convex bifunction attached to a saddle-function, Fu = K (u, ·)*: the inverse map of Corollaries 33.1.2 and 33.3.2.

Equations

• Rockafellar.bifunOfSaddleFn K = Tdaf.ConvexAnalysis.bifunOfSaddle (TdafSurface.pairing n) K

theorem Rockafellar.bifunBracket_apply {m n : ℕ} (F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)) (p : TdafSurface.Rn m × TdafSurface.Rn n) : bifunBracket F p = ⨆ (x : TdafSurface.Rn n), ↑(((TdafSurface.pairing n) x) p.2) - F p.1 x

The book's defining formula: ⟨Fu, x*⟩ = sup_x {⟨x, x*⟩ - (Fu)(x)}.

theorem Rockafellar.concaveBifunBracket_apply {m n : ℕ} (G : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn n) (TdafSurface.Rn m)) (p : TdafSurface.Rn m × TdafSurface.Rn n) : concaveBifunBracket G p = ⨅ (v : TdafSurface.Rn m), ↑(((TdafSurface.pairing m) p.1) v) - G p.2 v

The book's defining formula: ⟨u, Gx*⟩ = inf_v {⟨u, v⟩ - (Gx*)(v)}.

theorem Rockafellar.bifunOfSaddleFn_apply {m n : ℕ} (K : TdafSurface.Rn m × TdafSurface.Rn n → EReal) (u : TdafSurface.Rn m) (x : TdafSurface.Rn n) : bifunOfSaddleFn K u x = ⨆ (y : TdafSurface.Rn n), ↑(((TdafSurface.pairing n) x) y) - K (u, y)

The book's defining formula for Fu = K (u, ·)*.

theorem Rockafellar.conjBracket_indicatorFn {n : ℕ} (x y : TdafSurface.Rn n) : conjBracket (Tdaf.ConvexAnalysis.indicatorFn {x}) y = ↑(((TdafSurface.pairing n) x) y)

⟨f, x*⟩ = ⟨x, x*⟩ when f is the indicator of x: the notation extends the ordinary inner product along the embedding of ℝⁿ into the convex functions.

Theorem 33.1

theorem Rockafellar.theorem_33_1_concaveConvex {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.ConvexBifun F) : Tdaf.ConvexAnalysis.ConcaveConvexFn (bifunBracket F)

Theorem 33.1, first clause: for a convex bifunction F, ⟨Fu, x*⟩ is concave-convex in (u, x*). Concavity in u is Theorem 5.7 for the image of the graph function.

theorem Rockafellar.theorem_33_1_convexClosed {m n : ℕ} (F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)) : Tdaf.ConvexAnalysis.ConvexClosedFn (bifunBracket F)

Theorem 33.1, second clause: ⟨Fu, x*⟩ is convex-closed, with no hypothesis on F whatever — each slice is a conjugate.

theorem Rockafellar.theorem_33_1_inversion {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.ConvexBifun F) (u : TdafSurface.Rn m) (x : TdafSurface.Rn n) : Tdaf.ConvexAnalysis.clFn (F u) x = ⨆ (y : TdafSurface.Rn n), ↑(((TdafSurface.pairing n) x) y) - bifunBracket F (u, y)

Theorem 33.1, the inversion formula: Fenchel–Moreau (Theorem 12.2) uniformly in u.

theorem Rockafellar.theorem_33_1_convexBifun {m n : ℕ} {K : TdafSurface.Rn m × TdafSurface.Rn n → EReal} (hK : Tdaf.ConvexAnalysis.ConcaveConvexFn K) : Tdaf.ConvexAnalysis.ConvexBifun (bifunOfSaddleFn K)

Theorem 33.1, converse: for a concave-convex K, the bifunction Fu = K (u, ·)* is convex.

theorem Rockafellar.theorem_33_1_imageClosed {m n : ℕ} (K : TdafSurface.Rn m × TdafSurface.Rn n → EReal) : Tdaf.ConvexAnalysis.ImageClosedBifun (bifunOfSaddleFn K)

Theorem 33.1, converse: that bifunction is image-closed, each Fu being a conjugate.

theorem Rockafellar.theorem_33_1_bracket_eq {m n : ℕ} {K : TdafSurface.Rn m × TdafSurface.Rn n → EReal} (hK : Tdaf.ConvexAnalysis.ConcaveConvexFn K) : bifunBracket (bifunOfSaddleFn K) = cl₂ K

Theorem 33.1, converse, the identity that closes the loop: ⟨Fu, x*⟩ = (cl₂ K)(u, x*), with cl₂ the closure in the convex — second — argument.

Corollary 33.1.1

theorem Rockafellar.corollary_33_1_1_cl₁_concaveConvex {m n : ℕ} {K : TdafSurface.Rn m × TdafSurface.Rn n → EReal} (hK : Tdaf.ConvexAnalysis.ConcaveConvexFn K) : Tdaf.ConvexAnalysis.ConcaveConvexFn (cl₁ K)

Corollary 33.1.1: cl₁ K is again concave-convex.

theorem Rockafellar.corollary_33_1_1_cl₂_concaveConvex {m n : ℕ} {K : TdafSurface.Rn m × TdafSurface.Rn n → EReal} (hK : Tdaf.ConvexAnalysis.ConcaveConvexFn K) : Tdaf.ConvexAnalysis.ConcaveConvexFn (cl₂ K)

Corollary 33.1.1: cl₂ K is again concave-convex.

theorem Rockafellar.corollary_33_1_1_cl₁_concaveClosed {m n : ℕ} (K : TdafSurface.Rn m × TdafSurface.Rn n → EReal) : Tdaf.ConvexAnalysis.ConcaveClosedFn (cl₁ K)

Corollary 33.1.1: cl₁ K is concave-closed; the concave closure is idempotent.

theorem Rockafellar.corollary_33_1_1_cl₂_convexClosed {m n : ℕ} (K : TdafSurface.Rn m × TdafSurface.Rn n → EReal) : Tdaf.ConvexAnalysis.ConvexClosedFn (cl₂ K)

Corollary 33.1.1: cl₂ K is convex-closed.

Corollary 33.1.2

theorem Rockafellar.imageClosedBifun_of_closedBifun {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.ClosedBifun F) : Tdaf.ConvexAnalysis.ImageClosedBifun F

A closed bifunction is image-closed: a slice of a closed function is closed.

noncomputable def Rockafellar.corollary_33_1_2 {m n : ℕ} : { F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n) // Tdaf.ConvexAnalysis.ConvexBifun F ∧ Tdaf.ConvexAnalysis.ImageClosedBifun F } ≃ { K : TdafSurface.Rn m × TdafSurface.Rn n → EReal // Tdaf.ConvexAnalysis.ConcaveConvexFn K ∧ Tdaf.ConvexAnalysis.ConvexClosedFn K }

Corollary 33.1.2. The relations K (u, x*) = ⟨Fu, x*⟩ and Fu = K (u, ·)* are a one-to-one correspondence between the convex-closed concave-convex functions on ℝᵐ × ℝⁿ and the image-closed convex bifunctions from ℝᵐ to ℝⁿ.

Equations

• Rockafellar.corollary_33_1_2 = Tdaf.ConvexAnalysis.bifunSaddleEquiv

theorem Rockafellar.corollary_33_1_2_apply {m n : ℕ} (F : { F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n) // Tdaf.ConvexAnalysis.ConvexBifun F ∧ Tdaf.ConvexAnalysis.ImageClosedBifun F }) : ↑(corollary_33_1_2 F) = bifunBracket ↑F

The forward relation of Corollary 33.1.2 is K (u, x*) = ⟨Fu, x*⟩.

theorem Rockafellar.corollary_33_1_2_symm_apply {m n : ℕ} (K : { K : TdafSurface.Rn m × TdafSurface.Rn n → EReal // Tdaf.ConvexAnalysis.ConcaveConvexFn K ∧ Tdaf.ConvexAnalysis.ConvexClosedFn K }) : ↑(corollary_33_1_2.symm K) = bifunOfSaddleFn ↑K

The inverse relation of Corollary 33.1.2 is Fu = K (u, ·)*.

Corollary 33.1.3

theorem Rockafellar.corollary_33_1_3_convex {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.PolyhedralBifun F) (u : TdafSurface.Rn m) : Tdaf.ConvexAnalysis.PolyhedralFn fun (y : TdafSurface.Rn n) => bifunBracket F (u, y)

Corollary 33.1.3: for a polyhedral convex bifunction F, ⟨Fu, x*⟩ is polyhedral convex in x* for each u.

theorem Rockafellar.corollary_33_1_3_concave {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.PolyhedralBifun F) (y : TdafSurface.Rn n) : Tdaf.ConvexAnalysis.PolyhedralFn fun (u : TdafSurface.Rn m) => -bifunBracket F (u, y)

Corollary 33.1.3: ⟨Fu, x*⟩ is polyhedral concave in u for each x*.

theorem Rockafellar.corollary_33_1_3_inversion {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.PolyhedralBifun F) (hp : Tdaf.ConvexAnalysis.Proper (Tdaf.ConvexAnalysis.graphFn F)) (u : TdafSurface.Rn m) (x : TdafSurface.Rn n) : F u x = ⨆ (y : TdafSurface.Rn n), ↑(((TdafSurface.pairing n) x) y) - bifunBracket F (u, y)

Corollary 33.1.3: a proper polyhedral convex bifunction is recovered from its bracket with no closure operation, being already closed.

The adjoint bracket

theorem Rockafellar.adjointBracket_concaveConvex {m n : ℕ} (F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)) : Tdaf.ConvexAnalysis.ConcaveConvexFn (adjointBracket F)

⟨u, F*x*⟩ is concave-convex in (u, x*), with no hypothesis on F: the adjoint of any bifunction is concave.

theorem Rockafellar.adjointBracket_concaveClosed {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.ConvexBifun F) : Tdaf.ConvexAnalysis.ConcaveClosedFn (adjointBracket F)

⟨u, F*x*⟩ is concave-closed: it is a cl₁ by Theorem 33.2, and every cl₁ is concave-closed by Corollary 33.1.1.

Theorem 33.2

theorem Rockafellar.theorem_33_2_first {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.ConvexBifun F) : adjointBracket F = cl₁ (bifunBracket F)

Theorem 33.2, first equation: ⟨u, F*x*⟩ = cl₁ ⟨Fu, x*⟩, the closure in the concave — first — argument. It is concave Fenchel–Moreau in u.

theorem Rockafellar.theorem_33_2_second {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.ConvexBifun F) : cl₂ (adjointBracket F) = bifunBracket (Tdaf.ConvexAnalysis.clBifun F)

Theorem 33.2, second equation: cl₂ ⟨u, F*x*⟩ = ⟨(cl F)u, x*⟩, the closure in the convex — second — argument. It is the first equation at F* composed with Theorem 30.1's F** = cl F.

Corollary 33.2.1

theorem Rockafellar.corollary_33_2_1_primal {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.ConvexBifun F) {u : TdafSurface.Rn m} (hu : u ∈ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.domBifun F)) (y : TdafSurface.Rn n) : bifunBracket F (u, y) = adjointBracket F (u, y)

Corollary 33.2.1, first assertion: if u ∈ ri (dom F) then ⟨Fu, x*⟩ = ⟨u, F*x*⟩ for every x*. The two differ by cl₁, which Theorem 7.4 removes on ri (dom).

theorem Rockafellar.corollary_33_2_1_dual {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.ConvexBifun F) (hcl : Tdaf.ConvexAnalysis.ClosedBifun F) (u : TdafSurface.Rn m) {y : TdafSurface.Rn n} (hy : y ∈ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.domConcaveBifun (dualProgram F))) : bifunBracket F (u, y) = adjointBracket F (u, y)

Corollary 33.2.1, second assertion: if F is closed and x* ∈ ri (dom F*) then ⟨Fu, x*⟩ = ⟨u, F*x*⟩ for every u. The book's "apply the first fact to F*" is not literally available, F* being concave; the route here spends the closedness hypothesis, and it is spent nowhere else in the corollary.

Corollary 33.2.2

theorem Rockafellar.corollary_33_2_2 {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.PolyhedralBifun F) (hp : Tdaf.ConvexAnalysis.Proper (Tdaf.ConvexAnalysis.graphFn F)) (u : TdafSurface.Rn m) (y : TdafSurface.Rn n) (h : u ∈ Tdaf.ConvexAnalysis.domBifun F ∨ y ∈ Tdaf.ConvexAnalysis.domConcaveBifun (dualProgram F)) : bifunBracket F (u, y) = adjointBracket F (u, y)

Corollary 33.2.2. For a proper polyhedral convex bifunction F, ⟨Fu, x*⟩ = ⟨u, F*x*⟩ except when both u ∉ dom F and x* ∉ dom F*: polyhedrality drops Corollary 33.2.1's ri.

theorem Rockafellar.corollary_33_2_2_exceptional {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} {u : TdafSurface.Rn m} (hu : u ∉ Tdaf.ConvexAnalysis.domBifun F) {y : TdafSurface.Rn n} (hy : y ∉ Tdaf.ConvexAnalysis.domConcaveBifun (dualProgram F)) : bifunBracket F (u, y) = ⊥ ∧ adjointBracket F (u, y) = ⊤

Corollary 33.2.2, the parenthetical: in the exceptional case one quantity is +∞, the other -∞. Neither polyhedrality nor properness is used.

Full, lower and upper closedness

theorem Rockafellar.convexClosedFn_of_finite {m n : ℕ} {K : TdafSurface.Rn m × TdafSurface.Rn n → EReal} (hK : Tdaf.ConvexAnalysis.ConcaveConvexFn K) (hbot : ∀ (p : TdafSurface.Rn m × TdafSurface.Rn n), K p ≠ ⊥) (htop : ∀ (p : TdafSurface.Rn m × TdafSurface.Rn n), K p ≠ ⊤) : Tdaf.ConvexAnalysis.ConvexClosedFn K

A saddle-function finite everywhere is convex-closed: Corollary 10.1.1, slice by slice.

theorem Rockafellar.fullyClosedFn_of_finite {m n : ℕ} {K : TdafSurface.Rn m × TdafSurface.Rn n → EReal} (hK : Tdaf.ConvexAnalysis.ConcaveConvexFn K) (hbot : ∀ (p : TdafSurface.Rn m × TdafSurface.Rn n), K p ≠ ⊥) (htop : ∀ (p : TdafSurface.Rn m × TdafSurface.Rn n), K p ≠ ⊤) : Tdaf.ConvexAnalysis.FullyClosedFn K

A saddle-function finite everywhere is fully closed.

theorem Rockafellar.fullyClosed_iff_lowerClosed_and_upperClosed {m n : ℕ} (K : TdafSurface.Rn m × TdafSurface.Rn n → EReal) : Tdaf.ConvexAnalysis.FullyClosedFn K ↔ Tdaf.ConvexAnalysis.LowerClosedFn K ∧ Tdaf.ConvexAnalysis.UpperClosedFn K

Fully closed is lower closed and upper closed together, by idempotence of cl₁ and cl₂.

theorem Rockafellar.convexConcave_lowerClosed_iff {m n : ℕ} (K : TdafSurface.Rn m × TdafSurface.Rn n → EReal) : (fun (p : TdafSurface.Rn m × TdafSurface.Rn n) => -Tdaf.ConvexAnalysis.upperCl (fun (q : TdafSurface.Rn m × TdafSurface.Rn n) => -K q) p) = K ↔ Tdaf.ConvexAnalysis.UpperClosedFn fun (p : TdafSurface.Rn m × TdafSurface.Rn n) => -K p

The convex-concave convention. For a convex-concave K the book's cl₁ closes convexly in the first argument and its cl₂ concavely in the second, so both are the operators of this module conjugated by negation, and the book's "K is lower closed" says UpperClosedFn (-K).

theorem Rockafellar.convexConcave_upperClosed_iff {m n : ℕ} (K : TdafSurface.Rn m × TdafSurface.Rn n → EReal) : (fun (p : TdafSurface.Rn m × TdafSurface.Rn n) => -Tdaf.ConvexAnalysis.lowerCl (fun (q : TdafSurface.Rn m × TdafSurface.Rn n) => -K q) p) = K ↔ Tdaf.ConvexAnalysis.LowerClosedFn fun (p : TdafSurface.Rn m × TdafSurface.Rn n) => -K p

The other half: "K upper closed" for a convex-concave K is LowerClosedFn (-K).

Theorem 33.3

theorem Rockafellar.theorem_33_3_lowerClosed {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.ConvexBifun F) (hcl : Tdaf.ConvexAnalysis.ClosedBifun F) : Tdaf.ConvexAnalysis.LowerClosedFn (bifunBracket F)

Theorem 33.3, one direction: the bracket of a closed convex bifunction is a lower closed concave-convex function. Both closure steps are Theorem 33.2.

theorem Rockafellar.theorem_33_3 {m n : ℕ} {K : TdafSurface.Rn m × TdafSurface.Rn n → EReal} (hK : Tdaf.ConvexAnalysis.ConcaveConvexFn K) (hlc : Tdaf.ConvexAnalysis.LowerClosedFn K) : ∃! F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n), Tdaf.ConvexAnalysis.ConvexBifun F ∧ Tdaf.ConvexAnalysis.ClosedBifun F ∧ bifunBracket F = K

Theorem 33.3. The same relations are a one-to-one correspondence between the lower closed concave-convex functions on ℝᵐ × ℝⁿ and the closed convex bifunctions from ℝᵐ to ℝⁿ.

Corollary 33.3.1

theorem Rockafellar.corollary_33_3_1 {m n : ℕ} {Klow Kup : TdafSurface.Rn m × TdafSurface.Rn n → EReal} (hK : Tdaf.ConvexAnalysis.ConcaveConvexFn Klow) (h1 : cl₁ Klow = Kup) (h2 : cl₂ Kup = Klow) : ∃! F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n), Tdaf.ConvexAnalysis.ConvexBifun F ∧ Tdaf.ConvexAnalysis.ClosedBifun F ∧ bifunBracket F = Klow ∧ adjointBracket F = Kup

Corollary 33.3.1. For concave-convex K̲ and K̄, a closed convex bifunction F with K̲ (u, x*) = ⟨Fu, x*⟩ and K̄ (u, x*) = ⟨u, F*x*⟩ exists — and is then unique — if and only if cl₁ K̲ = K̄ and cl₂ K̄ = K̲. This is the sufficiency.

theorem Rockafellar.corollary_33_3_1_necessity_first {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.ConvexBifun F) : cl₁ (bifunBracket F) = adjointBracket F

Corollary 33.3.1, necessity: cl₁ ⟨Fu, x*⟩ = ⟨u, F*x*⟩, needing no closedness.

theorem Rockafellar.corollary_33_3_1_necessity_second {m n : ℕ} {F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n)} (hF : Tdaf.ConvexAnalysis.ConvexBifun F) (hcl : Tdaf.ConvexAnalysis.ClosedBifun F) : cl₂ (adjointBracket F) = bifunBracket F

Corollary 33.3.1, necessity: cl₂ ⟨u, F*x*⟩ = ⟨Fu, x*⟩ for a closed F.

theorem Rockafellar.corollary_33_3_1_lowerClosed {m n : ℕ} {Klow Kup : TdafSurface.Rn m × TdafSurface.Rn n → EReal} (h1 : cl₁ Klow = Kup) (h2 : cl₂ Kup = Klow) : Tdaf.ConvexAnalysis.LowerClosedFn Klow

Corollary 33.3.1: the closure relations make K̲ lower closed.

theorem Rockafellar.corollary_33_3_1_upperClosed {m n : ℕ} {Klow Kup : TdafSurface.Rn m × TdafSurface.Rn n → EReal} (h1 : cl₁ Klow = Kup) (h2 : cl₂ Kup = Klow) : Tdaf.ConvexAnalysis.UpperClosedFn Kup

Corollary 33.3.1: the closure relations make K̄ upper closed.

theorem Rockafellar.corollary_33_3_1_le {m n : ℕ} {Klow Kup : TdafSurface.Rn m × TdafSurface.Rn n → EReal} (h2 : cl₂ Kup = Klow) : Klow ≤ Kup

Corollary 33.3.1: K̲ ≤ K̄. Only the cl₂ relation is used, because cl₂ lowers.

Corollary 33.3.2

noncomputable def Rockafellar.corollary_33_3_2 {m n : ℕ} : { K : TdafSurface.Rn m × TdafSurface.Rn n → EReal // Tdaf.ConvexAnalysis.ConcaveConvexFn K ∧ Tdaf.ConvexAnalysis.LowerClosedFn K } ≃ { K : TdafSurface.Rn m × TdafSurface.Rn n → EReal // Tdaf.ConvexAnalysis.ConcaveConvexFn K ∧ Tdaf.ConvexAnalysis.UpperClosedFn K }

Corollary 33.3.2. K̄ = cl₁ K̲ and K̲ = cl₂ K̄ are a one-to-one correspondence between the lower closed and the upper closed concave-convex functions on ℝᵐ × ℝⁿ.

Equations

• Rockafellar.corollary_33_3_2 = Tdaf.ConvexAnalysis.lowerUpperClosedEquiv (TdafSurface.pairing m) (TdafSurface.pairing n)

theorem Rockafellar.corollary_33_3_2_apply {m n : ℕ} (K : { K : TdafSurface.Rn m × TdafSurface.Rn n → EReal // Tdaf.ConvexAnalysis.ConcaveConvexFn K ∧ Tdaf.ConvexAnalysis.LowerClosedFn K }) : ↑(corollary_33_3_2 K) = cl₁ ↑K

The forward relation of Corollary 33.3.2 is K̄ = cl₁ K̲.

theorem Rockafellar.corollary_33_3_2_symm_apply {m n : ℕ} (K : { K : TdafSurface.Rn m × TdafSurface.Rn n → EReal // Tdaf.ConvexAnalysis.ConcaveConvexFn K ∧ Tdaf.ConvexAnalysis.UpperClosedFn K }) : ↑(corollary_33_3_2.symm K) = cl₂ ↑K

The inverse relation of Corollary 33.3.2 is K̲ = cl₂ K̄.

Corollary 33.3.3

Where the book asks for K "finite continuous" on C × D, meaning jointly, the hypotheses below ask only for convexity, concavity and continuity of each one-variable section on its own set.

theorem Rockafellar.corollary_33_3_3_lowerClosed {m n : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn n)} {K : TdafSurface.Rn m × TdafSurface.Rn n → ℝ} (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : TdafSurface.Rn n) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : TdafSurface.Rn m) => K (u, x)) C) : Tdaf.ConvexAnalysis.LowerClosedFn (Tdaf.ConvexAnalysis.lowerSimpleExt C D K)

Corollary 33.3.3: the lower simple extension K̲ of such a K is lower closed.

theorem Rockafellar.corollary_33_3_3_upperClosed {m n : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn n)} {K : TdafSurface.Rn m × TdafSurface.Rn n → ℝ} (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : TdafSurface.Rn n) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : TdafSurface.Rn m) => K (u, x)) C) : Tdaf.ConvexAnalysis.UpperClosedFn (Tdaf.ConvexAnalysis.upperSimpleExt C D K)

Corollary 33.3.3: the upper simple extension K̄ is upper closed.

theorem Rockafellar.corollary_33_3_3 {m n : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn n)} {K : TdafSurface.Rn m × TdafSurface.Rn n → ℝ} (hC : Convex ℝ C) (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hDne : D.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : TdafSurface.Rn n) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : TdafSurface.Rn m) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : TdafSurface.Rn n) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : TdafSurface.Rn m) => K (u, x)) C) : ∃! F : Tdaf.ConvexAnalysis.Bifun (TdafSurface.Rn m) (TdafSurface.Rn n), Tdaf.ConvexAnalysis.ConvexBifun F ∧ Tdaf.ConvexAnalysis.ClosedBifun F ∧ bifunBracket F = Tdaf.ConvexAnalysis.lowerSimpleExt C D K ∧ adjointBracket F = Tdaf.ConvexAnalysis.upperSimpleExt C D K

Corollary 33.3.3, main clause: there is a unique closed convex bifunction F whose two brackets are the lower and the upper simple extension of K.

theorem Rockafellar.corollary_33_3_3_bracket {m n : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn n)} {K : TdafSurface.Rn m × TdafSurface.Rn n → ℝ} (hC : Convex ℝ C) (hDcl : IsClosed D) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : TdafSurface.Rn n) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : TdafSurface.Rn m) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : TdafSurface.Rn n) => K (u, x)) D) : bifunBracket (bifunOfSaddleFn (Tdaf.ConvexAnalysis.lowerSimpleExt C D K)) = Tdaf.ConvexAnalysis.lowerSimpleExt C D K

That bifunction is K̲ (u, ·)*, and its bracket is K̲ again.

theorem Rockafellar.corollary_33_3_3_adjointBracket {m n : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn n)} {K : TdafSurface.Rn m × TdafSurface.Rn n → ℝ} (hC : Convex ℝ C) (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : TdafSurface.Rn n) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : TdafSurface.Rn m) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : TdafSurface.Rn n) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : TdafSurface.Rn m) => K (u, x)) C) : adjointBracket (bifunOfSaddleFn (Tdaf.ConvexAnalysis.lowerSimpleExt C D K)) = Tdaf.ConvexAnalysis.upperSimpleExt C D K

Its adjoint bracket is K̄.

theorem Rockafellar.corollary_33_3_3_dom {m n : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn n)} {K : TdafSurface.Rn m × TdafSurface.Rn n → ℝ} (hC : Convex ℝ C) (hDcl : IsClosed D) (hDne : D.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : TdafSurface.Rn n) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : TdafSurface.Rn m) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : TdafSurface.Rn n) => K (u, x)) D) : Tdaf.ConvexAnalysis.domBifun (bifunOfSaddleFn (Tdaf.ConvexAnalysis.lowerSimpleExt C D K)) = C

Corollary 33.3.3: dom F = C.

theorem Rockafellar.corollary_33_3_3_domAdjoint {m n : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn n)} {K : TdafSurface.Rn m × TdafSurface.Rn n → ℝ} (hC : Convex ℝ C) (hCcl : IsClosed C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : TdafSurface.Rn n) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : TdafSurface.Rn m) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : TdafSurface.Rn n) => K (u, x)) D) (hcontC : ∀ x ∈ D, ContinuousOn (fun (u : TdafSurface.Rn m) => K (u, x)) C) : Tdaf.ConvexAnalysis.domConcaveBifun (dualProgram (bifunOfSaddleFn (Tdaf.ConvexAnalysis.lowerSimpleExt C D K))) = D

Corollary 33.3.3: dom F* = D.

theorem Rockafellar.corollary_33_3_3_bifun_of_notMem {m n : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn n)} {K : TdafSurface.Rn m × TdafSurface.Rn n → ℝ} {u : TdafSurface.Rn m} (hu : u ∉ C) (x : TdafSurface.Rn n) : bifunOfSaddleFn (Tdaf.ConvexAnalysis.lowerSimpleExt C D K) u x = ⊤

Corollary 33.3.3, the formula for F off C: (Fu)(x) = +∞.

theorem Rockafellar.corollary_33_3_3_bifun_of_mem {m n : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn n)} {K : TdafSurface.Rn m × TdafSurface.Rn n → ℝ} {u : TdafSurface.Rn m} (hu : u ∈ C) (x : TdafSurface.Rn n) : bifunOfSaddleFn (Tdaf.ConvexAnalysis.lowerSimpleExt C D K) u x = ⨆ y ∈ D, ↑(((TdafSurface.pairing n) x) y) - ↑(K (u, y))

Corollary 33.3.3, the formula for F on C: (Fu)(x) = sup {⟨x, x*⟩ - K (u, x*) | x* ∈ D}.

theorem Rockafellar.corollary_33_3_3_adjoint_of_mem {m n : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn n)} {K : TdafSurface.Rn m × TdafSurface.Rn n → ℝ} (hC : Convex ℝ C) (hDcl : IsClosed D) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : TdafSurface.Rn n) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : TdafSurface.Rn m) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : TdafSurface.Rn n) => K (u, x)) D) {y : TdafSurface.Rn n} (hy : y ∈ D) (v : TdafSurface.Rn m) : dualProgram (bifunOfSaddleFn (Tdaf.ConvexAnalysis.lowerSimpleExt C D K)) y v = ⨅ u ∈ C, ↑(((TdafSurface.pairing m) u) v) - ↑(K (u, y))

Corollary 33.3.3, the formula for F* on D: (F*x*)(u*) = inf {⟨u, u*⟩ - K (u, x*) | u ∈ C}.

theorem Rockafellar.corollary_33_3_3_adjoint_of_notMem {m n : ℕ} {C : Set (TdafSurface.Rn m)} {D : Set (TdafSurface.Rn n)} {K : TdafSurface.Rn m × TdafSurface.Rn n → ℝ} (hC : Convex ℝ C) (hDcl : IsClosed D) (hCne : C.Nonempty) (hconv : ∀ u ∈ C, ConvexOn ℝ D fun (x : TdafSurface.Rn n) => K (u, x)) (hconc : ∀ x ∈ D, ConcaveOn ℝ C fun (u : TdafSurface.Rn m) => K (u, x)) (hcontD : ∀ u ∈ C, ContinuousOn (fun (x : TdafSurface.Rn n) => K (u, x)) D) {y : TdafSurface.Rn n} (hy : y ∉ D) (v : TdafSurface.Rn m) : dualProgram (bifunOfSaddleFn (Tdaf.ConvexAnalysis.lowerSimpleExt C D K)) y v = ⊥

Corollary 33.3.3, the formula for F* off D: (F*x*)(u*) = -∞.