noncomputable def adjointOfConcaveBifunction {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) : (Fin n → ℝ) → (Fin m → ℝ) → EReal

Definition 6.30.15: the adjoint G* of a concave bifunction G : ℝ^m → ℝ^n is the bifunction on dual variables x* ∈ ℝ^n and u* ∈ ℝ^m given by G*(x*, u*) = sup_{u ∈ ℝ^m, x ∈ ℝ^n} (G(u, x) - ⟪x, x*⟫ + ⟪u, u*⟫). Equivalently, for each x*, the slice G* x* is the function u* ↦ sup_{u, x} (G(u, x) - ⟪x, x*⟫ + ⟪u, u*⟫).

@[reducible, inline]

noncomputable abbrev dualPerturbationFunctionOfConcaveProgram {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) : (Fin n → ℝ) → EReal

The perturbation family of the convex program dual to the concave program associated with G, obtained by passing to the concave adjoint bifunction G*.

theorem helperForTheorem_6_30_7_projectionFiber_eq_negSliceRange {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) (u : Fin m → ℝ) : {z : EReal | ∃ (w : Fin (m + n) → ℝ), (projectionLinearMap ⋯) w = u ∧ z = -bifunctionGraphFunction (↑G) w} = Set.range fun (x : Fin n → ℝ) => -↑G u x

Helper for Theorem 6.30.7: the projection fiber of the negated graph function over u is exactly the range of the negated slice x ↦ -G(u, x).

theorem helperForTheorem_6_30_7_negPerturbation_eq_sInf_negSlice {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) (u : Fin m → ℝ) : -perturbationFunctionOfConcaveProgram G u = sInf {z : EReal | ∃ (w : Fin (m + n) → ℝ), (projectionLinearMap ⋯) w = u ∧ z = -bifunctionGraphFunction (↑G) w}

Helper for Theorem 6.30.7: negating the perturbation supremum rewrites it as the fiber infimum of the negated graph function.

theorem helperForTheorem_6_30_7_convex_negPerturbation {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) : ConvexFunction fun (u : Fin m → ℝ) => -perturbationFunctionOfConcaveProgram G u

Helper for Theorem 6.30.7: the negated perturbation function is convex because it is the fiber-inf image of the convex negated graph function.

theorem helperForTheorem_6_30_7_effectiveDomain_mem_iff {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) (u : Fin m → ℝ) : ⊥ < perturbationFunctionOfConcaveProgram G u ↔ ∃ (x : Fin n → ℝ), ⊥ < ↑G u x

Helper for Theorem 6.30.7: the perturbation value at u is above ⊥ exactly when some point of the slice G u is above ⊥.

theorem perturbationFunction_concave_and_effectiveDomain_eq_bifunctionDomain {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) : (ConvexFunction fun (u : Fin m → ℝ) => -perturbationFunctionOfConcaveProgram G u) ∧ {u : Fin m → ℝ | ⊥ < perturbationFunctionOfConcaveProgram G u} = concaveBifunctionDomain G

Theorem 6.30.7: if G is a concave bifunction from ℝ^m to ℝ^n, then its perturbation function u ↦ sup_{x ∈ ℝ^n} G(u, x) is a concave extended-real-valued function on ℝ^m. Moreover, the effective domain of this perturbation function is exactly dom G, i.e. dom (sup G) = dom G.