Convex Analysis (Rockafellar, 1970) -- Chapter 08 -- Section 39 -- Part 4

open scoped Pointwiseopen scoped RealInnerProductSpaceopen scoped BigOperatorssection Chap08section Section39

The adjoint of a set-valued mapping in the book's Euclidean convention for the infimum-oriented inequality convention, defined by

.

def setValuedAdjointVecInf {m n : ℕ} (A : (Fin m → ℝ) → Set (Fin n → ℝ)) : (Fin n → ℝ) → Set (Fin m → ℝ) := fun xStar => { uStar | ∀ u, ∀ x, x ∈ A u → finDot u uStar ≤ finDot x xStar }

The adjoint of an EReal : TypeEReal-valued bifunction , viewed as the Fenchel conjugate on the product space with the sign convention

.

noncomputable def eRealBifunctionAdjoint {m n : ℕ} (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : (Fin n → ℝ) → (Fin m → ℝ) → EReal := fun xStar uStar => sSup ((fun p : (Fin m → ℝ) × (Fin n → ℝ) => ((finDot p.2 xStar - finDot p.1 uStar : ℝ) : EReal) - F p.1 p.2) '' Set.univ)
namespace ConvexProcess

The oriented indicator bifunction attached to a convex process Unknown identifier `A`A, depending on the chosen orientation: supremum orientation uses and infimum orientation uses .

noncomputable def indicatorBifunctionOriented {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n) : (Fin m → ℝ) → (Fin n → ℝ) → EReal := match o with | .supremum => ConvexProcess.indicatorBifunction A | .infimum => ConvexProcess.negIndicatorBifunction A

Helper for Theorem 39.2: every fiber of a convex process is convex, so the negative-indicator sections are concave in the Chapter 30 sense. This is the concavity package needed to form the textbook adjoint in infimum orientation.

lemma helperForTheorem_39_2_negIndicatorConcave {m n : ℕ} (A : ConvexProcess m n) : IsConcaveBifunction (ConvexProcess.negIndicatorBifunction A) := by -- This sectionwise concavity package is the local Chapter 33 input; keep it isolated from the -- global graph-style `ConcaveBifunction` bridge used below. intro u -- Step 1: first prove that the ordinary indicator of the fiber `A u` is Jensen-convex. have hIndicatorConv : IsERealConvexOn (Set.univ : Set (Fin n → ℝ)) (fun x => indicatorEReal (A.toSetValued u) x) := by intro x y hx hy a b ha hb hab hxy -- Step 2: use convexity of the fiber to keep convex combinations inside whenever both -- endpoints lie in the fiber, and otherwise reduce to the trivial `⊤` branches. have hConvFiber : Convex ℝ (A.toSetValued u) := (convexProcess_prop_39_0_2 A).1 u by_cases hxmem : x ∈ A.toSetValued u · by_cases hymem : y ∈ A.toSetValued u · -- If both endpoints lie in the fiber, the convex combination also lies in the fiber. have hxyMem : a • x + b • y ∈ A.toSetValued u := hConvFiber hxmem hymem ha hb hab simp [indicatorEReal, hxmem, hymem, hxyMem] · -- If `y` is off the fiber, the right-hand side already becomes large enough. by_cases hxyMem : a • x + b • y ∈ A.toSetValued u · by_cases hZero : b = 0 · have haOne : a = 1 := by linarith simp [indicatorEReal, hxmem, hymem, hZero, haOne] · have hbPos : 0 < b := lt_of_le_of_ne hb (by simpa [eq_comm] using hZero) simp [indicatorEReal, hxmem, hymem, hxyMem, EReal.coe_mul_top_of_pos hbPos] · by_cases hZero : b = 0 · have haOne : a = 1 := by linarith have : a • x + b • y ∈ A.toSetValued u := by simpa [hZero, haOne] using hxmem exact (hxyMem this).elim · have hbPos : 0 < b := lt_of_le_of_ne hb (by simpa [eq_comm] using hZero) simp [indicatorEReal, hxmem, hymem, hxyMem, EReal.coe_mul_top_of_pos hbPos] · by_cases hymem : y ∈ A.toSetValued u · -- This is the symmetric branch where only `x` is off the fiber. by_cases hxyMem : a • x + b • y ∈ A.toSetValued u · by_cases hZero : a = 0 · have hbOne : b = 1 := by linarith simp [indicatorEReal, hxmem, hymem, hZero, hbOne] · have haPos : 0 < a := lt_of_le_of_ne ha (by simpa [eq_comm] using hZero) simp [indicatorEReal, hxmem, hymem, hxyMem, EReal.coe_mul_top_of_pos haPos] · by_cases hZero : a = 0 · have hbOne : b = 1 := by linarith have : a • x + b • y ∈ A.toSetValued u := by simpa [hZero, hbOne] using hymem exact (hxyMem this).elim · have haPos : 0 < a := lt_of_le_of_ne ha (by simpa [eq_comm] using hZero) simp [indicatorEReal, hxmem, hymem, hxyMem, EReal.coe_mul_top_of_pos haPos] · -- If both endpoints are off the fiber, every Jensen branch is immediate after -- simplifying both indicator values to `⊤`. by_cases hxyMem : a • x + b • y ∈ A.toSetValued u · by_cases hZero : a = 0 · have hbOne : b = 1 := by linarith simp [indicatorEReal, hxmem, hymem, hZero, hbOne] · have haPos : 0 < a := lt_of_le_of_ne ha (by simpa [eq_comm] using hZero) have hLe : (0 : EReal) ≤ ((⊤ : EReal) + (b : EReal) * ⊤) := by have hEq : ((⊤ : EReal) + (b : EReal) * ⊤) = (⊤ : EReal) := by have hMulNeBot : ((b : EReal) * ⊤) ≠ (⊥ : EReal) := by by_cases hbZero : b = 0 · simp [hbZero] · have hbPos : 0 < b := lt_of_le_of_ne hb (by simpa [eq_comm] using hbZero) rw [EReal.coe_mul_top_of_pos hbPos] simp exact EReal.top_add_of_ne_bot hMulNeBot rw [hEq] simp simpa [indicatorEReal, hxmem, hymem, hxyMem, EReal.coe_mul_top_of_pos haPos] using hLe · by_cases hZero : a = 0 · have hbOne : b = 1 := by linarith simp [indicatorEReal, hxmem, hymem, This simp argument is unused: hxyMem Hint: Omit it from the simp argument list. simp [indicatorEReal, hxmem, hymem, hx̵y̵M̵e̵m̵,̵ ̵h̵Zero, hbOne] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hxyMem, hZero, hbOne] · have haPos : 0 < a := lt_of_le_of_ne ha (by simpa [eq_comm] using hZero) have hEq : ((⊤ : EReal) + (b : EReal) * ⊤) = (⊤ : EReal) := by have hMulNeBot : ((b : EReal) * ⊤) ≠ (⊥ : EReal) := by by_cases hbZero : b = 0 · simp [hbZero] · have hbPos : 0 < b := lt_of_le_of_ne hb (by simpa [eq_comm] using hbZero) rw [EReal.coe_mul_top_of_pos hbPos] simp exact EReal.top_add_of_ne_bot hMulNeBot simpa [indicatorEReal, hxmem, hymem, hxyMem, EReal.coe_mul_top_of_pos haPos] using hEq -- Step 3: negate the convex indicator section to get the desired concave negative indicator. have hConc : IsERealConcaveOn (Set.univ : Set (Fin n → ℝ)) (fun x => -indicatorEReal (A.toSetValued u) x) := helperForLemma33_0_5_convexNegation_isConcave (C := (Set.univ : Set (Fin n → ℝ))) (f := fun x => indicatorEReal (A.toSetValued u) x) hIndicatorConv have hEq : (fun x => -indicatorEReal (A.toSetValued u) x) = ConvexProcess.negIndicatorBifunction A u := by funext x by_cases hx : x ∈ A.toSetValued u <;> simp [ConvexProcess.negIndicatorBifunction, negIndicatorEReal, indicatorEReal, hx] simpa [hEq] using hConc

Helper for Theorem 39.2: the Chapter 30 concave adjoint in the infimum-oriented branch needs the global graph-style ConcaveBifunction {m n : ℕ} (G : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : PropConcaveBifunction package. This is the remaining textbook bridge from the already established sectionwise concavity of Unknown identifier `negIndicatorBifunction`negIndicatorBifunction.

lemma helperForTheorem_39_2_negIndicatorConcaveTextbook {m n : ℕ} (A : ConvexProcess m n) : ConcaveBifunction (ConvexProcess.negIndicatorBifunction A) := by -- The process graph is convex, so `-bifunctionGraphFunction` should be convex in the Chapter 30 -- sense. Keep this bridge isolated here; downstream theorem statements should use the corrected -- adjoint object rather than the old infimum-oriented convex adjoint. let graphSet : Set (Fin (m + n) → ℝ) := {z | (fun j => z (Fin.natAdd m j)) ∈ A.toSetValued (fun i => z (Fin.castAdd n i))} have hGraphSetConvex : Convex ℝ graphSet := by have hGraphConv : Convex ℝ (setValuedGraph A.toSetValued) := (helperForProposition_39_0_1_graphConvexCone_ofConvexProcess A).convex intro z₁ hz₁ z₂ hz₂ a b ha hb hab have hz₁' : ((fun i => z₁ (Fin.castAdd n i)), (fun j => z₁ (Fin.natAdd m j))) ∈ setValuedGraph A.toSetValued := by simpa [graphSet, setValuedGraph] using hz₁ have hz₂' : ((fun i => z₂ (Fin.castAdd n i)), (fun j => z₂ (Fin.natAdd m j))) ∈ setValuedGraph A.toSetValued := by simpa [graphSet, setValuedGraph] using hz₂ have hCombo : a • ((fun i => z₁ (Fin.castAdd n i)), (fun j => z₁ (Fin.natAdd m j))) + b • ((fun i => z₂ (Fin.castAdd n i)), (fun j => z₂ (Fin.natAdd m j))) ∈ setValuedGraph A.toSetValued := hGraphConv hz₁' hz₂' ha hb hab simpa [graphSet, setValuedGraph, Pi.add_apply, Pi.smul_apply] using hCombo have hIndicatorConvex : ConvexFunction (indicatorFunction graphSet) := convexFunction_indicator_of_convex (C := graphSet) hGraphSetConvex have hGraphEq : (fun z : Fin (m + n) → ℝ => -bifunctionGraphFunction (ConvexProcess.negIndicatorBifunction A) z) = indicatorFunction graphSet := by funext z by_cases hz : z ∈ graphSet · have hz' : (fun j => z (Fin.natAdd m j)) ∈ A.toSetValued (fun i => z (Fin.castAdd n i)) := by simpa [graphSet] using hz simp [graphSet, bifunctionGraphFunction, ConvexProcess.negIndicatorBifunction, indicatorFunction, negIndicatorEReal, hz, hz'] · have hz' : (fun j => z (Fin.natAdd m j)) ∉ A.toSetValued (fun i => z (Fin.castAdd n i)) := by simpa [graphSet] using hz simp [graphSet, bifunctionGraphFunction, ConvexProcess.negIndicatorBifunction, indicatorFunction, negIndicatorEReal, hz, hz'] -- Step 2: rewrite the negated graph function to the ordinary indicator of the graph and reuse -- the standard indicator-of-convex-set convexity theorem. simpa [ConcaveBifunction, hGraphEq] using hIndicatorConvex

