Convex Analysis (Rockafellar, 1970) -- Chapter 07 -- Section 34 -- Part 16

section Chap07section Section34open Setsection SaddleAmbientvariable {m n : ℕ}

Theorem 34.2, generated-class core: is the saddle-equivalence class generated by the canonical kernel, and the canonical kernel is a member of that class.

The additional adjoint, closed-representative, and realization conclusions in the prose theorem need their corresponding closedness or realization qualifications; they are exposed separately by the qualified projection API below rather than being asserted for arbitrary representatives.

theorem section34_theorem34_2
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F) :
    omegaClassOfConvexBifunction F =
        EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ ∧
      omegaClassOfConvexBifunction F =
        {K | saddleEquivalent K (convexBifunctionClosedKernel F)} ∧
      convexBifunctionClosedKernel F ∈ omegaClassOfConvexBifunction F := by
  have hKernelConcaveConvex : IsConcaveConvex (convexBifunctionClosedKernel F) := by
    exact (closedSaddleFunctions_imageClosedBifunctions_correspondence.1 F hF).1
  have hKernelSelf :
      saddleEquivalent (convexBifunctionClosedKernel F) (convexBifunctionClosedKernel F) :=
    ⟨hKernelConcaveConvex, hKernelConcaveConvex, rfl, rfl⟩
  constructor
  · rfl
  constructor
  · rfl
  exact hKernelSelf

The data attached by Theorem 34.2 to a closed representative of the generated class.

def Section34Theorem34_2ClosedRepresentativeData
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (K : SaddleFunction m n) : Prop :=
  partialClosure₁ K = convexBifunctionClosedKernel F ∧
    partialClosure₂ K = convexBifunctionClosedKernel F ∧
    saddleEffectiveDomain K =
      convexBifunctionDomain F ×ˢ convexBifunctionKernelAdjointDomain F ∧
    (∀ u x, F u x = convexConjugate (K u) x) ∧
    (∀ xStar uStar,
      section34ConcaveBifunctionAdjoint F xStar uStar =
        concaveConjugate (fun u => K u xStar) uStar) ∧
    ∀ u xStar,
      u ∈ intrinsicInterior ℝ (convexBifunctionDomain F) ∨
          xStar ∈ intrinsicInterior ℝ (convexBifunctionKernelAdjointDomain F) →
        K u xStar = convexBifunctionClosedKernel F u xStar

Explicit qualifications for the adjoint and closed-representative parts of Theorem 34.2. The representative data is deliberately required only after closedness of that representative has been supplied.

structure Section34Theorem34_2Qualification
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop where
  adjointPairing_eq :
    convexBifunctionClosedKernel F = section34ConcaveBifunctionAdjointPairing F
  adjoint_graphClosed :
    IsFunctionConcaveClosed
      (graphFunctionOfBifunction (section34ConcaveBifunctionAdjoint F))
  adjoint_imageClosed :
    IsImageClosedConcaveBifunction (section34ConcaveBifunctionAdjoint F)
  canonicalKernel_closed : IsClosedSaddleFunction (convexBifunctionClosedKernel F)
  closedRepresentativeData : ∀ K : SaddleFunction m n,
    K ∈ omegaClassOfConvexBifunction F → IsClosedSaddleFunction K →
      Section34Theorem34_2ClosedRepresentativeData F K

Explicit qualification for the converse realization part of Theorem 34.2.

def Section34Theorem34_2UniqueRealizationQualification (m n : ℕ) : Prop :=
  ∀ Omega : Set (SaddleFunction m n),
    IsClosedConcaveConvexEquivalenceClass Omega →
      ∃! G : (Fin m → ℝ) → (Fin n → ℝ) → EReal,
        IsClosedConvexBifunction G ∧ Omega = omegaClassOfConvexBifunction G

Dimension-wide qualification used by the converse and characterization projections.

