Convex Analysis (Rockafellar, 1970) -- Chapter 06 -- Section 31 -- Part 20

open scoped Topology Pointwisesection Chap06section Section31attribute [local instance] Classical.propDecidable

Tucker-style quadratic data for a partial-quadratic program over the nonnegative orthant.

structure QuadraticTuckerRepresentation (n : ℕ) (f : (Fin n → ℝ) → EReal) where auxDim : ℕ encode : (Fin n → ℝ) →ₗ[ℝ] (Fin auxDim → ℝ) rhs : Fin auxDim → ℝ quadraticPart : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ) linearPart : Fin n → ℝ constantPart : ℝ representation : ∀ x : Fin n → ℝ, f x = if ∀ i : Fin auxDim, 0 ≤ encode x i + rhs i then ((((dotProduct x (quadraticPart x)) / 2 + dotProduct linearPart x + constantPart : ℝ)) : EReal) else (⊤ : EReal)

The linear-programming application of Corollary 31.4.1, packaged with Tucker representations of Unknown identifier `f`f and .

def LinearProgrammingDualityApplicationStatement {n : ℕ} (f : (Fin n → ℝ) → EReal) : Prop := Nonempty (AffineTuckerRepresentation n f) ∧ Nonempty (AffineTuckerRepresentation n (fenchelConjugate n f)) ∧ NonnegativeOrthantFenchelApplicationStatement (n := n) f

The quadratic-programming application of Corollary 31.4.1, packaged with Tucker representations of Unknown identifier `f`f and .

def QuadraticProgrammingDualityApplicationStatement {n : ℕ} (f : (Fin n → ℝ) → EReal) : Prop := Nonempty (QuadraticTuckerRepresentation n f) ∧ Nonempty (QuadraticTuckerRepresentation n (fenchelConjugate n f)) ∧ NonnegativeOrthantFenchelApplicationStatement (n := n) f

A finite directed graph with Unknown identifier `n`n oriented edges, recorded by its tail and head maps.

structure FiniteDirectedGraph (n : ℕ) where vertexCount : ℕ tail : Fin n → Fin vertexCount head : Fin n → Fin vertexCount

The signed incidence coefficient of an oriented edge at a vertex: at the head, -1 : ℤ-1 at the tail, and 0 : ℕ0 elsewhere.

def directedGraphIncidenceCoeff {n : ℕ} (G : FiniteDirectedGraph n) (v : Fin G.vertexCount) (e : Fin n) : ℝ := (if G.head e = v then (1 : ℝ) else 0) - (if G.tail e = v then (1 : ℝ) else 0)

The incidence map sending an edge-flow to its signed vertex divergence.

noncomputable def directedGraphIncidenceMap {n : ℕ} (G : FiniteDirectedGraph n) : (Fin n → ℝ) →ₗ[ℝ] (Fin G.vertexCount → ℝ) where toFun x v := ∑ e : Fin n, directedGraphIncidenceCoeff G v e * x e map_add' x y := by ext v simp [directedGraphIncidenceCoeff, mul_add, Finset.sum_add_distrib, sub_eq_add_neg, add_comm, This simp argument is unused: add_left_comm Hint: Omit it from the simp argument list. simp [directedGraphIncidenceCoeff, mul_add, Finset.sum_add_distrib, sub_eq_add_neg, add_comm, ̲ ̲ ̲ ̲ ̲ ̲a̵d̵d̵_̵l̵e̵f̵t̵_̵c̵o̵m̵m̵,̵ ̵add_assoc] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`add_left_comm, This simp argument is unused: add_assoc Hint: Omit it from the simp argument list. simp [directedGraphIncidenceCoeff, mul_add, Finset.sum_add_distrib, sub_eq_add_neg, add_comm, ̲ ̲ ̲ ̲ ̲ ̲a̵d̵d̵_̵l̵e̵f̵t̵_̵c̵o̵m̵m̵,̵ ̵a̵d̵d̵_̵a̵s̵s̵o̵c̵]̵a̲d̲d̲_̲l̲e̲f̲t̲_̲c̲o̲m̲m̲]̲ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`add_assoc] map_smul' a x := by ext v simp only [Pi.smul_apply] trans ∑ e : Fin n, a * (directedGraphIncidenceCoeff G v e * x e) · apply Finset.sum_congr rfl intro e he simp [smul_eq_mul] ring_nf · simpa [smul_eq_mul, mul_assoc] using (Finset.mul_sum (s := Finset.univ) (f := fun e : Fin n => directedGraphIncidenceCoeff G v e * x e) a).symm

The cycle space of a finite directed graph, viewed as a subspace of edge-vectors.

noncomputable def directedGraphCycleSpace {n : ℕ} (G : FiniteDirectedGraph n) : Submodule ℝ (Fin n → ℝ) := LinearMap.ker (directedGraphIncidenceMap G)

The tension space of a finite directed graph, identified with the orthogonal complement of its cycle space in the sense used by Corollary 31.4.2.

def directedGraphTensionSpace {n : ℕ} (G : FiniteDirectedGraph n) : Set (Fin n → ℝ) := {xStar | ∀ x ∈ (directedGraphCycleSpace G : Set (Fin n → ℝ)), dotProduct xStar x = 0}

The graph specialization of Corollary 31.4.2: for a directed graph Unknown identifier `G`G, minimize Unknown identifier `f`f on the cycle space of Unknown identifier `G`G and minimize on the corresponding tension space.