The oriented adjoint bifunction attached to the oriented indicator of a convex process. In supremum orientation this is the Fenchel adjoint of the convex indicator; in infimum orientation it is the Chapter 30 concave adjoint of the negative indicator.

noncomputable def indicatorBifunctionAdjointOriented {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n) : (Fin n → ℝ) → (Fin m → ℝ) → EReal := match o with | .supremum => eRealBifunctionAdjoint (indicatorBifunctionOriented .supremum A) | .infimum => adjointOfConcaveBifunction ⟨indicatorBifunctionOriented .infimum A, helperForTheorem_39_2_negIndicatorConcaveTextbook A⟩

The oriented indicator bifunction attached to a set-valued mapping , depending on the chosen orientation: supremum orientation uses and infimum orientation uses .

noncomputable def indicatorBifunctionSetValuedOriented {U X : Type*} (o : ConvexSetOrientation) (A : U → Set X) : U → X → EReal := match o with | .supremum => indicatorBifunctionSetValued A | .infimum => fun u x => negIndicatorEReal (A u) x

The oriented adjoint of a set-valued mapping in the book's Euclidean convention: for supremum orientation it uses the inequality , and for infimum orientation it uses . The resulting set-valued mapping has the opposite orientation.

def adjointVecOrientedSetValued {m n : ℕ} (o : ConvexSetOrientation) (A : (Fin m → ℝ) → Set (Fin n → ℝ)) : OrientedSetValuedMap (Fin n → ℝ) (Fin m → ℝ) := match o with | .supremum => { toSetValued := setValuedAdjointVec A orientation := .infimum } | .infimum => { toSetValued := setValuedAdjointVecInf A orientation := .supremum }

The adjoint of a (supremum oriented) convex process , viewed as an infimum oriented set-valued mapping using the Euclidean pairing on Fin ?m.1 → ℝ : TypeFin _ → ℝ.

def adjointVec {m n : ℕ} (A : ConvexProcess m n) : OrientedSetValuedMap (Fin n → ℝ) (Fin m → ℝ) := { toSetValued := setValuedAdjointVec A.toSetValued orientation := .infimum }

The oriented adjoint of a convex process , parameterized by the chosen orientation convention Unknown identifier `o`o.

def adjointVecOriented {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n) : OrientedSetValuedMap (Fin n → ℝ) (Fin m → ℝ) := adjointVecOrientedSetValued o A.toSetValued

The double adjoint set-valued mapping , using the Euclidean pairing on Fin ?m.1 → ℝ : TypeFin _ → ℝ.

def doubleAdjointVecSetValued {m n : ℕ} (A : ConvexProcess m n) : (Fin m → ℝ) → Set (Fin n → ℝ) := setValuedAdjointVec (setValuedAdjointVec A.toSetValued)

The oriented double adjoint set-valued mapping , where the adjoint is taken using the orientation convention Unknown identifier `o`o for Unknown identifier `A`A and then the opposite convention for .

def doubleAdjointVecSetValuedOriented {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n) : (Fin m → ℝ) → Set (Fin n → ℝ) := let Astar : (Fin n → ℝ) → Set (Fin m → ℝ) := (adjointVecOriented o A).toSetValued (adjointVecOrientedSetValued (m := n) (n := m) o.opposite Astar).toSetValued

Oriented version of Proposition 39.0.15 in Euclidean coordinates: taking the inverse of the adjoint is the same as taking the adjoint of the inverse, provided the orientation is switched on the right-hand side. This is the form compatible with Rockafellar's graph-symmetry argument.

theorem prop_39_0_15_orientedVec {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n) : setValuedInverse (adjointVecOriented o A).toSetValued = (adjointVecOriented o.opposite A.inverse).toSetValued := by ext uStar xStar cases o · constructor · intro hx change uStar ∈ setValuedAdjointVec A.toSetValued xStar at hx change xStar ∈ setValuedAdjointVecInf A.inverse.toSetValued uStar intro x u hxu rw [helperForProposition_39_0_6_inverse_toSetValued A] at hxu exact hx u x hxu · intro hx change uStar ∈ setValuedAdjointVec A.toSetValued xStar change xStar ∈ setValuedAdjointVecInf A.inverse.toSetValued uStar at hx intro u x hux have hinv : u ∈ A.inverse.toSetValued x := by rw [helperForProposition_39_0_6_inverse_toSetValued A] exact hux exact hx x u hinv · constructor · intro hx change uStar ∈ setValuedAdjointVecInf A.toSetValued xStar at hx change xStar ∈ setValuedAdjointVec A.inverse.toSetValued uStar intro x u hxu rw [helperForProposition_39_0_6_inverse_toSetValued A] at hxu exact hx u x hxu · intro hx change uStar ∈ setValuedAdjointVecInf A.toSetValued xStar change xStar ∈ setValuedAdjointVec A.inverse.toSetValued uStar at hx intro u x hux have hinv : u ∈ A.inverse.toSetValued x := by rw [helperForProposition_39_0_6_inverse_toSetValued A] exact hux exact hx x u hinv

Proposition 39.0.15 in the default textbook situation of a supremum-oriented convex process.

theorem prop_39_0_15_textbook {m n : ℕ} (A : ConvexProcess m n) : setValuedInverse (adjointVecOriented ConvexSetOrientation.supremum A).toSetValued = (adjointVecOriented ConvexSetOrientation.infimum A.inverse).toSetValued := by simpa using prop_39_0_15_orientedVec ConvexSetOrientation.supremum A

Helper for Theorem 39.2: the oriented adjoint is bundled with the opposite orientation by definition, so the orientation conjunct of the theorem is already immediate.

lemma helperForTheorem_39_2_adjointVecOriented_orientation {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n) : (adjointVecOriented o A).orientation = o.opposite := by -- Unfold the bundled oriented adjoint and read off the orientation field in each orientation -- branch of the definition. cases o <;> rfl

Helper for Theorem 39.2: the oriented adjoint already satisfies the convex-process axioms directly from its defining pointwise inequality, in either orientation.