structure Section34Theorem34_2GlobalQualification (m n : ℕ) : Prop where
  qualification : ∀ (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal),
    IsClosedConvexBifunction F → Section34Theorem34_2Qualification F
  uniqueRealization : Section34Theorem34_2UniqueRealizationQualification m n
  canonicalClosureRealization : Section34CanonicalClosureRealizationQualification m n

Qualified full projection package for Theorem 34.2. Its generated-class core is supplied by section34_theorem34_2 {m n : ℕ} (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) : omegaClassOfConvexBifunction F = EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ ∧ omegaClassOfConvexBifunction F = {K | saddleEquivalent K (convexBifunctionClosedKernel F)} ∧ convexBifunctionClosedKernel F ∈ omegaClassOfConvexBifunction Fsection34_theorem34_2; the stronger conclusions are exactly the explicit qualifications above.

theorem section34_theorem34_2_qualified
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F)
    (hQ : Section34Theorem34_2Qualification F) :
    convexBifunctionClosedKernel F = section34ConcaveBifunctionAdjointPairing F ∧
      omegaClassOfConvexBifunction F =
        {K | saddleEquivalent K (convexBifunctionClosedKernel F)} ∧
      convexBifunctionClosedKernel F ∈ omegaClassOfConvexBifunction F ∧
      (∀ K : SaddleFunction m n,
        K ∈ omegaClassOfConvexBifunction F → IsClosedSaddleFunction K) ∧
      ∀ K : SaddleFunction m n,
        K ∈ omegaClassOfConvexBifunction F →
          Section34Theorem34_2ClosedRepresentativeData F K := by
  have hCore := section34_theorem34_2 F hF
  have hAllClosed : ∀ K : SaddleFunction m n,
      K ∈ omegaClassOfConvexBifunction F → IsClosedSaddleFunction K := by
    intro K hK
    have hEq : saddleEquivalent K (convexBifunctionClosedKernel F) := hK
    have hEqSymm : saddleEquivalent (convexBifunctionClosedKernel F) K :=
      ⟨hEq.2.1, hEq.1, hEq.2.2.1.symm, hEq.2.2.2.symm⟩
    exact section34_text_34_1_10 hQ.canonicalKernel_closed hEqSymm
  refine ⟨hQ.adjointPairing_eq, hCore.2.1, hCore.2.2, hAllClosed, ?_⟩
  intro K hK
  exact hQ.closedRepresentativeData K hK (hAllClosed K hK)

Generated-class form of Theorem 34.2: the canonical class coincides with the EquivalenceClassGeneratedByConvexBifunction {m n : ℕ} (F : { F // IsImageClosedConvexBifunction F }) : Set (SaddleFunction m n)EquivalenceClassGeneratedByConvexBifunction attached to the same closed convex bifunction.

theorem omegaClassOfConvexBifunction_eq_generatedClass
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F) :
    omegaClassOfConvexBifunction F =
      EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ := by
  exact (section34_theorem34_2 F hF).1

Original-wording form of Theorem 34.2: the canonical class is exactly the saddleEquivalent {m n : ℕ} (K L : SaddleFunction m n) : PropsaddleEquivalent-class of the canonical closed kernel generated by Unknown identifier `F`F.

theorem omegaClassOfConvexBifunction_eq_saddleEquivalenceClass
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F) :
    omegaClassOfConvexBifunction F =
      {K | saddleEquivalent K (convexBifunctionClosedKernel F)} := by
  exact (section34_theorem34_2 F hF).2.1

Original-wording membership form of Theorem 34.2: iff Unknown identifier `K`K is saddle-equivalent to the canonical closed kernel of Unknown identifier `F`F.

theorem mem_omegaClassOfConvexBifunction_iff_saddleEquivalent_closedKernel
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F)
    {K : SaddleFunction m n} :
    K ∈ omegaClassOfConvexBifunction F ↔
      saddleEquivalent K (convexBifunctionClosedKernel F) := by
  simp [omegaClassOfConvexBifunction_eq_saddleEquivalenceClass (F := F) hF]