def GraphCycleTensionFenchelApplicationStatement {n : ℕ} (f : (Fin n → ℝ) → EReal) (G : FiniteDirectedGraph n) : Prop := let cycleSpace := directedGraphCycleSpace G let tensionSpace := directedGraphTensionSpace G let primal : EReal := functionInfimumEReal (fun x => f x + indicatorFunction (cycleSpace : Set (Fin n → ℝ)) x) let dual : EReal := functionInfimumEReal (fun xStar => fenchelConjugate n f xStar + indicatorFunction tensionSpace xStar) ((((∃ x : Fin n → ℝ, x ∈ (cycleSpace : Set (Fin n → ℝ)) ∧ x ∈ euclideanRelativeInterior_fin n (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f)) ∨ ∃ xStar : Fin n → ℝ, xStar ∈ tensionSpace ∧ xStar ∈ euclideanRelativeInterior_fin n (effectiveDomain (Set.univ : Set (Fin n → ℝ)) (fenchelConjugate n f))) → primal = -dual) ∧ ((∃ x : Fin n → ℝ, x ∈ (cycleSpace : Set (Fin n → ℝ)) ∧ x ∈ euclideanRelativeInterior_fin n (effectiveDomain (Set.univ : Set (Fin n → ℝ)) f)) → ∃ xStar : Fin n → ℝ, xStar ∈ tensionSpace ∧ dual = fenchelConjugate n f xStar) ∧ ((∃ xStar : Fin n → ℝ, xStar ∈ tensionSpace ∧ xStar ∈ euclideanRelativeInterior_fin n (effectiveDomain (Set.univ : Set (Fin n → ℝ)) (fenchelConjugate n f))) → ∃ x : Fin n → ℝ, x ∈ (cycleSpace : Set (Fin n → ℝ)) ∧ primal = f x))
-- Proof sketch: for 1., specialize Corollary 31.4.1 to partially affine and partially quadratic -- convex functions, and package the resulting consequences using the existing -- linear-/quadratic-programming application predicates together with chosen Tucker -- representations of `f` and `f⋆`. For 2., specialize Corollary 31.4.2 to -- `L := directedGraphCycleSpace G`; the corresponding orthogonal system is realized here by -- `directedGraphTensionSpace G`, yielding the cycle/tension dual extremum problem.

Remark 31.4.4 (Applications of Corollaries 31.4.1 and 31.4.2): 1. If Unknown identifier `f`f in Corollary 31.4.1 is partially affine and both Unknown identifier `f`f and admit Tucker representations, then one obtains the nonnegative-orthant Fenchel duality statement underlying the Gale-Kuhn-Tucker duality theorem for linear programming; likewise, if Unknown identifier `f`f is partial quadratic and both Unknown identifier `f`f and admit quadratic Tucker representations, one obtains the corresponding nonnegative-orthant duality statement for quadratic programming. 2. For Corollary 31.4.2, the subspaces Unknown identifier `L`L and encode dual linear systems; in particular, taking Unknown identifier `L`L to be the cycle space of a directed graph and directedGraphTensionSpace sorry : Set (Fin ?m.1 → ℝ)directedGraphTensionSpace Unknown identifier `G`G as the chosen realization of gives the dual extremum problems of minimizing Unknown identifier `f`f on cycles and minimizing on tensions.

theorem fenchel_duality_corollaries_applications_to_programming_and_subspaces {n : ℕ} (f : (Fin n → ℝ) → EReal) : (IsPartialAffineConvexFunction n f → ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f → ClosedConvexFunction f → Nonempty (AffineTuckerRepresentation n f) → Nonempty (AffineTuckerRepresentation n (fenchelConjugate n f)) → LinearProgrammingDualityApplicationStatement (n := n) f) ∧ (IsPartialQuadraticConvexFunction n f → ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f → ClosedConvexFunction f → Nonempty (QuadraticTuckerRepresentation n f) → Nonempty (QuadraticTuckerRepresentation n (fenchelConjugate n f)) → QuadraticProgrammingDualityApplicationStatement (n := n) f) ∧ (∀ G : FiniteDirectedGraph n, ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) f → ClosedConvexFunction f → SubspaceFenchelApplicationStatement (n := n) f (directedGraphCycleSpace G) ∧ GraphCycleTensionFenchelApplicationStatement (n := n) f G) := by constructor · intro _hPartialAffine hproper hclosed hfTucker hfStarTucker refine ⟨hfTucker, hfStarTucker, ?_⟩ simpa [NonnegativeOrthantFenchelApplicationStatement] using (fenchel_duality_nonnegative_orthant_corollary (n := n) f hproper hclosed) constructor · intro _hPartialQuadratic hproper hclosed hfTucker hfStarTucker refine ⟨hfTucker, hfStarTucker, ?_⟩ simpa [NonnegativeOrthantFenchelApplicationStatement] using (fenchel_duality_nonnegative_orthant_corollary (n := n) f hproper hclosed) · intro G hproper hclosed have hSubspace : SubspaceFenchelApplicationStatement (n := n) f (directedGraphCycleSpace G) := by simpa [SubspaceFenchelApplicationStatement] using (fenchel_duality_subspace_corollary (n := n) f hproper hclosed (directedGraphCycleSpace G)) refine ⟨hSubspace, ?_⟩ dsimp [GraphCycleTensionFenchelApplicationStatement, SubspaceFenchelApplicationStatement, directedGraphTensionSpace] at hSubspace ⊢ exact ⟨hSubspace.1, hSubspace.2.1, hSubspace.2.2.1⟩
end Section31end Chap06