lemma helperForTheorem_39_2_adjointVecOriented_isConvexProcessMap {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n) : IsConvexProcessMap (adjointVecOriented o A).toSetValued := by cases o · constructor · intro xStar₁ xStar₂ rintro uStar ⟨uStar₁, hu₁, uStar₂, hu₂, rfl⟩ change ∀ u x, x ∈ A.toSetValued u → finDot u (uStar₁ + uStar₂) ≥ finDot x (xStar₁ + xStar₂) intro u x hx have h1 := hu₁ u x hx have h2 := hu₂ u x hx simp [finDot, dotProduct] at h1 h2 ⊢ simpa [Finset.sum_add_distrib, mul_add, add_mul, add_comm, add_left_comm, add_assoc] using add_le_add h1 h2 · constructor · intro xStar r hr ext uStar constructor · intro hu refine ⟨r⁻¹ • uStar, ?_, ?_⟩ · change ∀ u x, x ∈ A.toSetValued u → finDot u (r⁻¹ • uStar) ≥ finDot x xStar intro u x hx have h := hu u x hx simp [finDot, dotProduct] at h ⊢ set a : ℝ := ∑ i, x i * xStar i with ha set b : ℝ := ∑ i, u i * uStar i with hb have hleft : ∑ i, x i * (r * xStar i) = r * a := by rw [ha, Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro i hi ring have hright : ∑ i, u i * (r⁻¹ * uStar i) = r⁻¹ * b := by rw [hb, Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro i hi ring rw [hright] have h' : r * a ≤ b := by simpa [hleft] using h have h'' := mul_le_mul_of_nonneg_left h' (le_of_lt (inv_pos.2 hr)) have h''' : a ≤ r⁻¹ * b := by simpa [mul_assoc, hr.ne'] using h'' exact h''' · ext i simp [smul_eq_mul, hr.ne'] · rintro ⟨v, hv, rfl⟩ change ∀ u x, x ∈ A.toSetValued u → finDot u (r • v) ≥ finDot x (r • xStar) intro u x hx have h := hv u x hx simp [finDot, dotProduct] at h ⊢ set a : ℝ := ∑ i, x i * xStar i with ha set b : ℝ := ∑ i, u i * v i with hb have hleft : ∑ i, x i * (r * xStar i) = r * a := by rw [ha, Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro i hi ring have hright : ∑ i, u i * (r * v i) = r * b := by rw [hb, Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro i hi ring rw [hleft, hright] have h' : a ≤ b := by simpa [ha, hb] using h exact mul_le_mul_of_nonneg_left h' (le_of_lt hr) · change (0 : Fin m → ℝ) ∈ setValuedAdjointVec A.toSetValued (0 : Fin n → ℝ) intro u x hx simp [finDot] · constructor · intro xStar₁ xStar₂ rintro uStar ⟨uStar₁, hu₁, uStar₂, hu₂, rfl⟩ change ∀ u x, x ∈ A.toSetValued u → finDot u (uStar₁ + uStar₂) ≤ finDot x (xStar₁ + xStar₂) intro u x hx have h1 := hu₁ u x hx have h2 := hu₂ u x hx simp [finDot, dotProduct] at h1 h2 ⊢ simpa [Finset.sum_add_distrib, mul_add, add_mul, add_comm, add_left_comm, add_assoc] using add_le_add h1 h2 · constructor · intro xStar r hr ext uStar constructor · intro hu refine ⟨r⁻¹ • uStar, ?_, ?_⟩ · change ∀ u x, x ∈ A.toSetValued u → finDot u (r⁻¹ • uStar) ≤ finDot x xStar intro u x hx have h := hu u x hx simp [finDot, dotProduct] at h ⊢ set a : ℝ := ∑ i, x i * xStar i with ha set b : ℝ := ∑ i, u i * uStar i with hb have hleft : ∑ i, x i * (r * xStar i) = r * a := by rw [ha, Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro i hi ring have hright : ∑ i, u i * (r⁻¹ * uStar i) = r⁻¹ * b := by rw [hb, Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro i hi ring rw [hright] have h' : b ≤ r * a := by simpa [hleft] using h have h'' := mul_le_mul_of_nonneg_left h' (le_of_lt (inv_pos.2 hr)) have h''' : r⁻¹ * b ≤ a := by simpa [mul_assoc, hr.ne'] using h'' exact h''' · ext i simp [smul_eq_mul, hr.ne'] · rintro ⟨v, hv, rfl⟩ change ∀ u x, x ∈ A.toSetValued u → finDot u (r • v) ≤ finDot x (r • xStar) intro u x hx have h := hv u x hx simp [finDot, dotProduct] at h ⊢ set a : ℝ := ∑ i, x i * xStar i with ha set b : ℝ := ∑ i, u i * v i with hb have hleft : ∑ i, x i * (r * xStar i) = r * a := by rw [ha, Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro i hi ring have hright : ∑ i, u i * (r * v i) = r * b := by rw [hb, Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro i hi ring rw [hleft, hright] have h' : b ≤ a := by simpa [ha, hb] using h exact mul_le_mul_of_nonneg_left h' (le_of_lt hr) · change (0 : Fin m → ℝ) ∈ setValuedAdjointVecInf A.toSetValued (0 : Fin n → ℝ) intro u x hx simp [finDot]

Pack a graph point (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `u`u, Unknown identifier `x`x) into a single Fin (sorry + sorry) → ℝ : TypeFin (Unknown identifier `m`m+Unknown identifier `n`n) → ℝ vector. This is the coordinate model used for the graph-cone polarity argument in Theorem 39.2.

def unpackAppend39_2 {m n : ℕ} (z : Fin (m + n) → ℝ) : (Fin m → ℝ) × (Fin n → ℝ) := ((fun i => z (Fin.castAdd n i)), (fun j => z (Fin.natAdd m j)))
lemma unpackAppend39_2_add {m n : ℕ} (z w : Fin (m + n) → ℝ) : unpackAppend39_2 (z + w) = unpackAppend39_2 z + unpackAppend39_2 w := by ext <;> simp [unpackAppend39_2]lemma unpackAppend39_2_smul {m n : ℕ} (r : ℝ) (z : Fin (m + n) → ℝ) : unpackAppend39_2 (r • z) = r • unpackAppend39_2 z := by ext <;> simp [unpackAppend39_2]

The unpacking map as a linear map.

def unpackAppendLinearMap39_2 {m n : ℕ} : (Fin (m + n) → ℝ) →ₗ[ℝ] ((Fin m → ℝ) × (Fin n → ℝ)) := { toFun := unpackAppend39_2 map_add' := unpackAppend39_2_add map_smul' := unpackAppend39_2_smul }
lemma unpackAppend39_2_append {m n : ℕ} (u : Fin m → ℝ) (x : Fin n → ℝ) : unpackAppend39_2 (Fin.append u x) = (u, x) := by ext <;> simp [unpackAppend39_2]lemma append_unpackAppend39_2 {m n : ℕ} (z : Fin (m + n) → ℝ) : Fin.append (unpackAppend39_2 z).1 (unpackAppend39_2 z).2 = z := by ext i cases h : finSumFinEquiv.symm i with | inl hi => have hi' : i = Fin.castAdd n hi := by simpa [finSumFinEquiv_apply_left] using congrArg finSumFinEquiv h subst i simp [unpackAppend39_2, Fin.append_left] | inr hj => have hj' : i = Fin.natAdd m hj := by simpa [finSumFinEquiv_apply_right] using congrArg finSumFinEquiv h subst i simp [unpackAppend39_2, Fin.append_right]

The packed/unpacked graph coordinates form a linear equivalence.

def packAppendLinearEquiv39_2 {m n : ℕ} : ((Fin m → ℝ) × (Fin n → ℝ)) ≃ₗ[ℝ] (Fin (m + n) → ℝ) := { toFun := fun p => Fin.append p.1 p.2 invFun := unpackAppend39_2 left_inv := by intro p rcases p with ⟨u, x⟩ simpa using unpackAppend39_2_append u x right_inv := append_unpackAppend39_2 map_add' := by intro p q ext i cases h : finSumFinEquiv.symm i with | inl hi => have hi' : i = Fin.castAdd n hi := by simpa [finSumFinEquiv_apply_left] using congrArg finSumFinEquiv h subst i simp [Fin.append_left] | inr hj => have hj' : i = Fin.natAdd m hj := by simpa [finSumFinEquiv_apply_right] using congrArg finSumFinEquiv h subst i simp [Fin.append_right] map_smul' := by intro r p ext i cases h : finSumFinEquiv.symm i with | inl hi => have hi' : i = Fin.castAdd n hi := by simpa [finSumFinEquiv_apply_left] using congrArg finSumFinEquiv h subst i simp [Fin.append_left] | inr hj => have hj' : i = Fin.natAdd m hj := by simpa [finSumFinEquiv_apply_right] using congrArg finSumFinEquiv h subst i simp [Fin.append_right] }
lemma continuous_packAppend39_2 {m n : ℕ} : Continuous (fun p : (Fin m → ℝ) × (Fin n → ℝ) => Fin.append p.1 p.2) := by refine continuous_pi ?_ intro i cases h : finSumFinEquiv.symm i with | inl hi => have hi' : i = Fin.castAdd n hi := by simpa [finSumFinEquiv_apply_left] using congrArg finSumFinEquiv h subst i simpa [Fin.append_left] using ((continuous_apply hi).comp continuous_fst : Continuous fun p : (Fin m → ℝ) × (Fin n → ℝ) => p.1 hi) | inr hj => have hj' : i = Fin.natAdd m hj := by simpa [finSumFinEquiv_apply_right] using congrArg finSumFinEquiv h subst i simpa [Fin.append_right] using ((continuous_apply hj).comp continuous_snd : Continuous fun p : (Fin m → ℝ) × (Fin n → ℝ) => p.2 hj)lemma continuous_unpackAppend39_2 {m n : ℕ} : Continuous (fun z : Fin (m + n) → ℝ => unpackAppend39_2 z) := by refine Continuous.prodMk ?_ ?_ · refine continuous_pi ?_ intro i simpa [unpackAppend39_2] using (continuous_apply (Fin.castAdd n i)) · refine continuous_pi ?_ intro j simpa [unpackAppend39_2] using (continuous_apply (Fin.natAdd m j))

The packed/unpacked coordinates as a continuous linear equivalence, used to transport closure between the product graph and its packed Fin (sorry + sorry) : TypeFin (Unknown identifier `m`m+Unknown identifier `n`n) model.

noncomputable def packAppendContinuousLinearEquiv39_2 {m n : ℕ} : ((Fin m → ℝ) × (Fin n → ℝ)) ≃L[ℝ] (Fin (m + n) → ℝ) := (packAppendLinearEquiv39_2 (m := m) (n := n)).toContinuousLinearEquivOfContinuous (continuous_packAppend39_2 (m := m) (n := n))

Packed graph of a convex process in Fin (sorry + sorry) → ℝ : TypeFin (Unknown identifier `m`m+Unknown identifier `n`n) → ℝ.

def packedGraphSet39_2 {m n : ℕ} (A : ConvexProcess m n) : Set (Fin (m + n) → ℝ) := (fun p : (Fin m → ℝ) × (Fin n → ℝ) => Fin.append p.1 p.2) '' setValuedGraph A.toSetValued

Packed graph cone of a convex process.

def packedGraphCone39_2 {m n : ℕ} (A : ConvexProcess m n) : ConvexCone ℝ (Fin (m + n) → ℝ) := (helperForProposition_39_0_1_graphConvexCone_ofConvexProcess A).comap (unpackAppendLinearMap39_2 (m := m) (n := n))
lemma packedGraphCone39_2_carrier {m n : ℕ} (A : ConvexProcess m n) : ((packedGraphCone39_2 A : ConvexCone ℝ (Fin (m + n) → ℝ)) : Set (Fin (m + n) → ℝ)) = packedGraphSet39_2 A := by ext z constructor · intro hz refine ⟨unpackAppend39_2 z, ?_, ?_⟩ · exact hz · exact append_unpackAppend39_2 z · rintro ⟨p, hp, rfl⟩ change unpackAppend39_2 (Fin.append p.1 p.2) ∈ ((helperForProposition_39_0_1_graphConvexCone_ofConvexProcess A : ConvexCone ℝ ((Fin m → ℝ) × (Fin n → ℝ))) : Set ((Fin m → ℝ) × (Fin n → ℝ))) simpa [unpackAppend39_2_append]

The packed primal-dual pairing for the supremum-oriented adjoint.

lemma dotProduct_append_primalDual_sup39_2 {m n : ℕ} (u : Fin m → ℝ) (x : Fin n → ℝ) (uStar : Fin m → ℝ) (xStar : Fin n → ℝ) : dotProduct (Fin.append u x) (Fin.append (-uStar) xStar) = finDot x xStar - finDot u uStar := by simp [finDot, dotProduct, Fin.sum_univ_add, sub_eq_add_neg, add_comm]

The packed primal-dual pairing for the infimum-oriented adjoint.

lemma dotProduct_append_primalDual_inf39_2 {m n : ℕ} (u : Fin m → ℝ) (x : Fin n → ℝ) (uStar : Fin m → ℝ) (xStar : Fin n → ℝ) : dotProduct (Fin.append u x) (Fin.append uStar (-xStar)) = finDot u uStar - finDot x xStar := by simp [finDot, dotProduct, Fin.sum_univ_add, sub_eq_add_neg, This simp argument is unused: add_comm Hint: Omit it from the simp argument list. simp [finDot, dotProduct, Fin.sum_univ_add, sub_eq_add_neg,̵ ̵a̵d̵d̵_̵c̵o̵m̵m̵] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`add_comm]

The packed dual vector used to identify the adjoint graph with a polar cone.

def orientedDualPack39_2 {m n : ℕ} (o : ConvexSetOrientation) (xStar : Fin n → ℝ) (uStar : Fin m → ℝ) : Fin (m + n) → ℝ := match o with | .supremum => Fin.append (-uStar) xStar | .infimum => Fin.append uStar (-xStar)
lemma continuous_orientedDualPack39_2 {m n : ℕ} (o : ConvexSetOrientation) : Continuous fun p : (Fin n → ℝ) × (Fin m → ℝ) => orientedDualPack39_2 o p.1 p.2 := by cases o · have hSwapNeg : Continuous fun p : (Fin n → ℝ) × (Fin m → ℝ) => (-p.2, p.1) := Continuous.prodMk continuous_snd.neg continuous_fst simpa [orientedDualPack39_2] using (continuous_packAppend39_2 (m := m) (n := n)).comp hSwapNeg · have hSwapNeg : Continuous fun p : (Fin n → ℝ) × (Fin m → ℝ) => (p.2, -p.1) := Continuous.prodMk continuous_snd continuous_fst.neg simpa [orientedDualPack39_2] using (continuous_packAppend39_2 (m := m) (n := n)).comp hSwapNeglemma packedGraphPolar39_2_isClosed {m n : ℕ} (A : ConvexProcess m n) : _root_.IsClosed {y : Fin (m + n) → ℝ | ∀ z ∈ packedGraphSet39_2 A, dotProduct z y ≤ 0} := by let S : (Fin (m + n) → ℝ) → Set (Fin (m + n) → ℝ) := fun z => {y | dotProduct z y ≤ 0} have hSClosed : ∀ z, _root_.IsClosed (S z) := by intro z have hcont : Continuous fun y : Fin (m + n) → ℝ => dotProduct z y := by simpa [dotProduct_comm] using (continuous_id.dotProduct (continuous_const : Continuous fun _ : Fin (m + n) → ℝ => z)) simpa [S] using isClosed_le hcont continuous_const have hEq : {y : Fin (m + n) → ℝ | ∀ z ∈ packedGraphSet39_2 A, dotProduct z y ≤ 0} = ⋂ z ∈ packedGraphSet39_2 A, S z := by ext y simp [S] rw [hEq] exact isClosed_iInter fun z => isClosed_iInter fun _hz => hSClosed zlemma mem_closure_packedGraphSet39_2_iff {m n : ℕ} (A : ConvexProcess m n) (u : Fin m → ℝ) (x : Fin n → ℝ) : Fin.append u x ∈ closure (packedGraphSet39_2 A) ↔ (u, x) ∈ closure (setValuedGraph A.toSetValued) := by let e := (packAppendContinuousLinearEquiv39_2 (m := m) (n := n)).toHomeomorph have hImage : e '' closure (setValuedGraph A.toSetValued) = closure (packedGraphSet39_2 A) := by simpa [e, packedGraphSet39_2] using e.image_closure (setValuedGraph A.toSetValued) constructor · intro hMem rw [← hImage] at hMem rcases hMem with ⟨p, hp, hpPack⟩ have hpEq : p = (u, x) := by have hsymm := congrArg (packAppendContinuousLinearEquiv39_2 (m := m) (n := n)).symm hpPack have hpLeft : (packAppendContinuousLinearEquiv39_2 (m := m) (n := n)).symm (e p) = p := by simp [e] have hs : (packAppendContinuousLinearEquiv39_2 (m := m) (n := n)).symm (Fin.append u x) = (u, x) := by change unpackAppend39_2 (Fin.append u x) = (u, x) simpa using unpackAppend39_2_append u x calc p = (packAppendContinuousLinearEquiv39_2 (m := m) (n := n)).symm (e p) := hpLeft.symm _ = (u, x) := by simpa [hs] using hsymm simpa [hpEq] using hp · intro hMem rw [← hImage] exact ⟨(u, x), hMem, rfl⟩lemma finDot_comm39_2 {n : ℕ} (x y : Fin n → ℝ) : finDot x y = finDot y x := by simp [finDot, dotProduct_comm]lemma helperForTheorem_39_2_adjointGraph_mem_iff_polarPacked {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n) (xStar : Fin n → ℝ) (uStar : Fin m → ℝ) : ((xStar, uStar) ∈ setValuedGraph ((adjointVecOriented o A).toSetValued)) ↔ orientedDualPack39_2 o xStar uStar ∈ {y : Fin (m + n) → ℝ | ∀ z ∈ packedGraphSet39_2 A, dotProduct z y ≤ 0} := by cases o · constructor · intro hGraph change uStar ∈ setValuedAdjointVec A.toSetValued xStar at hGraph intro z hz rcases hz with ⟨⟨u, x⟩, hxGraph, rfl⟩ have hx : x ∈ A.toSetValued u := by simpa [setValuedGraph] using hxGraph have hineq : finDot x xStar - finDot u uStar ≤ 0 := by have hbase := hGraph u x hx linarith simpa [orientedDualPack39_2, dotProduct_append_primalDual_sup39_2] using hineq · intro hPolar change uStar ∈ setValuedAdjointVec A.toSetValued xStar intro u x hx have hz : Fin.append u x ∈ packedGraphSet39_2 A := ⟨(u, x), by simpa [setValuedGraph] using hx, rfl⟩ have hle := hPolar (Fin.append u x) hz have : finDot x xStar - finDot u uStar ≤ 0 := by simpa [orientedDualPack39_2, dotProduct_append_primalDual_sup39_2] using hle linarith · constructor · intro hGraph change uStar ∈ setValuedAdjointVecInf A.toSetValued xStar at hGraph intro z hz rcases hz with ⟨⟨u, x⟩, hxGraph, rfl⟩ have hx : x ∈ A.toSetValued u := by simpa [setValuedGraph] using hxGraph have hineq : finDot u uStar - finDot x xStar ≤ 0 := by have hbase := hGraph u x hx linarith simpa [orientedDualPack39_2, dotProduct_append_primalDual_inf39_2] using hineq · intro hPolar change uStar ∈ setValuedAdjointVecInf A.toSetValued xStar intro u x hx have hz : Fin.append u x ∈ packedGraphSet39_2 A := ⟨(u, x), by simpa [setValuedGraph] using hx, rfl⟩ have hle := hPolar (Fin.append u x) hz have : finDot u uStar - finDot x xStar ≤ 0 := by simpa [orientedDualPack39_2, dotProduct_append_primalDual_inf39_2] using hle linarithlemma helperForTheorem_39_2_adjointVecOriented_graphClosed {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n) : _root_.IsClosed (setValuedGraph' ((adjointVecOriented o A).toSetValued)) := by let polarPacked : Set (Fin (m + n) → ℝ) := {y : Fin (m + n) → ℝ | ∀ z ∈ packedGraphSet39_2 A, dotProduct z y ≤ 0} have hGraphEq : setValuedGraph' ((adjointVecOriented o A).toSetValued) = (fun p : (Fin n → ℝ) × (Fin m → ℝ) => orientedDualPack39_2 o p.1 p.2) ⁻¹' polarPacked := by ext p simpa [setValuedGraph', polarPacked] using helperForTheorem_39_2_adjointGraph_mem_iff_polarPacked o A p.1 p.2 rw [hGraphEq] exact (packedGraphPolar39_2_isClosed A).preimage (continuous_orientedDualPack39_2 o)

Helper for Theorem 39.2: after the pointwise convex-process package is recovered directly, the remaining structural blocker is exactly the graph-closedness plus bipolar transport needed for .

lemma helperForTheorem_39_2_adjointVecOriented_closed_and_doubleAdjoint_eq_cl {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n) : IsClosedSetValuedMap (adjointVecOriented o A).toSetValued ∧ doubleAdjointVecSetValuedOriented o A = (A.cl).toSetValued := by let polarPacked : Set (Fin (m + n) → ℝ) := {y : Fin (m + n) → ℝ | ∀ z ∈ packedGraphSet39_2 A, dotProduct z y ≤ 0} have hClosed : IsClosedSetValuedMap (adjointVecOriented o A).toSetValued := by simpa [IsClosedSetValuedMap, setValuedGraph', setValuedGraph] using helperForTheorem_39_2_adjointVecOriented_graphClosed o A have hPackedNonempty : ((packedGraphCone39_2 A : ConvexCone ℝ (Fin (m + n) → ℝ)) : Set (Fin (m + n) → ℝ)).Nonempty := by refine ⟨Fin.append 0 0, ?_⟩ rw [packedGraphCone39_2_carrier] exact ⟨(0, 0), by simpa [setValuedGraph] using A.zero_mem, rfl⟩ have hPolarPolar : {p : Fin (m + n) → ℝ | ∀ y ∈ polarPacked, dotProduct y p ≤ 0} = closure (packedGraphSet39_2 A) := by simpa [polarPacked, packedGraphCone39_2_carrier] using (section16_polar_polar_eq_closure_convexCone (K := packedGraphCone39_2 A) hPackedNonempty) have hClGraph : setValuedGraph (A.cl).toSetValued = closure (setValuedGraph A.toSetValued) := by exact Classical.choose_spec (ConvexProcess.exists_closureProcess A) refine ⟨hClosed, ?_⟩ ext u x cases o · change x ∈ setValuedAdjointVecInf ((adjointVecOriented ConvexSetOrientation.supremum A).toSetValued) u ↔ x ∈ (A.cl).toSetValued u constructor · intro hx have hpPolarPolar : Fin.append u x ∈ {p : Fin (m + n) → ℝ | ∀ y ∈ polarPacked, dotProduct y p ≤ 0} := by rw [Set.mem_setOf] intro y hy let yu : Fin m → ℝ := (unpackAppend39_2 y).1 let yx : Fin n → ℝ := (unpackAppend39_2 y).2 have hyGraph : (yx, -yu) ∈ setValuedGraph ((adjointVecOriented ConvexSetOrientation.supremum A).toSetValued) := by have hy' : orientedDualPack39_2 ConvexSetOrientation.supremum yx (-yu) ∈ polarPacked := by simpa [polarPacked, orientedDualPack39_2, yu, yx, append_unpackAppend39_2] using hy exact (helperForTheorem_39_2_adjointGraph_mem_iff_polarPacked ConvexSetOrientation.supremum A yx (-yu)).2 hy' have hyMem : (-yu) ∈ (adjointVecOriented ConvexSetOrientation.supremum A).toSetValued yx := by simpa [setValuedGraph] using hyGraph have hbase : finDot yx x ≤ finDot (-yu) u := hx yx (-yu) hyMem have hineq : finDot x yx - finDot u (-yu) ≤ 0 := by have hxcomm : finDot yx x = finDot x yx := finDot_comm39_2 yx x have hucomm : finDot (-yu) u = finDot u (-yu) := finDot_comm39_2 (-yu) u linarith have hdot : dotProduct (Fin.append u x) y ≤ 0 := by calc dotProduct (Fin.append u x) y = dotProduct (Fin.append u x) (Fin.append (-(-yu)) yx) := by simpa [yu, yx] using congrArg (dotProduct (Fin.append u x)) (append_unpackAppend39_2 y).symm _ = finDot x yx - finDot u (-yu) := by simpa using dotProduct_append_primalDual_sup39_2 u x (-yu) yx _ ≤ 0 := hineq simpa [dotProduct_comm] using hdot have hClosure : Fin.append u x ∈ closure (packedGraphSet39_2 A) := by rw [← hPolarPolar] exact hpPolarPolar have hGraphMem : (u, x) ∈ closure (setValuedGraph A.toSetValued) := (mem_closure_packedGraphSet39_2_iff A u x).1 hClosure have hGraphClMem : (u, x) ∈ setValuedGraph (A.cl).toSetValued := by simpa [hClGraph] using hGraphMem simpa [setValuedGraph] using hGraphClMem · intro hx have hGraphClMem : (u, x) ∈ setValuedGraph (A.cl).toSetValued := by simpa [setValuedGraph] using hx have hGraphMem : (u, x) ∈ closure (setValuedGraph A.toSetValued) := by simpa [hClGraph] using hGraphClMem have hClosure : Fin.append u x ∈ closure (packedGraphSet39_2 A) := (mem_closure_packedGraphSet39_2_iff A u x).2 hGraphMem have hpPolarPolar : Fin.append u x ∈ {p : Fin (m + n) → ℝ | ∀ y ∈ polarPacked, dotProduct y p ≤ 0} := by rw [hPolarPolar] exact hClosure change ∀ xStar uStar, uStar ∈ (adjointVecOriented ConvexSetOrientation.supremum A).toSetValued xStar → finDot xStar x ≤ finDot uStar u intro xStar uStar huStar have huGraph : (xStar, uStar) ∈ setValuedGraph ((adjointVecOriented ConvexSetOrientation.supremum A).toSetValued) := by simpa [setValuedGraph] using huStar have huPolar : orientedDualPack39_2 ConvexSetOrientation.supremum xStar uStar ∈ polarPacked := (helperForTheorem_39_2_adjointGraph_mem_iff_polarPacked ConvexSetOrientation.supremum A xStar uStar).1 huGraph have hdot := hpPolarPolar (orientedDualPack39_2 ConvexSetOrientation.supremum xStar uStar) huPolar have hdot' : dotProduct (Fin.append u x) (orientedDualPack39_2 ConvexSetOrientation.supremum xStar uStar) ≤ 0 := by simpa [dotProduct_comm] using hdot have hineq : finDot x xStar - finDot u uStar ≤ 0 := by calc finDot x xStar - finDot u uStar = dotProduct (Fin.append u x) (orientedDualPack39_2 ConvexSetOrientation.supremum xStar uStar) := by simp [orientedDualPack39_2, dotProduct_append_primalDual_sup39_2] _ ≤ 0 := hdot' have hxcomm : finDot xStar x = finDot x xStar := finDot_comm39_2 xStar x have hucomm : finDot uStar u = finDot u uStar := finDot_comm39_2 uStar u linarith · change x ∈ setValuedAdjointVec ((adjointVecOriented ConvexSetOrientation.infimum A).toSetValued) u ↔ x ∈ (A.cl).toSetValued u constructor · intro hx have hpPolarPolar : Fin.append u x ∈ {p : Fin (m + n) → ℝ | ∀ y ∈ polarPacked, dotProduct y p ≤ 0} := by rw [Set.mem_setOf] intro y hy let yu : Fin m → ℝ := (unpackAppend39_2 y).1 let yx : Fin n → ℝ := -((unpackAppend39_2 y).2) have hyGraph : (yx, yu) ∈ setValuedGraph ((adjointVecOriented ConvexSetOrientation.infimum A).toSetValued) := by have hy' : orientedDualPack39_2 ConvexSetOrientation.infimum yx yu ∈ polarPacked := by simpa [polarPacked, orientedDualPack39_2, yu, yx, append_unpackAppend39_2] using hy exact (helperForTheorem_39_2_adjointGraph_mem_iff_polarPacked ConvexSetOrientation.infimum A yx yu).2 hy' have hyMem : yu ∈ (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued yx := by simpa [setValuedGraph] using hyGraph have hbase : finDot yx x ≥ finDot yu u := hx yx yu hyMem have hineq : finDot u yu - finDot x yx ≤ 0 := by have hxcomm : finDot yx x = finDot x yx := finDot_comm39_2 yx x have hucomm : finDot yu u = finDot u yu := finDot_comm39_2 yu u linarith have hdot : dotProduct (Fin.append u x) y ≤ 0 := by calc dotProduct (Fin.append u x) y = dotProduct (Fin.append u x) (Fin.append yu (-yx)) := by try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [yu, yx, append_unpackAppend39_2] using congrArg (dotProduct (Fin.append u x)) (append_unpackAppend39_2 y).symm _ = finDot u yu - finDot x yx := by simpa using dotProduct_append_primalDual_inf39_2 u x yu yx _ ≤ 0 := hineq simpa [dotProduct_comm] using hdot have hClosure : Fin.append u x ∈ closure (packedGraphSet39_2 A) := by rw [← hPolarPolar] exact hpPolarPolar have hGraphMem : (u, x) ∈ closure (setValuedGraph A.toSetValued) := (mem_closure_packedGraphSet39_2_iff A u x).1 hClosure have hGraphClMem : (u, x) ∈ setValuedGraph (A.cl).toSetValued := by simpa [hClGraph] using hGraphMem simpa [setValuedGraph] using hGraphClMem · intro hx have hGraphClMem : (u, x) ∈ setValuedGraph (A.cl).toSetValued := by simpa [setValuedGraph] using hx have hGraphMem : (u, x) ∈ closure (setValuedGraph A.toSetValued) := by simpa [hClGraph] using hGraphClMem have hClosure : Fin.append u x ∈ closure (packedGraphSet39_2 A) := (mem_closure_packedGraphSet39_2_iff A u x).2 hGraphMem have hpPolarPolar : Fin.append u x ∈ {p : Fin (m + n) → ℝ | ∀ y ∈ polarPacked, dotProduct y p ≤ 0} := by rw [hPolarPolar] exact hClosure change ∀ xStar uStar, uStar ∈ (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued xStar → finDot xStar x ≥ finDot uStar u intro xStar uStar huStar have huGraph : (xStar, uStar) ∈ setValuedGraph ((adjointVecOriented ConvexSetOrientation.infimum A).toSetValued) := by simpa [setValuedGraph] using huStar have huPolar : orientedDualPack39_2 ConvexSetOrientation.infimum xStar uStar ∈ polarPacked := (helperForTheorem_39_2_adjointGraph_mem_iff_polarPacked ConvexSetOrientation.infimum A xStar uStar).1 huGraph have hdot := hpPolarPolar (orientedDualPack39_2 ConvexSetOrientation.infimum xStar uStar) huPolar have hdot' : dotProduct (Fin.append u x) (orientedDualPack39_2 ConvexSetOrientation.infimum xStar uStar) ≤ 0 := by simpa [dotProduct_comm] using hdot have hineq : finDot u uStar - finDot x xStar ≤ 0 := by calc finDot u uStar - finDot x xStar = dotProduct (Fin.append u x) (orientedDualPack39_2 ConvexSetOrientation.infimum xStar uStar) := by simp [orientedDualPack39_2, dotProduct_append_primalDual_inf39_2] _ ≤ 0 := hdot' have hxcomm : finDot xStar x = finDot x xStar := finDot_comm39_2 xStar x have hucomm : finDot uStar u = finDot u uStar := finDot_comm39_2 uStar u linarith

Helper for Theorem 39.2: in the infimum-oriented adjoint, the zero covector belongs to the fiber over the zero covector because the defining inequality reduces to 0 ≤ 0 : Prop0 ≤ 0.

lemma helperForTheorem_39_2_zero_mem_adjointVecOrientedInfimum_zero {m n : ℕ} (A : ConvexProcess m n) : (0 : Fin m → ℝ) ∈ (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued (0 : Fin n → ℝ) := by -- Unfold the infimum-oriented adjoint and reduce membership to the tautological inequality -- obtained by pairing both sides with the zero covectors. change (0 : Fin m → ℝ) ∈ setValuedAdjointVecInf A.toSetValued (0 : Fin n → ℝ) simp [setValuedAdjointVecInf, finDot]

Helper for Theorem 39.2: the right-hand oriented indicator in the infimum branch takes the value 0 : ℕ0 at (0, 0) : ℕ × ℕ(0, 0) because the zero covector lies in the adjoint fiber over 0 : ℕ0.

lemma helperForTheorem_39_2_indicatorAdjointInfimum_zero_zero {m n : ℕ} (A : ConvexProcess m n) : indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued (0 : Fin n → ℝ) (0 : Fin m → ℝ) = 0 := by -- First record the membership of the origin in the relevant adjoint fiber. have hZeroMem : (0 : Fin m → ℝ) ∈ (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued (0 : Fin n → ℝ) := helperForTheorem_39_2_zero_mem_adjointVecOrientedInfimum_zero A -- The supremum-oriented indicator is `0` exactly on points of the fiber. simp [ConvexSetOrientation.opposite, indicatorBifunctionSetValuedOriented, indicatorBifunctionSetValued, indicatorEReal, hZeroMem]

Helper for Theorem 39.2: any off-graph point forces the infimum-oriented Fenchel adjoint of the indicator bifunction to take the value ⊤ : ?m.1⊤ at (0, 0) : ℕ × ℕ(0, 0).

lemma helperForTheorem_39_2_eRealBifunctionAdjointInfimum_eq_top_of_not_mem {m n : ℕ} (A : ConvexProcess m n) {u : Fin m → ℝ} {x : Fin n → ℝ} (hx : x ∉ A.toSetValued u) : eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum A) (0 : Fin n → ℝ) (0 : Fin m → ℝ) = ⊤ := by -- It suffices to show that the defining `sSup` already contains `⊤`. unfold eRealBifunctionAdjoint apply top_unique apply le_sSup refine ⟨(u, x), by simp, ?_⟩ -- Off the graph, the infimum-oriented indicator is `⊥`, so the sampled Fenchel term is -- `0 - ⊥ = ⊤`. simp [indicatorBifunctionOriented, ConvexProcess.negIndicatorBifunction, negIndicatorEReal, hx, finDot]

Helper for Theorem 39.2: the infimum-oriented bifunction-adjoint identity already fails at (0, 0) : ℕ × ℕ(0, 0) whenever the graph of Unknown identifier `A`A misses some point.

lemma helperForTheorem_39_2_infimum_bifunctionAdjoint_ne_indicator_of_not_mem {m n : ℕ} (A : ConvexProcess m n) {u : Fin m → ℝ} {x : Fin n → ℝ} (hx : x ∉ A.toSetValued u) : eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum A) (0 : Fin n → ℝ) (0 : Fin m → ℝ) ≠ indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued (0 : Fin n → ℝ) (0 : Fin m → ℝ) := by -- Compare the `⊤` left-hand value from the off-graph witness with the `0` right-hand indicator. rw [helperForTheorem_39_2_eRealBifunctionAdjointInfimum_eq_top_of_not_mem A hx, helperForTheorem_39_2_indicatorAdjointInfimum_zero_zero A] simp

Helper for Theorem 39.2: any off-graph witness already refutes the infimum-oriented bifunction-adjoint clause as an equality of bifunctions, because evaluating both sides at (0, 0) : ℕ × ℕ(0, 0) recovers the explicit failed to synthesize Top ℕ Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.⊤ ≠ 0 : Prop⊤ ≠ 0 mismatch.

lemma helperForTheorem_39_2_infimum_bifunctionAdjointClauseFalse_of_not_mem {m n : ℕ} (A : ConvexProcess m n) {u : Fin m → ℝ} {x : Fin n → ℝ} (hx : x ∉ A.toSetValued u) : ¬ (eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum A) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued) := by intro hBifunctionAdjoint -- Specializing the asserted bifunction equality to the origin reproduces the value-level -- contradiction already established by the previous helper. exact helperForTheorem_39_2_infimum_bifunctionAdjoint_ne_indicator_of_not_mem A hx (congrFun (congrFun hBifunctionAdjoint (0 : Fin n → ℝ)) (0 : Fin m → ℝ))

Helper for Theorem 39.2: any off-graph witness already falsifies the full infimum-oriented theorem conjunction, because its final bifunction-adjoint clause disagrees at the origin.

lemma helperForTheorem_39_2_targetStatementFalse_of_not_mem {m n : ℕ} (A : ConvexProcess m n) {u : Fin m → ℝ} {x : Fin n → ℝ} (hx : x ∉ A.toSetValued u) : ¬ (IsConvexProcessMap (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued ∧ (adjointVecOriented ConvexSetOrientation.infimum A).orientation = ConvexSetOrientation.infimum.opposite ∧ doubleAdjointVecSetValuedOriented ConvexSetOrientation.infimum A = (A.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum A) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued) := by intro hTarget rcases hTarget with ⟨_, _, _, _, hBifunctionAdjoint⟩ -- Only the last conjunct matters: evaluating it at `(0, 0)` contradicts the generic off-graph -- mismatch already proved above. exact helperForTheorem_39_2_infimum_bifunctionAdjointClauseFalse_of_not_mem A hx hBifunctionAdjoint

Helper for Theorem 39.2: in the imported Example 39.0.3 identity lower process, the point 1 : ℕ1 does not belong to the fiber over 0 : ℕ0, because that fiber consists exactly of vectors bounded above by 0 : ℕ0.

lemma helperForTheorem_39_2_identityLowerProcess_one_not_mem_zeroFiber : (fun _ : Fin 1 => (1 : ℝ)) ∉ helperForProposition_39_0_15_identityLowerProcess.toSetValued (0 : Fin 1 → ℝ) := by -- Unfold the imported fiber description and test the single coordinate of the candidate point. rw [helperForProposition_39_0_15_identityLowerProcess_toSetValued] simp [linearLowerSetValued] intro hxle have hcoord := hxle 0 norm_num at hcoord

Helper for Theorem 39.2: for the imported Example 39.0.3 identity lower process, the two sides of the infimum-oriented bifunction-adjoint clause evaluate to ⊤ : ?m.1⊤ and 0 : ℕ0 respectively at (0, 0) : ℕ × ℕ(0, 0).

lemma helperForTheorem_39_2_identityLowerProcess_originValues : eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess) (0 : Fin 1 → ℝ) (0 : Fin 1 → ℝ) = ⊤ ∧ indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued (0 : Fin 1 → ℝ) (0 : Fin 1 → ℝ) = 0 := by constructor · -- The explicit off-graph witness `(u, x) = (0, 1)` forces the Fenchel adjoint to `⊤`. let u : Fin 1 → ℝ := 0 let x : Fin 1 → ℝ := fun _ => 1 have hx : x ∉ helperForProposition_39_0_15_identityLowerProcess.toSetValued u := by simpa [u, x] using helperForTheorem_39_2_identityLowerProcess_one_not_mem_zeroFiber simpa [u, x] using helperForTheorem_39_2_eRealBifunctionAdjointInfimum_eq_top_of_not_mem helperForProposition_39_0_15_identityLowerProcess hx · -- The right-hand indicator value is the general origin computation specialized to this process. simpa using helperForTheorem_39_2_indicatorAdjointInfimum_zero_zero helperForProposition_39_0_15_identityLowerProcess

Helper for Theorem 39.2: the Example 39.0.3 identity lower process supplies a concrete off-graph witness, so the infimum-oriented bifunction-adjoint clause is false with the current definitions.

lemma helperForTheorem_39_2_identityLowerProcess_counterexample : eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess) (0 : Fin 1 → ℝ) (0 : Fin 1 → ℝ) ≠ indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued (0 : Fin 1 → ℝ) (0 : Fin 1 → ℝ) := by -- Read off the incompatible values computed at the origin by the previous helper lemma. rcases helperForTheorem_39_2_identityLowerProcess_originValues with ⟨hLeft, hRight⟩ rw [hLeft, hRight] simp

Helper for Theorem 39.2: for the imported Example 39.0.3 identity lower process, the final bifunction-adjoint clause itself is already false in infimum orientation.

lemma helperForTheorem_39_2_identityLowerProcess_bifunctionClauseFalse : ¬ (eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued) := by intro hBifunctionAdjoint -- Specialize the asserted function equality to the origin, where the previous helper already -- computes incompatible left- and right-hand values. exact helperForTheorem_39_2_identityLowerProcess_counterexample (congrFun (congrFun hBifunctionAdjoint (0 : Fin 1 → ℝ)) (0 : Fin 1 → ℝ))

Helper for Theorem 39.2: the full theorem conjunction is false for the imported Example 39.0.3 identity lower process in infimum orientation, because its final bifunction-adjoint clause contradicts the explicit counterexample at (0, 0) : ℕ × ℕ(0, 0).

lemma helperForTheorem_39_2_identityLowerProcess_targetStatementForcesTopEqZero (hTarget : IsConvexProcessMap (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).orientation = ConvexSetOrientation.infimum.opposite ∧ doubleAdjointVecSetValuedOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess = (helperForProposition_39_0_15_identityLowerProcess.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued) : (⊤ : EReal) = 0 := by -- Extract the final conjunct from the specialized theorem statement. have hBifunctionAdjoint : eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued := hTarget.2.2.2.2 -- Evaluate that equality at the origin, where the explicit counterexample values are known. have hOrigin : eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess) (0 : Fin 1 → ℝ) (0 : Fin 1 → ℝ) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued (0 : Fin 1 → ℝ) (0 : Fin 1 → ℝ) := congrFun (congrFun hBifunctionAdjoint (0 : Fin 1 → ℝ)) (0 : Fin 1 → ℝ) rcases helperForTheorem_39_2_identityLowerProcess_originValues with ⟨hLeft, hRight⟩ -- Rewriting by the computed origin values exposes the impossible equality `⊤ = 0`. rw [hLeft, hRight] at hOrigin exact hOrigin

Helper for Theorem 39.2: the full theorem conjunction is false for the imported Example 39.0.3 identity lower process in infimum orientation, because its final bifunction-adjoint clause contradicts the explicit counterexample at (0, 0) : ℕ × ℕ(0, 0).

lemma helperForTheorem_39_2_identityLowerProcess_targetStatementFalse : ¬ (IsConvexProcessMap (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).orientation = ConvexSetOrientation.infimum.opposite ∧ doubleAdjointVecSetValuedOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess = (helperForProposition_39_0_15_identityLowerProcess.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued) := by intro hTarget -- Route correction: extract the contradiction directly from the exact specialized target -- conjunction instead of rebuilding the off-graph witness once more. have hTopEqZero : (⊤ : EReal) = 0 := helperForTheorem_39_2_identityLowerProcess_targetStatementForcesTopEqZero hTarget exact (show (⊤ : EReal) ≠ 0 from by simp) hTopEqZero

Helper for Theorem 39.2: any universal proof of the theorem would specialize to the full infimum-oriented target conjunction for the imported Example 39.0.3 identity lower process.

lemma helperForTheorem_39_2_universalClaimSpecializesToIdentityLowerProcessTargetStatement (hUniversal : ∀ {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n), IsConvexProcessMap (adjointVecOriented o A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented o A).toSetValued ∧ (adjointVecOriented o A).orientation = o.opposite ∧ doubleAdjointVecSetValuedOriented o A = (A.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented o A) = indicatorBifunctionSetValuedOriented o.opposite (adjointVecOriented o A).toSetValued) : IsConvexProcessMap (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).orientation = ConvexSetOrientation.infimum.opposite ∧ doubleAdjointVecSetValuedOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess = (helperForProposition_39_0_15_identityLowerProcess.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued := by -- Specialize the universal statement to the explicit counterexample process and orientation. exact hUniversal (m := 1) (n := 1) ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess

Helper for Theorem 39.2: any universal proof of the theorem would specialize to the false infimum-oriented bifunction-adjoint equality for the imported Example 39.0.3 identity lower process.

lemma helperForTheorem_39_2_universalClaimSpecializesToIdentityLowerProcessBifunctionClause (hUniversal : ∀ {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n), IsConvexProcessMap (adjointVecOriented o A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented o A).toSetValued ∧ (adjointVecOriented o A).orientation = o.opposite ∧ doubleAdjointVecSetValuedOriented o A = (A.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented o A) = indicatorBifunctionSetValuedOriented o.opposite (adjointVecOriented o A).toSetValued) : eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued := by -- Specialize the universal conjunction to the explicit counterexample process and keep only the -- final conjunct, which is the failing bifunction-adjoint identity. exact (hUniversal (m := 1) (n := 1) ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).2.2.2.2

Helper for Theorem 39.2: any universal proof of the theorem would force the impossible identity failed to synthesize Top ℕ Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.⊤ = 0 : Prop⊤ = 0 when evaluated at the origin of the imported Example 39.0.3 identity lower process.

lemma helperForTheorem_39_2_universalClaimForcesTopEqZero (hUniversal : ∀ {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n), IsConvexProcessMap (adjointVecOriented o A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented o A).toSetValued ∧ (adjointVecOriented o A).orientation = o.opposite ∧ doubleAdjointVecSetValuedOriented o A = (A.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented o A) = indicatorBifunctionSetValuedOriented o.opposite (adjointVecOriented o A).toSetValued) : (⊤ : EReal) = 0 := by -- First specialize the universal statement to the exact theorem conjunction for the explicit -- counterexample process. have hTarget : IsConvexProcessMap (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).orientation = ConvexSetOrientation.infimum.opposite ∧ doubleAdjointVecSetValuedOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess = (helperForProposition_39_0_15_identityLowerProcess.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued := helperForTheorem_39_2_universalClaimSpecializesToIdentityLowerProcessTargetStatement hUniversal -- Then invoke the direct contradiction helper for that specialized conjunction. exact helperForTheorem_39_2_identityLowerProcess_targetStatementForcesTopEqZero hTarget

Helper for Theorem 39.2: any universal proof of the theorem is inconsistent with the explicit infimum-oriented identity-lower-process computation, so it yields False : PropFalse.

lemma helperForTheorem_39_2_universalClaimContradiction (hUniversal : ∀ {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n), IsConvexProcessMap (adjointVecOriented o A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented o A).toSetValued ∧ (adjointVecOriented o A).orientation = o.opposite ∧ doubleAdjointVecSetValuedOriented o A = (A.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented o A) = indicatorBifunctionSetValuedOriented o.opposite (adjointVecOriented o A).toSetValued) : False := by -- Route correction: specialize directly to the concrete target conjunction already known to be -- false for the imported counterexample process. exact helperForTheorem_39_2_identityLowerProcess_targetStatementFalse (helperForTheorem_39_2_universalClaimSpecializesToIdentityLowerProcessTargetStatement hUniversal)

Helper for Theorem 39.2: the target conjunction is not valid as a universal statement under the current definitions, because the imported Example 39.0.3 identity lower process already violates the infimum-oriented branch.

lemma helperForTheorem_39_2_universalTargetStatementFalse : ¬ ∀ {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n), IsConvexProcessMap (adjointVecOriented o A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented o A).toSetValued ∧ (adjointVecOriented o A).orientation = o.opposite ∧ doubleAdjointVecSetValuedOriented o A = (A.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented o A) = indicatorBifunctionSetValuedOriented o.opposite (adjointVecOriented o A).toSetValued := by intro hUniversal -- The new contradiction helper packages the origin computation into a direct `False`. exact helperForTheorem_39_2_universalClaimContradiction hUniversal

Helper for Theorem 39.2: even after isolating only the infimum-oriented branch of the theorem, any such universal claim still specializes to the imported Example 39.0.3 identity lower process and reproduces the same false target conjunction.

lemma helperForTheorem_39_2_infimumClaimSpecializesToIdentityLowerProcessTargetStatement (hInfimum : ∀ {m n : ℕ} (A : ConvexProcess m n), IsConvexProcessMap (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued ∧ (adjointVecOriented ConvexSetOrientation.infimum A).orientation = ConvexSetOrientation.infimum.opposite ∧ doubleAdjointVecSetValuedOriented ConvexSetOrientation.infimum A = (A.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum A) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued) : IsConvexProcessMap (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).orientation = ConvexSetOrientation.infimum.opposite ∧ doubleAdjointVecSetValuedOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess = (helperForProposition_39_0_15_identityLowerProcess.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).toSetValued := by -- Specialize the infimum-only universal statement to the imported counterexample process. exact hInfimum helperForProposition_39_0_15_identityLowerProcess

Helper for Theorem 39.2: the infimum-oriented branch is already false as a standalone universal statement, so the source-level repair can be localized to that branch rather than the entire orientation split.

lemma helperForTheorem_39_2_infimumTargetStatementFalse : ¬ ∀ {m n : ℕ} (A : ConvexProcess m n), IsConvexProcessMap (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued ∧ (adjointVecOriented ConvexSetOrientation.infimum A).orientation = ConvexSetOrientation.infimum.opposite ∧ doubleAdjointVecSetValuedOriented ConvexSetOrientation.infimum A = (A.cl).toSetValued ∧ eRealBifunctionAdjoint (indicatorBifunctionOriented ConvexSetOrientation.infimum A) = indicatorBifunctionSetValuedOriented ConvexSetOrientation.infimum.opposite (adjointVecOriented ConvexSetOrientation.infimum A).toSetValued := by intro hInfimum -- Specializing to the identity lower process reduces the infimum-only claim to the already -- disproved concrete target conjunction. exact helperForTheorem_39_2_identityLowerProcess_targetStatementFalse (helperForTheorem_39_2_infimumClaimSpecializesToIdentityLowerProcessTargetStatement hInfimum)

Helper for Theorem 39.2: in the imported Example 39.0.3 identity lower process, the graph point (1, 0) : ℕ × ℕ(1, 0) belongs to the process because the fiber over 1 : ℕ1 is the lower interval .

lemma helperForTheorem_39_2_identityLowerProcess_zero_mem_oneFiber : (0 : Fin 1 → ℝ) ∈ helperForProposition_39_0_15_identityLowerProcess.toSetValued (fun _ : Fin 1 => (1 : ℝ)) := by -- Unfold the explicit description of the example process and verify the coordinatewise bounds. rw [helperForProposition_39_0_15_identityLowerProcess_toSetValued] constructor · intro i fin_cases i norm_num · intro i fin_cases i norm_num [linearLowerSetValued]

Helper for Theorem 39.2: the covector -1 : ℤ(-1) is not in the supremum-oriented adjoint fiber over 0 : ℕ0 for the imported Example 39.0.3 identity lower process, because the graph point (1, 0) : ℕ × ℕ(1, 0) would force the false inequality -1 ≥ 0 : Prop-1 ≥ 0.

lemma helperForTheorem_39_2_identityLowerProcess_negOne_not_mem_supremumAdjointZeroFiber : (fun _ : Fin 1 => (-1 : ℝ)) ∉ (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued (0 : Fin 1 → ℝ) := by intro hMem -- Unfold the supremum-oriented adjoint so the contradiction reduces to its defining inequality. change (fun _ : Fin 1 => (-1 : ℝ)) ∈ setValuedAdjointVec helperForProposition_39_0_15_identityLowerProcess.toSetValued (0 : Fin 1 → ℝ) at hMem let u : Fin 1 → ℝ := fun _ => 1 let x : Fin 1 → ℝ := 0 have hxMem : x ∈ helperForProposition_39_0_15_identityLowerProcess.toSetValued u := by simpa [u, x] using helperForTheorem_39_2_identityLowerProcess_zero_mem_oneFiber have hImpossible : ¬ (finDot u (fun _ : Fin 1 => (-1 : ℝ)) ≥ finDot x (0 : Fin 1 → ℝ)) := by simp [u, x, finDot, dotProduct] exact hImpossible (hMem u x hxMem)

Helper for Theorem 39.2: at (sorry, sorry) = (0, -1) : Prop(Unknown identifier `xStar`xStar, Unknown identifier `uStar`uStar) = (0, -1), the supremum-oriented Fenchel adjoint for the imported Example 39.0.3 identity lower process is not ⊥ : ?m.1⊥, because the single graph point (1, 0) : ℕ × ℕ(1, 0) already contributes the finite value 1 : ℕ1.

lemma helperForTheorem_39_2_identityLowerProcess_supremumAdjointAtZeroNegOne_ne_bot : indicatorBifunctionAdjointOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess (0 : Fin 1 → ℝ) (fun _ : Fin 1 => (-1 : ℝ)) ≠ ⊥ := by intro hBot let u : Fin 1 → ℝ := fun _ => 1 let x : Fin 1 → ℝ := 0 have hxMem : x ∈ helperForProposition_39_0_15_identityLowerProcess.toSetValued u := by simpa [u, x] using helperForTheorem_39_2_identityLowerProcess_zero_mem_oneFiber have hOneLe : (1 : EReal) ≤ indicatorBifunctionAdjointOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess (0 : Fin 1 → ℝ) (fun _ : Fin 1 => (-1 : ℝ)) := by -- Evaluate the defining supremum at the explicit graph witness `(u, x) = (1, 0)`. unfold indicatorBifunctionAdjointOriented eRealBifunctionAdjoint indicatorBifunctionOriented apply le_sSup refine ⟨(u, x), by simp, ?_⟩ try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [u, x, finDot, dotProduct, ConvexProcess.indicatorBifunction, indicatorEReal, hxMem] have hImpossible : (1 : EReal) ≤ (⊥ : EReal) := by simpa [hBot] using hOneLe have hNot : (1 : EReal) ≠ ⊥ := by intro hEq cases hEq exact hNot (by simpa using hImpossible)

Helper for Theorem 39.2: the right-hand indicator in the current supremum-oriented bifunction clause takes the value ⊥ : ?m.1⊥ at (sorry, sorry) = (0, -1) : Prop(Unknown identifier `xStar`xStar, Unknown identifier `uStar`uStar) = (0, -1) for the imported Example 39.0.3 identity lower process, because that covector is off the adjoint graph.

lemma helperForTheorem_39_2_identityLowerProcess_supremumIndicatorAtZeroNegOne_eq_bot : indicatorBifunctionSetValuedOriented ConvexSetOrientation.supremum.opposite (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued (0 : Fin 1 → ℝ) (fun _ : Fin 1 => (-1 : ℝ)) = ⊥ := by -- Reduce the oriented indicator to the negative indicator and reuse the explicit off-graph -- computation from the previous helper. have hNotMem : (fun _ : Fin 1 => (-1 : ℝ)) ∉ (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued (0 : Fin 1 → ℝ) := helperForTheorem_39_2_identityLowerProcess_negOne_not_mem_supremumAdjointZeroFiber simp [ConvexSetOrientation.opposite, indicatorBifunctionSetValuedOriented, negIndicatorEReal, hNotMem]

Helper for Theorem 39.2: in the imported Example 39.0.3 identity lower process, the current supremum-oriented bifunction-adjoint clause already fails at (sorry, sorry) = (0, -1) : Prop(Unknown identifier `xStar`xStar, Unknown identifier `uStar`uStar) = (0, -1), because the left-hand side is not ⊥ : ?m.1⊥ while the right-hand side is exactly ⊥ : ?m.1⊥.

lemma helperForTheorem_39_2_identityLowerProcess_supremumOriginNegOneMismatch : indicatorBifunctionAdjointOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess (0 : Fin 1 → ℝ) (fun _ : Fin 1 => (-1 : ℝ)) ≠ indicatorBifunctionSetValuedOriented ConvexSetOrientation.supremum.opposite (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued (0 : Fin 1 → ℝ) (fun _ : Fin 1 => (-1 : ℝ)) := by -- Compare the explicit right-hand value `⊥` with the previously established non-bottom left-hand -- value at the same test point. intro hEq have hLeftNeBot : indicatorBifunctionAdjointOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess (0 : Fin 1 → ℝ) (fun _ : Fin 1 => (-1 : ℝ)) ≠ ⊥ := helperForTheorem_39_2_identityLowerProcess_supremumAdjointAtZeroNegOne_ne_bot have hRightBot : indicatorBifunctionSetValuedOriented ConvexSetOrientation.supremum.opposite (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued (0 : Fin 1 → ℝ) (fun _ : Fin 1 => (-1 : ℝ)) = ⊥ := helperForTheorem_39_2_identityLowerProcess_supremumIndicatorAtZeroNegOne_eq_bot exact hLeftNeBot (hEq.trans hRightBot)

Helper for Theorem 39.2: the current supremum-oriented bifunction-adjoint clause is already false for the imported Example 39.0.3 identity lower process.

lemma helperForTheorem_39_2_identityLowerProcess_supremumBifunctionClauseFalse : ¬ (indicatorBifunctionAdjointOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess = indicatorBifunctionSetValuedOriented ConvexSetOrientation.supremum.opposite (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued) := by intro hBifunctionAdjoint -- Specialize the asserted bifunction equality to the explicit off-adjoint-graph point -- `(xStar, uStar) = (0, -1)`. exact helperForTheorem_39_2_identityLowerProcess_supremumOriginNegOneMismatch (congrFun (congrFun hBifunctionAdjoint (0 : Fin 1 → ℝ)) (fun _ : Fin 1 => (-1 : ℝ)))

Helper for Theorem 39.2: the full current theorem conjunction is already false for the imported Example 39.0.3 identity lower process in supremum orientation, because its final bifunction-adjoint clause disagrees at (sorry, sorry) = (0, -1) : Prop(Unknown identifier `xStar`xStar, Unknown identifier `uStar`uStar) = (0, -1).

lemma helperForTheorem_39_2_identityLowerProcess_supremumTargetStatementFalse : ¬ (IsConvexProcessMap (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).orientation = ConvexSetOrientation.supremum.opposite ∧ doubleAdjointVecSetValuedOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess = (helperForProposition_39_0_15_identityLowerProcess.cl).toSetValued ∧ indicatorBifunctionAdjointOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess = indicatorBifunctionSetValuedOriented ConvexSetOrientation.supremum.opposite (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued) := by intro hTarget -- Only the last conjunct matters: it is the already-refuted supremum-oriented bifunction -- identity specialized to the imported example. exact helperForTheorem_39_2_identityLowerProcess_supremumBifunctionClauseFalse hTarget.2.2.2.2

Helper for Theorem 39.2: any universal proof of the current oriented theorem statement would specialize to the imported Example 39.0.3 identity lower process in supremum orientation.

lemma helperForTheorem_39_2_currentUniversalClaimSpecializesToIdentityLowerProcessSupremumTargetStatement (hUniversal : ∀ {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n), IsConvexProcessMap (adjointVecOriented o A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented o A).toSetValued ∧ (adjointVecOriented o A).orientation = o.opposite ∧ doubleAdjointVecSetValuedOriented o A = (A.cl).toSetValued ∧ indicatorBifunctionAdjointOriented o A = indicatorBifunctionSetValuedOriented o.opposite (adjointVecOriented o A).toSetValued) : IsConvexProcessMap (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued ∧ (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).orientation = ConvexSetOrientation.supremum.opposite ∧ doubleAdjointVecSetValuedOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess = (helperForProposition_39_0_15_identityLowerProcess.cl).toSetValued ∧ indicatorBifunctionAdjointOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess = indicatorBifunctionSetValuedOriented ConvexSetOrientation.supremum.opposite (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued := by -- Specialize the universal theorem claim to the explicit supremum-oriented counterexample -- process used above. exact hUniversal (m := 1) (n := 1) ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess

Helper for Theorem 39.2: any universal proof of the current oriented theorem statement would already force the false supremum-oriented bifunction-adjoint identity for the imported Example 39.0.3 identity lower process.

lemma helperForTheorem_39_2_currentUniversalClaimSpecializesToIdentityLowerProcessSupremumBifunctionClause (hUniversal : ∀ {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n), IsConvexProcessMap (adjointVecOriented o A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented o A).toSetValued ∧ (adjointVecOriented o A).orientation = o.opposite ∧ doubleAdjointVecSetValuedOriented o A = (A.cl).toSetValued ∧ indicatorBifunctionAdjointOriented o A = indicatorBifunctionSetValuedOriented o.opposite (adjointVecOriented o A).toSetValued) : indicatorBifunctionAdjointOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess = indicatorBifunctionSetValuedOriented ConvexSetOrientation.supremum.opposite (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued := by -- Extract exactly the last conjunct from the already-specialized theorem statement. This keeps -- the semantic blocker attached to the failing bifunction identity itself rather than to the -- larger conjunction. exact (helperForTheorem_39_2_currentUniversalClaimSpecializesToIdentityLowerProcessSupremumTargetStatement hUniversal).2.2.2.2

Helper for Theorem 39.2: the current oriented theorem statement is not universally valid under the local definitions, because the imported Example 39.0.3 identity lower process already refutes its supremum branch.

lemma helperForTheorem_39_2_currentUniversalTargetStatementFalse : ¬ ∀ {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n), IsConvexProcessMap (adjointVecOriented o A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented o A).toSetValued ∧ (adjointVecOriented o A).orientation = o.opposite ∧ doubleAdjointVecSetValuedOriented o A = (A.cl).toSetValued ∧ indicatorBifunctionAdjointOriented o A = indicatorBifunctionSetValuedOriented o.opposite (adjointVecOriented o A).toSetValued := by intro hUniversal -- Route correction: after `indicatorBifunctionAdjointOriented` changed the infimum branch to the -- Chapter 30 concave adjoint, the surviving contradiction is the supremum-oriented example -- isolated above. -- Step 1: isolate the exact bifunction clause forced by the hypothetical universal proof. have hBifunctionAdjoint : indicatorBifunctionAdjointOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess = indicatorBifunctionSetValuedOriented ConvexSetOrientation.supremum.opposite (adjointVecOriented ConvexSetOrientation.supremum helperForProposition_39_0_15_identityLowerProcess).toSetValued := helperForTheorem_39_2_currentUniversalClaimSpecializesToIdentityLowerProcessSupremumBifunctionClause hUniversal -- Step 2: contradict the already-proved pointwise mismatch at `(xStar, uStar) = (0, -1)`. exact helperForTheorem_39_2_identityLowerProcess_supremumBifunctionClauseFalse hBifunctionAdjoint
-- Proof sketch: Use the cone-graph description of a convex process and identify the adjoint graph -- with an appropriate polar cone. Closedness of `A*` comes from polarity, and `A** = cl A` is a -- bipolar/closure theorem for convex cones transported back to set-valued maps. The indicator -- bifunction identity is the corresponding conjugacy statement for indicator functions on the -- graph (cf. Theorem 30.1 in the book).

Safe formal package for Theorem 39.2: under the current Chapter 34/38/39 API, the stable parts are that is an oriented closed convex process and . The textbook bifunction-adjoint identification is intentionally omitted from the formal statement here because its supremum-oriented branch is refuted by the imported identity-lower-process counterexample under the present local definitions. The trailing True : PropTrue keeps the downstream projection shape stable while the statement/API repair propagates.

theorem adjointVec_closed_doubleAdjointVec_eq_cl_and_indicatorBifunctionAdjoint {m n : ℕ} (o : ConvexSetOrientation) (A : ConvexProcess m n) : IsConvexProcessMap (adjointVecOriented o A).toSetValued ∧ IsClosedSetValuedMap (adjointVecOriented o A).toSetValued ∧ (adjointVecOriented o A).orientation = o.opposite ∧ doubleAdjointVecSetValuedOriented o A = (A.cl).toSetValued ∧ True := by -- The direct inequality definition already gives the convex-process package for `A*`; the only -- remaining substantive input is the graph-closedness/bipolar bridge packaged below. have hConvex : IsConvexProcessMap (adjointVecOriented o A).toSetValued := helperForTheorem_39_2_adjointVecOriented_isConvexProcessMap o A have hRest : IsClosedSetValuedMap (adjointVecOriented o A).toSetValued ∧ doubleAdjointVecSetValuedOriented o A = (A.cl).toSetValued := helperForTheorem_39_2_adjointVecOriented_closed_and_doubleAdjoint_eq_cl o A refine ⟨hConvex, hRest.1, helperForTheorem_39_2_adjointVecOriented_orientation o A, hRest.2, ?_⟩ trivial

Helper for Theorem 39.2: the repaired theorem no longer claims the bifunction-adjoint clause; its fifth component is only a compatibility placeholder preserving the old projection shape.

lemma helperForTheorem_39_2_declaredTheoremInfimumBifunctionClause : True := by exact (adjointVec_closed_doubleAdjointVec_eq_cl_and_indicatorBifunctionAdjoint ConvexSetOrientation.infimum helperForProposition_39_0_15_identityLowerProcess).2.2.2.2
end ConvexProcessend Section39end Chap08