Membership bridge for Theorem 34.2: iff Unknown identifier `K`K belongs to the generated equivalence class of Unknown identifier `F`F.

theorem mem_omegaClassOfConvexBifunction_iff_mem_generatedClass
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F)
    {K : SaddleFunction m n} :
    K ∈ omegaClassOfConvexBifunction F ↔
      K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ := by
  simp [omegaClassOfConvexBifunction_eq_generatedClass (F := F) hF]

Generated-class membership form of Theorem 34.2: generated-class membership is equivalent to saddle-equivalence with the canonical closed kernel.

theorem mem_generatedClass_iff_saddleEquivalent_closedKernel
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F)
    {K : SaddleFunction m n} :
    K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ ↔
      saddleEquivalent K (convexBifunctionClosedKernel F) := by
  constructor
  · intro hK
    exact (mem_omegaClassOfConvexBifunction_iff_saddleEquivalent_closedKernel (F := F) hF).1
      ((mem_omegaClassOfConvexBifunction_iff_mem_generatedClass (F := F) hF).2 hK)
  · intro hK
    exact (mem_omegaClassOfConvexBifunction_iff_mem_generatedClass (F := F) hF).1
      ((mem_omegaClassOfConvexBifunction_iff_saddleEquivalent_closedKernel (F := F) hF).2 hK)

Original-wording class identity for Theorem 34.2: the generated equivalence class of a closed convex bifunction is exactly the saddle-equivalence class of its canonical closed kernel.

theorem equivalenceClassGeneratedByConvexBifunction_eq_saddleEquivalenceClass
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F) :
    EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ =
      {K | saddleEquivalent K (convexBifunctionClosedKernel F)} := by
  ext K
  exact mem_generatedClass_iff_saddleEquivalent_closedKernel (F := F) hF

One-way original-wording membership bridge for Theorem 34.2: any saddle-function saddle-equivalent to the canonical closed kernel belongs to .

theorem mem_omegaClassOfConvexBifunction_of_saddleEquivalent_closedKernel
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F)
    {K : SaddleFunction m n}
    (hK : saddleEquivalent K (convexBifunctionClosedKernel F)) :
    K ∈ omegaClassOfConvexBifunction F := by
  exact (mem_omegaClassOfConvexBifunction_iff_saddleEquivalent_closedKernel (F := F) hF).2 hK

One-way original-wording membership bridge for Theorem 34.2: any saddle-function saddle-equivalent to the canonical closed kernel belongs to the generated equivalence class of Unknown identifier `F`F.

theorem mem_generatedClass_of_saddleEquivalent_closedKernel
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F)
    {K : SaddleFunction m n}
    (hK : saddleEquivalent K (convexBifunctionClosedKernel F)) :
    K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ := by
  exact (mem_generatedClass_iff_saddleEquivalent_closedKernel (F := F) hF).2 hK

One-way membership bridge for Theorem 34.2: generated-class membership implies membership in .

theorem mem_omegaClassOfConvexBifunction_of_mem_generatedClass
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F)
    {K : SaddleFunction m n}
    (hK : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) :
    K ∈ omegaClassOfConvexBifunction F := by
  exact (mem_omegaClassOfConvexBifunction_iff_mem_generatedClass (F := F) hF).2 hK

One-way membership bridge for Theorem 34.2: membership in implies generated-class membership.

theorem mem_generatedClass_of_mem_omegaClassOfConvexBifunction
    (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal)
    (hF : IsClosedConvexBifunction F)
    {K : SaddleFunction m n}
    (hK : K ∈ omegaClassOfConvexBifunction F) :
    K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ := by
  exact (mem_omegaClassOfConvexBifunction_iff_mem_generatedClass (F := F) hF).1 hK

end SaddleAmbientend Section34end Chap07