theorem ConvexProcess.helperForTheorem_39_4_parameterSection_superadditive {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hConc : ∀ (xStar : Fin n → ℝ), IsERealConcaveOn Set.univ fun (u : Fin m → ℝ) => K u xStar) (hNoBot : HasNoBotValuesBifunction K) (hHom : IsNormalizedBihomogeneousERealBifunction K) (u₁ u₂ : Fin m → ℝ) (xStar : Fin n → ℝ) : K u₁ xStar + K u₂ xStar ≤ K (u₁ + u₂) xStar

Helper for Theorem 39.4: for a fixed covector x*, concavity of the parameter section u ↦ K(u,x*), together with positive homogeneity and the exclusion of ⊥, yields the superadditivity inequality needed for the reconstructed process law.

theorem ConvexProcess.helperForTheorem_39_4_processMapOfBifunction_map_add_superset {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hK : IsLowerClosedConcaveConvexPosHomBifunction K) (hNoBot : HasNoBotValuesBifunction K) (u₁ u₂ : Fin m → ℝ) : processMapOfBifunction K u₁ + processMapOfBifunction K u₂ ⊆ processMapOfBifunction K (u₁ + u₂)

Helper for Theorem 39.4: the half-space reconstruction is superadditive once the parameter sections of K are concave and positively homogeneous.

noncomputable def ConvexProcess.processOfLowerClosedConcaveConvexPosHomBifunction {m n : ℕ} (hQualification : Section39Theorem39_4GlobalQualification m n) (K : LowerClosedConcaveConvexPosHomBifunction m n) : ClosedConvexProcess m n

The reverse reconstruction of Theorem 39.4: from a lower-closed concave-convex bihomogeneous kernel K, build the candidate closed convex process A_K u = {x | ⟪x,x*⟫ ≤ K(u,x*), ∀ x*}.

theorem ConvexProcess.helperForTheorem_39_4_leftInverse {m n : ℕ} (hQualification : Section39Theorem39_4GlobalQualification m n) : Function.LeftInverse (fun (A : ClosedConvexProcess m n) => ⟨(↑A).bracketBifunctionOfProcess, ⋯⟩) (processOfLowerClosedConcaveConvexPosHomBifunction hQualification)

Helper for Theorem 39.4: the canonical reverse reconstruction K ↦ A_K followed by the canonical bracket recovery A ↦ K_A returns the original bihomogeneous kernel fiberwise.

theorem ConvexProcess.helperForTheorem_39_4_rightInverse {m n : ℕ} (hQualification : Section39Theorem39_4GlobalQualification m n) : Function.RightInverse (fun (A : ClosedConvexProcess m n) => ⟨(↑A).bracketBifunctionOfProcess, ⋯⟩) (processOfLowerClosedConcaveConvexPosHomBifunction hQualification)

Helper for Theorem 39.4: the canonical forward reconstruction A ↦ K_A ↦ A_{K_A} recovers each closed convex fiber, hence the original process.

theorem ConvexProcess.theorem_39_4 {m n : ℕ} (hQualification : Section39Theorem39_4GlobalQualification m n) : ∃ (toProcess : LowerClosedConcaveConvexPosHomBifunction m n → ClosedConvexProcess m n) (toBifunction : ClosedConvexProcess m n → LowerClosedConcaveConvexPosHomBifunction m n), (∀ (A : ClosedConvexProcess m n), ↑(toBifunction A) = (↑A).bracketBifunctionOfProcess) ∧ (∀ (K : LowerClosedConcaveConvexPosHomBifunction m n), (↑(toProcess K)).toSetValued = processMapOfBifunction ↑K) ∧ Function.LeftInverse toBifunction toProcess ∧ Function.RightInverse toBifunction toProcess

Theorem 39.4: The relations

K(u, x*) = ⟪A u, x*⟫ and A u = {x | ⟪x, x*⟫ ≤ K(u, x*), ∀ x*}

define a one-to-one correspondence between lower closed concave-convex bifunctions K : ℝ^m × ℝ^n → [-∞,+∞] with K(0,0)=0 and positive homogeneity K(r•u,x*) = r K(u,x*) = K(u,r•x*) for all r>0, and supremum-oriented closed convex processes A : ℝ^m ⇉ ℝ^n. (Similarly for upper closed convex-concave functions and infimum oriented convex processes.)