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

section Chap07section Section34open Setsection SaddleAmbientvariable {m n : ℕ}

Canonical-kernel membership form of Theorem 34.2: the canonical closed kernel belongs to .

theorem convexBifunctionClosedKernel_mem_omegaClassOfConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) : convexBifunctionClosedKernel F ∈ omegaClassOfConvexBifunction F := by exact (section34_theorem34_2 F hF).2.2

Canonical-kernel membership form of Theorem 34.2: the kernel generated by a closed convex bifunction belongs to its generated equivalence class.

theorem convexBifunctionClosedKernel_mem_generatedClass (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) : convexBifunctionClosedKernel F ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ := by exact mem_generatedClass_of_mem_omegaClassOfConvexBifunction (F := F) hF (convexBifunctionClosedKernel_mem_omegaClassOfConvexBifunction (F := F) hF)

Closedness form of Theorem 34.2 for the canonical representative: the canonical closed kernel of a closed convex bifunction is itself a closed saddle-function.

theorem isClosedSaddleFunction_convexBifunctionClosedKernel (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (unused variable `hF` Note: This linter can be disabled with `set_option linter.unusedVariables false`hF : IsClosedConvexBifunction F) (hQ : Section34Theorem34_2Qualification F) : IsClosedSaddleFunction (convexBifunctionClosedKernel F) := by exact hQ.canonicalKernel_closed

Class-level forward projection of Theorem 34.2: for every closed convex bifunction Unknown identifier `F`F, the canonical class is a closed concave-convex equivalence class.

theorem isClosedConcaveConvexEquivalenceClass_omegaClassOfConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) (hQ : Section34Theorem34_2Qualification F) : IsClosedConcaveConvexEquivalenceClass (omegaClassOfConvexBifunction F) := by have hKernelClosed : IsClosedSaddleFunction (convexBifunctionClosedKernel F) := isClosedSaddleFunction_convexBifunctionClosedKernel (F := F) hF hQ refine ⟨convexBifunctionClosedKernel F, hKernelClosed.1.1, hKernelClosed, ?_⟩ exact omegaClassOfConvexBifunction_eq_saddleEquivalenceClass (F := F) hF

Original-wording forward projection of Theorem 34.2: the saddle-equivalence class of the canonical closed kernel is a closed concave-convex equivalence class.

theorem isClosedConcaveConvexEquivalenceClass_saddleEquivalenceClass_closedKernel (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) (hQ : Section34Theorem34_2Qualification F) : IsClosedConcaveConvexEquivalenceClass {K | saddleEquivalent K (convexBifunctionClosedKernel F)} := by simpa [omegaClassOfConvexBifunction_eq_saddleEquivalenceClass (F := F) hF] using isClosedConcaveConvexEquivalenceClass_omegaClassOfConvexBifunction (F := F) hF hQ

Class-level forward projection of Theorem 34.2: the generated equivalence class of a closed convex bifunction is a closed concave-convex equivalence class.

theorem isClosedConcaveConvexEquivalenceClass_generatedClass (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) (hQ : Section34Theorem34_2Qualification F) : IsClosedConcaveConvexEquivalenceClass (EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) := by simpa [omegaClassOfConvexBifunction_eq_generatedClass (F := F) hF] using isClosedConcaveConvexEquivalenceClass_omegaClassOfConvexBifunction (F := F) hF hQ

A fixed seed closed convex bifunction, obtained from the constant-zero kernel, used to instantiate the converse half of Theorem 34.2 without introducing any extra assumptions.

lemma exists_closedConvexBifunction_seed : (∃ F₀ : (Fin m → ℝ) → (Fin n → ℝ) → EReal, IsClosedConvexBifunction F₀) → ∃ F₀ : (Fin m → ℝ) → (Fin n → ℝ) → EReal, IsClosedConvexBifunction F₀ := by intro hSeed exact hSeed

Converse projection of Theorem 34.2: every closed concave-convex equivalence class is for a unique closed convex bifunction Unknown identifier `F`F.

theorem existsUnique_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass (Omega : Set (SaddleFunction m n)) (hOmega : IsClosedConcaveConvexEquivalenceClass Omega) (hGlobal : Section34Theorem34_2GlobalQualification m n) : ∃! G : (Fin m → ℝ) → (Fin n → ℝ) → EReal, IsClosedConvexBifunction G ∧ Omega = omegaClassOfConvexBifunction G := by exact hGlobal.uniqueRealization Omega hOmega

Existence form of the converse half of Theorem 34.2: every closed concave-convex equivalence class is for some closed convex bifunction Unknown identifier `F`F.

theorem exists_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass (Omega : Set (SaddleFunction m n)) (hOmega : IsClosedConcaveConvexEquivalenceClass Omega) (hGlobal : Section34Theorem34_2GlobalQualification m n) : ∃ G : (Fin m → ℝ) → (Fin n → ℝ) → EReal, IsClosedConvexBifunction G ∧ Omega = omegaClassOfConvexBifunction G := by exact ExistsUnique.exists (existsUnique_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass (Omega := Omega) hOmega hGlobal)

Uniqueness form of the converse half of Theorem 34.2: two closed convex bifunctions generating the same closed concave-convex equivalence class must coincide.

theorem closedConvexBifunction_eq_of_closedConcaveConvexEquivalenceClass_eq (Omega : Set (SaddleFunction m n)) (hOmega : IsClosedConcaveConvexEquivalenceClass Omega) {G H : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hG : IsClosedConvexBifunction G) (hH : IsClosedConvexBifunction H) (hOmegaG : Omega = omegaClassOfConvexBifunction G) (hOmegaH : Omega = omegaClassOfConvexBifunction H) (hGlobal : Section34Theorem34_2GlobalQualification m n) : G = H := by rcases existsUnique_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass (Omega := Omega) hOmega hGlobal with ⟨F, hF, huniq⟩ calc G = F := huniq G ⟨hG, hOmegaG⟩ _ = H := (huniq H ⟨hH, hOmegaH⟩).symm

Original-wording converse form of Theorem 34.2: every closed concave-convex equivalence class is the saddle-equivalence class of the canonical closed kernel of a unique closed convex bifunction.

theorem existsUnique_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass_saddleEquivalenceClass (Omega : Set (SaddleFunction m n)) (hOmega : IsClosedConcaveConvexEquivalenceClass Omega) (hGlobal : Section34Theorem34_2GlobalQualification m n) : ∃! G : (Fin m → ℝ) → (Fin n → ℝ) → EReal, IsClosedConvexBifunction G ∧ Omega = {K | saddleEquivalent K (convexBifunctionClosedKernel G)} := by rcases existsUnique_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass (Omega := Omega) hOmega hGlobal with ⟨G, hG, huniq⟩ refine ⟨G, ?_, ?_⟩ · rcases hG with ⟨hGclosed, hOmegaG⟩ refine ⟨hGclosed, ?_⟩ calc Omega = omegaClassOfConvexBifunction G := hOmegaG _ = {K | saddleEquivalent K (convexBifunctionClosedKernel G)} := omegaClassOfConvexBifunction_eq_saddleEquivalenceClass (F := G) hGclosed · intro H hH rcases hH with ⟨hHclosed, hOmegaH⟩ apply huniq H refine ⟨hHclosed, ?_⟩ calc Omega = {K | saddleEquivalent K (convexBifunctionClosedKernel H)} := hOmegaH _ = omegaClassOfConvexBifunction H := (omegaClassOfConvexBifunction_eq_saddleEquivalenceClass (F := H) hHclosed).symm

Original-wording existence form of the converse half of Theorem 34.2.

theorem exists_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass_saddleEquivalenceClass (Omega : Set (SaddleFunction m n)) (hOmega : IsClosedConcaveConvexEquivalenceClass Omega) (hGlobal : Section34Theorem34_2GlobalQualification m n) : ∃ G : (Fin m → ℝ) → (Fin n → ℝ) → EReal, IsClosedConvexBifunction G ∧ Omega = {K | saddleEquivalent K (convexBifunctionClosedKernel G)} := by exact ExistsUnique.exists (existsUnique_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass_saddleEquivalenceClass (Omega := Omega) hOmega hGlobal)

Original-wording uniqueness form of the converse half of Theorem 34.2.

theorem closedConvexBifunction_eq_of_closedConcaveConvexEquivalenceClass_eq_saddleEquivalenceClass (Omega : Set (SaddleFunction m n)) (hOmega : IsClosedConcaveConvexEquivalenceClass Omega) {G H : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hG : IsClosedConvexBifunction G) (hH : IsClosedConvexBifunction H) (hOmegaG : Omega = {K | saddleEquivalent K (convexBifunctionClosedKernel G)}) (hOmegaH : Omega = {K | saddleEquivalent K (convexBifunctionClosedKernel H)}) (hGlobal : Section34Theorem34_2GlobalQualification m n) : G = H := by apply closedConvexBifunction_eq_of_closedConcaveConvexEquivalenceClass_eq (Omega := Omega) hOmega hG hH (hGlobal := hGlobal) · calc Omega = {K | saddleEquivalent K (convexBifunctionClosedKernel G)} := hOmegaG _ = omegaClassOfConvexBifunction G := (omegaClassOfConvexBifunction_eq_saddleEquivalenceClass (F := G) hG).symm · calc Omega = {K | saddleEquivalent K (convexBifunctionClosedKernel H)} := hOmegaH _ = omegaClassOfConvexBifunction H := (omegaClassOfConvexBifunction_eq_saddleEquivalenceClass (F := H) hH).symm

Characterization form of Theorem 34.2: a class of saddle-functions is a closed concave-convex equivalence class exactly when it is for some closed convex bifunction Unknown identifier `F`F.

theorem isClosedConcaveConvexEquivalenceClass_iff_exists_closedConvexBifunction (Omega : Set (SaddleFunction m n)) (hGlobal : Section34Theorem34_2GlobalQualification m n) : IsClosedConcaveConvexEquivalenceClass Omega ↔ ∃ G : (Fin m → ℝ) → (Fin n → ℝ) → EReal, IsClosedConvexBifunction G ∧ Omega = omegaClassOfConvexBifunction G := by constructor · intro hOmega exact exists_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass (Omega := Omega) hOmega hGlobal · rintro ⟨G, hG, rfl⟩ exact isClosedConcaveConvexEquivalenceClass_omegaClassOfConvexBifunction (F := G) hG (hGlobal.qualification G hG)

Original-wording characterization form of Theorem 34.2: a class of saddle-functions is a closed concave-convex equivalence class exactly when it is the saddle-equivalence class of the canonical closed kernel of some closed convex bifunction.

theorem isClosedConcaveConvexEquivalenceClass_iff_exists_closedConvexBifunction_saddleEquivalenceClass (Omega : Set (SaddleFunction m n)) (hGlobal : Section34Theorem34_2GlobalQualification m n) : IsClosedConcaveConvexEquivalenceClass Omega ↔ ∃ G : (Fin m → ℝ) → (Fin n → ℝ) → EReal, IsClosedConvexBifunction G ∧ Omega = {K | saddleEquivalent K (convexBifunctionClosedKernel G)} := by constructor · intro hOmega exact exists_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass_saddleEquivalenceClass (Omega := Omega) hOmega hGlobal · rintro ⟨G, hG, rfl⟩ exact isClosedConcaveConvexEquivalenceClass_saddleEquivalenceClass_closedKernel (F := G) hG (hGlobal.qualification G hG)

Unique-existence characterization form of Theorem 34.2.

theorem isClosedConcaveConvexEquivalenceClass_iff_existsUnique_closedConvexBifunction (Omega : Set (SaddleFunction m n)) (hGlobal : Section34Theorem34_2GlobalQualification m n) : IsClosedConcaveConvexEquivalenceClass Omega ↔ ∃! G : (Fin m → ℝ) → (Fin n → ℝ) → EReal, IsClosedConvexBifunction G ∧ Omega = omegaClassOfConvexBifunction G := by constructor · intro hOmega exact existsUnique_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass (Omega := Omega) hOmega hGlobal · rintro ⟨G, hG, _⟩ simpa [hG.2] using isClosedConcaveConvexEquivalenceClass_omegaClassOfConvexBifunction (F := G) hG.1 (hGlobal.qualification G hG.1)

Original-wording unique-existence characterization form of Theorem 34.2.

theorem isClosedConcaveConvexEquivalenceClass_iff_existsUnique_closedConvexBifunction_saddleEquivalenceClass (Omega : Set (SaddleFunction m n)) (hGlobal : Section34Theorem34_2GlobalQualification m n) : IsClosedConcaveConvexEquivalenceClass Omega ↔ ∃! G : (Fin m → ℝ) → (Fin n → ℝ) → EReal, IsClosedConvexBifunction G ∧ Omega = {K | saddleEquivalent K (convexBifunctionClosedKernel G)} := by constructor · intro hOmega exact existsUnique_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass_saddleEquivalenceClass (Omega := Omega) hOmega hGlobal · rintro ⟨G, hG, _⟩ simpa [hG.2] using isClosedConcaveConvexEquivalenceClass_saddleEquivalenceClass_closedKernel (F := G) hG.1 (hGlobal.qualification G hG.1)

Generated-class characterization form of Theorem 34.2.

theorem isClosedConcaveConvexEquivalenceClass_iff_exists_closedConvexBifunction_generatedClass (Omega : Set (SaddleFunction m n)) (hGlobal : Section34Theorem34_2GlobalQualification m n) : IsClosedConcaveConvexEquivalenceClass Omega ↔ ∃ G : (Fin m → ℝ) → (Fin n → ℝ) → EReal, ∃ hG : IsClosedConvexBifunction G, Omega = EquivalenceClassGeneratedByConvexBifunction ⟨G, hG⟩ := by constructor · intro hOmega rcases exists_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass (Omega := Omega) hOmega hGlobal with ⟨G, hG, hEq⟩ exact ⟨G, hG, by simpa [omegaClassOfConvexBifunction_eq_generatedClass (F := G) hG] using hEq⟩ · rintro ⟨G, hG, rfl⟩ exact isClosedConcaveConvexEquivalenceClass_generatedClass (F := G) hG (hGlobal.qualification G hG)

Generated-class unique-existence characterization form of Theorem 34.2.

theorem isClosedConcaveConvexEquivalenceClass_iff_existsUnique_closedConvexBifunction_generatedClass (Omega : Set (SaddleFunction m n)) (hGlobal : Section34Theorem34_2GlobalQualification m n) : IsClosedConcaveConvexEquivalenceClass Omega ↔ ∃! G : (Fin m → ℝ) → (Fin n → ℝ) → EReal, ∃ hG : IsClosedConvexBifunction G, Omega = EquivalenceClassGeneratedByConvexBifunction ⟨G, hG⟩ := by constructor · intro hOmega rcases existsUnique_closedConvexBifunction_of_closedConcaveConvexEquivalenceClass (Omega := Omega) hOmega hGlobal with ⟨G, hG, huniq⟩ refine ⟨G, ?_, ?_⟩ · exact ⟨hG.1, by simpa [omegaClassOfConvexBifunction_eq_generatedClass (F := G) hG.1] using hG.2⟩ · intro H hH rcases hH with ⟨hHclosed, hEqH⟩ apply huniq H refine ⟨hHclosed, ?_⟩ simpa [omegaClassOfConvexBifunction_eq_generatedClass (F := H) hHclosed] using hEqH · rintro ⟨G, hG, _⟩ rcases hG with ⟨hGclosed, hEq⟩ simpa [hEq] using isClosedConcaveConvexEquivalenceClass_generatedClass (F := G) hGclosed (hGlobal.qualification G hGclosed)

Kernel-equality projection of Theorem 34.2: for a closed convex bifunction Unknown identifier `F`F, the canonical closed kernel agrees with the adjoint kernel .

theorem convexBifunctionClosedKernel_eq_section34ConcaveBifunctionAdjointPairing (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (unused variable `hF` Note: This linter can be disabled with `set_option linter.unusedVariables false`hF : IsClosedConvexBifunction F) (hQ : Section34Theorem34_2Qualification F) : convexBifunctionClosedKernel F = section34ConcaveBifunctionAdjointPairing F := by exact hQ.adjointPairing_eq

Closedness projection of Theorem 34.2: every member of is closed.

theorem isClosedSaddleFunction_of_mem_omegaClassOfConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ omegaClassOfConvexBifunction F) (hQ : Section34Theorem34_2Qualification F) : IsClosedSaddleFunction K := by exact (section34_theorem34_2_qualified F hF hQ).2.2.2.1 K hK

Closedness projection of Theorem 34.2: every member of the generated equivalence class of a closed convex bifunction is closed.

theorem isClosedSaddleFunction_of_mem_generatedClass (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) (hQ : Section34Theorem34_2Qualification F) : IsClosedSaddleFunction K := by exact isClosedSaddleFunction_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_mem_generatedClass (F := F) hF hK) hQ

Domain projection of Theorem 34.2: every member of has effective domain .

theorem saddleEffectiveDomain_eq_domain_prod_of_mem_omegaClassOfConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (unused variable `hF` Note: This linter can be disabled with `set_option linter.unusedVariables false`hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ omegaClassOfConvexBifunction F) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : saddleEffectiveDomain K = convexBifunctionDomain F ×ˢ convexBifunctionKernelAdjointDomain F := by exact (hQ.closedRepresentativeData K hK hKclosed).2.2.1

Domain projection of Theorem 34.2: every member of the generated equivalence class of a closed convex bifunction has effective domain .

theorem saddleEffectiveDomain_eq_domain_prod_of_mem_generatedClass (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : saddleEffectiveDomain K = convexBifunctionDomain F ×ˢ convexBifunctionKernelAdjointDomain F := by exact saddleEffectiveDomain_eq_domain_prod_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_mem_generatedClass (F := F) hF hK) hKclosed hQ

First partial-closure projection of Theorem 34.2: every member of has first partial closure equal to the canonical kernel.

theorem partialClosure₁_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (unused variable `hF` Note: This linter can be disabled with `set_option linter.unusedVariables false`hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ omegaClassOfConvexBifunction F) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : partialClosure₁ K = convexBifunctionClosedKernel F := by exact (hQ.closedRepresentativeData K hK hKclosed).1

Second partial-closure projection of Theorem 34.2: every member of has second partial closure equal to the canonical kernel.

theorem partialClosure₂_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (unused variable `hF` Note: This linter can be disabled with `set_option linter.unusedVariables false`hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ omegaClassOfConvexBifunction F) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : partialClosure₂ K = convexBifunctionClosedKernel F := by exact (hQ.closedRepresentativeData K hK hKclosed).2.1

Primal recovery projection of Theorem 34.2: every member of recovers Unknown identifier `F`F by convex conjugation of its first slices.

theorem convexBifunction_eq_convexConjugate_slice_of_mem_omegaClassOfConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (unused variable `hF` Note: This linter can be disabled with `set_option linter.unusedVariables false`hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ omegaClassOfConvexBifunction F) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : ∀ u x, F u x = convexConjugate (K u) x := by exact (hQ.closedRepresentativeData K hK hKclosed).2.2.2.1

Adjoint recovery projection of Theorem 34.2: every member of recovers the concave adjoint by concave conjugation of its second slices.

theorem concaveAdjoint_eq_concaveConjugate_slice_of_mem_omegaClassOfConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (unused variable `hF` Note: This linter can be disabled with `set_option linter.unusedVariables false`hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ omegaClassOfConvexBifunction F) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : ∀ xStar uStar, section34ConcaveBifunctionAdjoint F xStar uStar = concaveConjugate (fun u => K u xStar) uStar := by exact (hQ.closedRepresentativeData K hK hKclosed).2.2.2.2.1

Relative-interior agreement projection of Theorem 34.2: every member of agrees with the canonical kernel on in the first variable or in the second variable.

theorem eq_convexBifunctionClosedKernel_on_relativeInterior_of_mem_omegaClassOfConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (unused variable `hF` Note: This linter can be disabled with `set_option linter.unusedVariables false`hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ omegaClassOfConvexBifunction F) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : ∀ u xStar, u ∈ intrinsicInterior ℝ (convexBifunctionDomain F) ∨ xStar ∈ intrinsicInterior ℝ (convexBifunctionKernelAdjointDomain F) → K u xStar = convexBifunctionClosedKernel F u xStar := by exact (hQ.closedRepresentativeData K hK hKclosed).2.2.2.2.2

Original-wording closedness projection of Theorem 34.2: every saddle-function saddle- equivalent to the canonical closed kernel is closed.

theorem isClosedSaddleFunction_of_saddleEquivalent_closedKernel (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : saddleEquivalent K (convexBifunctionClosedKernel F)) (hQ : Section34Theorem34_2Qualification F) : IsClosedSaddleFunction K := by exact isClosedSaddleFunction_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_saddleEquivalent_closedKernel (F := F) hF hK) hQ

Original-wording domain projection of Theorem 34.2: every saddle-function saddle-equivalent to the canonical closed kernel has effective domain .

theorem saddleEffectiveDomain_eq_domain_prod_of_saddleEquivalent_closedKernel (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : saddleEquivalent K (convexBifunctionClosedKernel F)) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : saddleEffectiveDomain K = convexBifunctionDomain F ×ˢ convexBifunctionKernelAdjointDomain F := by exact saddleEffectiveDomain_eq_domain_prod_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_saddleEquivalent_closedKernel (F := F) hF hK) hKclosed hQ

Original-wording first partial-closure projection of Theorem 34.2.

theorem partialClosure₁_eq_convexBifunctionClosedKernel_of_saddleEquivalent_closedKernel (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : saddleEquivalent K (convexBifunctionClosedKernel F)) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : partialClosure₁ K = convexBifunctionClosedKernel F := by exact partialClosure₁_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_saddleEquivalent_closedKernel (F := F) hF hK) hKclosed hQ

Original-wording second partial-closure projection of Theorem 34.2.

theorem partialClosure₂_eq_convexBifunctionClosedKernel_of_saddleEquivalent_closedKernel (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : saddleEquivalent K (convexBifunctionClosedKernel F)) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : partialClosure₂ K = convexBifunctionClosedKernel F := by exact partialClosure₂_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_saddleEquivalent_closedKernel (F := F) hF hK) hKclosed hQ

Original-wording primal recovery projection of Theorem 34.2.

theorem convexBifunction_eq_convexConjugate_slice_of_saddleEquivalent_closedKernel (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : saddleEquivalent K (convexBifunctionClosedKernel F)) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : ∀ u x, F u x = convexConjugate (K u) x := by exact convexBifunction_eq_convexConjugate_slice_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_saddleEquivalent_closedKernel (F := F) hF hK) hKclosed hQ

Original-wording adjoint recovery projection of Theorem 34.2.

theorem concaveAdjoint_eq_concaveConjugate_slice_of_saddleEquivalent_closedKernel (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : saddleEquivalent K (convexBifunctionClosedKernel F)) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : ∀ xStar uStar, section34ConcaveBifunctionAdjoint F xStar uStar = concaveConjugate (fun u => K u xStar) uStar := by exact concaveAdjoint_eq_concaveConjugate_slice_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_saddleEquivalent_closedKernel (F := F) hF hK) hKclosed hQ

Original-wording relative-interior agreement projection of Theorem 34.2.

theorem eq_convexBifunctionClosedKernel_on_relativeInterior_of_saddleEquivalent_closedKernel (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : saddleEquivalent K (convexBifunctionClosedKernel F)) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : ∀ u xStar, u ∈ intrinsicInterior ℝ (convexBifunctionDomain F) ∨ xStar ∈ intrinsicInterior ℝ (convexBifunctionKernelAdjointDomain F) → K u xStar = convexBifunctionClosedKernel F u xStar := by exact eq_convexBifunctionClosedKernel_on_relativeInterior_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_saddleEquivalent_closedKernel (F := F) hF hK) hKclosed hQ

Generated-class form of the first partial-closure projection in Theorem 34.2.

theorem partialClosure₁_eq_convexBifunctionClosedKernel_of_mem_generatedClass (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : partialClosure₁ K = convexBifunctionClosedKernel F := by exact partialClosure₁_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_mem_generatedClass (F := F) hF hK) hKclosed hQ

Generated-class form of the second partial-closure projection in Theorem 34.2.

theorem partialClosure₂_eq_convexBifunctionClosedKernel_of_mem_generatedClass (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : partialClosure₂ K = convexBifunctionClosedKernel F := by exact partialClosure₂_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_mem_generatedClass (F := F) hF hK) hKclosed hQ

Generated-class form of the primal recovery projection in Theorem 34.2.

theorem convexBifunction_eq_convexConjugate_slice_of_mem_generatedClass (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : ∀ u x, F u x = convexConjugate (K u) x := by exact convexBifunction_eq_convexConjugate_slice_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_mem_generatedClass (F := F) hF hK) hKclosed hQ

Generated-class form of the adjoint recovery projection in Theorem 34.2.

theorem concaveAdjoint_eq_concaveConjugate_slice_of_mem_generatedClass (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : ∀ xStar uStar, section34ConcaveBifunctionAdjoint F xStar uStar = concaveConjugate (fun u => K u xStar) uStar := by exact concaveAdjoint_eq_concaveConjugate_slice_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_mem_generatedClass (F := F) hF hK) hKclosed hQ

Generated-class form of the relative-interior agreement projection in Theorem 34.2.

theorem eq_convexBifunctionClosedKernel_on_relativeInterior_of_mem_generatedClass (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) (hKclosed : IsClosedSaddleFunction K) (hQ : Section34Theorem34_2Qualification F) : ∀ u xStar, u ∈ intrinsicInterior ℝ (convexBifunctionDomain F) ∨ xStar ∈ intrinsicInterior ℝ (convexBifunctionKernelAdjointDomain F) → K u xStar = convexBifunctionClosedKernel F u xStar := by exact eq_convexBifunctionClosedKernel_on_relativeInterior_of_mem_omegaClassOfConvexBifunction (F := F) hF (mem_omegaClassOfConvexBifunction_of_mem_generatedClass (F := F) hF hK) hKclosed hQ
-- Proof sketch: combine the closed-equivalence-class description from Theorem 34.2 with the -- one-variable convex and concave closure characterizations of the coordinate slices, then read -- off how the slice domains behave on the relative interiors, boundary layers, and complements of -- `dom₁ K` and `dom₂ K`.

Defn 34.8: a concave-convex function Unknown identifier `K`K on ℝ ^ sorry × ℝ ^ sorry : Typeℝ^Unknown identifier `m`m × ℝ^Unknown identifier `n`n is simple when every convex section with Unknown identifier `u`sorry ∈ sorry : Propu ∈ Unknown identifier `ri`ri (dom₁ K) has effective domain contained in closure sorry : Set ?m.1closure (Unknown identifier `dom₂`dom₂ K), and every concave section with Unknown identifier `v`sorry ∈ sorry : Propv ∈ Unknown identifier `ri`ri (dom₂ K) has effective domain contained in closure sorry : Set ?m.1closure (Unknown identifier `dom₁`dom₁ K).

def IsSimpleConcaveConvex (K : SaddleFunction m n) : Prop := IsConcaveConvex K ∧ (∀ u, u ∈ intrinsicInterior ℝ (effectiveDomain₁ K) → convexFunctionEffectiveDomain (K u) ⊆ closure (effectiveDomain₂ K)) ∧ ∀ v, v ∈ intrinsicInterior ℝ (effectiveDomain₂ K) → concaveFunctionEffectiveDomain (fun u => K u v) ⊆ closure (effectiveDomain₁ K)

A saddle-function is simple when it satisfies the section-domain containment condition in whichever of the two saddle orientations it carries.

def IsSimpleSaddleFunction (K : SaddleFunction m n) : Prop := IsSimpleConcaveConvex K ∨ (IsConvexConcave K ∧ (∀ u, u ∈ intrinsicInterior ℝ (effectiveDomain₁ K) → concaveFunctionEffectiveDomain (K u) ⊆ closure (effectiveDomain₂ K)) ∧ ∀ v, v ∈ intrinsicInterior ℝ (effectiveDomain₂ K) → convexFunctionEffectiveDomain (fun u => K u v) ⊆ closure (effectiveDomain₁ K))

Forward closed-slice half of Theorem 34.3: for a proper concave-convex saddle-function on ℝ ^ sorry × ℝ ^ sorry : Typeℝ^Unknown identifier `m`m × ℝ^Unknown identifier `n`n, closedness forces the coordinate slice conditions listed in the text.

theorem closed_concaveConvex_iff_relativeInterior_slice_conditions (K : SaddleFunction m n) (hKproper : IsProperSaddleFunction K) (hKcc : IsConcaveConvex K) (hGlobal : Section34Theorem34_2GlobalQualification m n) : IsClosedSaddleFunction K → let C := effectiveDomain₁ K let D := effectiveDomain₂ K (∀ u, u ∈ intrinsicInterior ℝ C → IsProperClosedConvexFunctionWithDomain (K u) D) ∧ (∀ u, u ∈ C \ intrinsicInterior ℝ C → IsProperConvexFunctionWithDomainBetween (K u) D (closure D)) ∧ (∀ u, u ∉ C → IsImproperConvexFunction (K u) ∧ (∀ v, v ∈ intrinsicInterior ℝ D → K u v = (⊥ : EReal)) ∧ (u ∉ closure C → ∀ v, v ∈ D → K u v = (⊥ : EReal))) ∧ (∀ v, v ∈ intrinsicInterior ℝ D → IsProperClosedConcaveFunctionWithDomain (fun u => K u v) C) ∧ (∀ v, v ∈ D \ intrinsicInterior ℝ D → IsProperConcaveFunctionWithDomainBetween (fun u => K u v) C (closure C)) ∧ ∀ v, v ∉ D → IsImproperConcaveFunction (fun u => K u v) ∧ (∀ u, u ∈ intrinsicInterior ℝ C → K u v = (⊤ : EReal)) ∧ (v ∉ closure D → ∀ u, u ∈ C → K u v = (⊤ : EReal)) := by intro hKclosed let Omega : Set (SaddleFunction m n) := {L | saddleEquivalent L K} have hOmega : IsClosedConcaveConvexEquivalenceClass Omega := by refine ⟨K, hKcc, hKclosed, ?_⟩ rfl rcases (isClosedConcaveConvexEquivalenceClass_iff_exists_closedConvexBifunction_generatedClass (Omega := Omega) hGlobal).1 hOmega with ⟨F, hF, hOmegaEq⟩ have hQ : Section34Theorem34_2Qualification F := hGlobal.qualification F hF have hKrefl : saddleEquivalent K K := ⟨hKcc, hKcc, rfl, rfl⟩ have hKmemOmega : K ∈ Omega := by simpa [Omega] using hKrefl have hKmem : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ := by simpa [hOmegaEq] using hKmemOmega have hKernelEq : convexBifunctionClosedKernel F = section34ConcaveBifunctionAdjointPairing F := convexBifunctionClosedKernel_eq_section34ConcaveBifunctionAdjointPairing (F := F) hF hQ have hKernelPc1 : partialClosure₁ (convexBifunctionClosedKernel F) = convexBifunctionClosedKernel F := by exact partialClosure₁_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F := F) hF (convexBifunctionClosedKernel_mem_omegaClassOfConvexBifunction (F := F) hF) hQ.canonicalKernel_closed hQ have hKernelPc2 : partialClosure₂ (convexBifunctionClosedKernel F) = convexBifunctionClosedKernel F := by exact partialClosure₂_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F := F) hF (convexBifunctionClosedKernel_mem_omegaClassOfConvexBifunction (F := F) hF) hQ.canonicalKernel_closed hQ have hEq : saddleEquivalent K (convexBifunctionClosedKernel F) := (mem_generatedClass_iff_saddleEquivalent_closedKernel (F := F) hF).1 hKmem have hKsand : IsConcaveConvex K ∧ (∀ u xStar, convexBifunctionClosedKernel F u xStar ≤ K u xStar) ∧ (∀ u xStar, K u xStar ≤ section34ConcaveBifunctionAdjointPairing F u xStar) := by refine ⟨hEq.1, ?_, ?_⟩ · intro u xStar have hLe : partialClosure₂ K u xStar ≤ K u xStar := helperForText_34_0_1_partialClosure₂_le K u xStar simpa [hEq.2.2.2, hKernelPc2] using hLe · intro u xStar have hLe : K u xStar ≤ partialClosure₁ K u xStar := helperForText_34_0_1_le_partialClosure₁ K u xStar have hLeKernel : K u xStar ≤ convexBifunctionClosedKernel F u xStar := by simpa [hEq.2.2.1, hKernelPc1] using hLe exact hKernelEq ▸ hLeKernel have hKeq : K = convexBifunctionClosedKernel F := by funext u xStar apply le_antisymm · exact (hKsand.2.2 u xStar).trans (hKernelEq ▸ le_rfl) · exact hKsand.2.1 u xStar have hCeq : effectiveDomain₁ K = convexBifunctionDomain F := by try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [convexBifunctionDomain, hKeq] have hDeq : effectiveDomain₂ K = convexBifunctionKernelAdjointDomain F := by try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [convexBifunctionKernelAdjointDomain, hKeq] have hDomainNonempty : (saddleEffectiveDomain K).Nonempty := Set.nonempty_iff_ne_empty.mpr hKproper rcases hDomainNonempty with ⟨⟨u0, xStar0⟩, hu0xStar0⟩ have hCnonempty : (effectiveDomain₁ K).Nonempty := ⟨u0, (Set.mem_prod.mp hu0xStar0).1⟩ have hDnonempty : (effectiveDomain₂ K).Nonempty := ⟨xStar0, (Set.mem_prod.mp hu0xStar0).2⟩ have hParamSubsetKernelDomain : convexBifunctionParameterDomain F ⊆ convexBifunctionDomain F := by intro u huParam xStar rcases huParam with ⟨x, hx⟩ have hPairNeBot : convexBifunctionPairing F u xStar ≠ (⊥ : EReal) := by simpa [convexBifunctionPairing, bifunctionPairingNotation, convexConjugate] using helperForTheorem33_1_convexConjugate_ne_bot_of_point (f := F u) (x₀ := x) hx xStar exact bot_lt_iff_ne_bot.mpr hPairNeBot have hKernelConvex : ∀ u, IsERealConvexOn (Set.univ : Set (Fin n → ℝ)) (convexBifunctionClosedKernel F u) := by intro u simpa [hKeq] using hKcc.2 u (by simp) have hKernelConcave : ∀ xStar, IsERealConcaveOn (Set.univ : Set (Fin m → ℝ)) (fun u => convexBifunctionClosedKernel F u xStar) := by intro xStar simpa [hKeq] using hKcc.1 xStar (by simp) have hKernelSliceClosed2 : ∀ u, IsFunctionConvexClosed (convexBifunctionClosedKernel F u) := by intro u unfold IsFunctionConvexClosed funext xStar have hPoint : partialClosure₂ (convexBifunctionClosedKernel F) u xStar = convexBifunctionClosedKernel F u xStar := by exact congrArg (fun G => G u xStar) hKernelPc2 simpa [partialClosure₂, convexClosureInSecond, functionConvexClosure] using hPoint.symm have hKernelSliceClosed1 : ∀ xStar, IsFunctionConcaveClosed (fun u => convexBifunctionClosedKernel F u xStar) := by intro xStar unfold IsFunctionConcaveClosed funext u have hPoint : partialClosure₁ (convexBifunctionClosedKernel F) u xStar = convexBifunctionClosedKernel F u xStar := by exact congrArg (fun G => G u xStar) hKernelPc1 simpa [partialClosure₁, concaveClosureInFirst, functionConcaveClosure] using hPoint.symm have hOffFirstBot : ∀ {u : Fin m → ℝ}, u ∉ convexBifunctionDomain F → ∀ xStar : Fin n → ℝ, convexBifunctionClosedKernel F u xStar = (⊥ : EReal) := by intro u hu xStar have huParam : u ∉ convexBifunctionParameterDomain F := by intro huParam exact hu (hParamSubsetKernelDomain huParam) simpa [convexBifunctionClosedKernel] using helperForCorollary33_2_2_convex_pairing_eq_bot_of_off_parameterDomain (G := F) (u := u) huParam xStar have hSecondDomainEq : convexBifunctionKernelAdjointDomain F = concaveBifunctionEffectiveDomain (section34ConcaveBifunctionAdjoint F) := by ext xStar constructor · intro hx have hx0 : xStar ∈ effectiveDomain (Set.univ : Set (Fin n → ℝ)) (fun x' => concaveBifunctionPairing (section34ConcaveBifunctionAdjoint F) x' (0 : Fin m → ℝ)) := by rw [effectiveDomain_eq] constructor · simp have hPoint : section34ConcaveBifunctionAdjointPairing F (0 : Fin m → ℝ) xStar < (⊤ : EReal) := by rw [← hKernelEq] exact hx (0 : Fin m → ℝ) simpa [section34ConcaveBifunctionAdjointPairing, concaveBifunctionPairing] using hPoint rw [_root_.helperForCorollary33_2_1_concavePairingSection_effectiveDomain_eq (m := n) (n := m) (F := section34ConcaveBifunctionAdjoint F) (0 : Fin m → ℝ)] at hx0 simpa [concaveBifunctionEffectiveDomain, bot_lt_iff_ne_bot] using hx0 · intro hx uStar have hxu : xStar ∈ effectiveDomain (Set.univ : Set (Fin n → ℝ)) (fun x' => concaveBifunctionPairing (section34ConcaveBifunctionAdjoint F) x' uStar) := by rw [_root_.helperForCorollary33_2_1_concavePairingSection_effectiveDomain_eq (m := n) (n := m) (F := section34ConcaveBifunctionAdjoint F) uStar] simpa [concaveBifunctionEffectiveDomain, bot_lt_iff_ne_bot] using hx have hPairFinite : concaveBifunctionPairing (section34ConcaveBifunctionAdjoint F) xStar uStar < (⊤ : EReal) := by simpa [effectiveDomain_eq] using hxu have hPoint : section34ConcaveBifunctionAdjointPairing F uStar xStar < (⊤ : EReal) := by simpa [section34ConcaveBifunctionAdjointPairing, concaveBifunctionPairing] using hPairFinite rw [hKernelEq] exact hPoint have hOffSecondTop : ∀ {xStar : Fin n → ℝ}, xStar ∉ convexBifunctionKernelAdjointDomain F → ∀ u : Fin m → ℝ, convexBifunctionClosedKernel F u xStar = (⊤ : EReal) := by intro xStar hxStar u have hxAdj : xStar ∉ concaveBifunctionEffectiveDomain (section34ConcaveBifunctionAdjoint F) := by simpa [hSecondDomainEq] using hxStar have hAllBot : ∀ uStar : Fin m → ℝ, section34ConcaveBifunctionAdjoint F xStar uStar = (⊥ : EReal) := by intro uStar by_contra hNeBot exact hxAdj ⟨uStar, bot_lt_iff_ne_bot.mpr hNeBot⟩ have hPairTop : section34ConcaveBifunctionAdjointPairing F u xStar = (⊤ : EReal) := by rw [section34ConcaveBifunctionAdjointPairing, concaveBifunctionPairing, bifunctionPairingNotation, conjugatePairingNotation] simp [hAllBot] rw [hKernelEq] exact hPairTop dsimp refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ · intro u hu rw [hCeq] at hu have huF : u ∈ intrinsicInterior ℝ (convexBifunctionDomain F) := hu have huDom : u ∈ convexBifunctionDomain F := intrinsicInterior_subset huF refine ⟨?_, ?_, ?_, ?_⟩ · simpa [hKeq] using hKernelConvex u · simpa [hKeq] using hKernelSliceClosed2 u · intro xStar exact bot_lt_iff_ne_bot.mp (by simpa [hKeq] using huDom xStar) · ext xStar constructor · intro hx by_contra hxOut have hxOutF : xStar ∉ convexBifunctionKernelAdjointDomain F := by simpa [hDeq] using hxOut have hTop : convexBifunctionClosedKernel F u xStar = (⊤ : EReal) := hOffSecondTop hxOutF u exact (lt_top_iff_ne_top.mp (by simpa [convexFunctionEffectiveDomain, hKeq] using hx)) (by simpa [hKeq] using hTop) · intro hx have hxF : xStar ∈ convexBifunctionKernelAdjointDomain F := by simpa [hDeq] using hx simpa [convexFunctionEffectiveDomain, hKeq] using hxF u · intro u hu have huDomK : u ∈ effectiveDomain₁ K := hu.1 have huDom : u ∈ convexBifunctionDomain F := by simpa [hCeq] using huDomK refine ⟨?_, ?_, ?_, ?_, ?_⟩ · simpa [hKeq] using hKernelConvex u · intro xStar exact bot_lt_iff_ne_bot.mp (by simpa [hKeq] using huDom xStar) · rcases hDnonempty with ⟨xStar, hxStar⟩ exact ⟨xStar, by simpa [convexFunctionEffectiveDomain] using hxStar u⟩ · intro xStar hxStar simpa [convexFunctionEffectiveDomain] using hxStar u · intro xStar hx by_contra hxOut have hxOutK : xStar ∉ effectiveDomain₂ K := by intro hxMem exact hxOut (subset_closure hxMem) have hxOutF : xStar ∉ convexBifunctionKernelAdjointDomain F := by simpa [hDeq] using hxOutK have hTop : convexBifunctionClosedKernel F u xStar = (⊤ : EReal) := hOffSecondTop hxOutF u exact (lt_top_iff_ne_top.mp (by simpa [convexFunctionEffectiveDomain, hKeq] using hx)) (by simpa [hKeq] using hTop) · intro u hu have huF : u ∉ convexBifunctionDomain F := by simpa [hCeq] using hu refine ⟨?_, ?_, ?_⟩ · refine ⟨?_, ?_⟩ · simpa [hKeq] using hKernelConvex u · intro hProperSlice rcases hDnonempty with ⟨xStar, _⟩ have hBot : K u xStar = (⊥ : EReal) := by simpa [hKeq] using hOffFirstBot huF xStar exact (hProperSlice.1 xStar) hBot · intro xStar _hxStar simpa [hKeq] using hOffFirstBot huF xStar · intro _huCl xStar _hxStar simpa [hKeq] using hOffFirstBot huF xStar · intro xStar hxStar rw [hDeq] at hxStar have hxStarF : xStar ∈ intrinsicInterior ℝ (convexBifunctionKernelAdjointDomain F) := hxStar have hxStarDom : xStar ∈ convexBifunctionKernelAdjointDomain F := intrinsicInterior_subset hxStarF refine ⟨?_, ?_, ?_, ?_⟩ · simpa [hKeq] using hKernelConcave xStar · simpa [hKeq] using hKernelSliceClosed1 xStar · intro u exact lt_top_iff_ne_top.mp (by simpa [hKeq] using hxStarDom u) · ext u constructor · intro hu by_contra huOut have huOutF : u ∉ convexBifunctionDomain F := by simpa [hCeq] using huOut have hBot : convexBifunctionClosedKernel F u xStar = (⊥ : EReal) := hOffFirstBot huOutF xStar exact (bot_lt_iff_ne_bot.mp (by simpa [concaveFunctionEffectiveDomain, hKeq] using hu)) (by simpa [hKeq] using hBot) · intro hu have huF : u ∈ convexBifunctionDomain F := by simpa [hCeq] using hu simpa [concaveFunctionEffectiveDomain, hKeq] using huF xStar · intro xStar hxStar have hxStarDomK : xStar ∈ effectiveDomain₂ K := hxStar.1 have hxStarDom : xStar ∈ convexBifunctionKernelAdjointDomain F := by simpa [hDeq] using hxStarDomK refine ⟨?_, ?_, ?_, ?_, ?_⟩ · simpa [hKeq] using hKernelConcave xStar · intro u exact lt_top_iff_ne_top.mp (by simpa [hKeq] using hxStarDom u) · rcases hCnonempty with ⟨u, hu⟩ exact ⟨u, by simpa [concaveFunctionEffectiveDomain] using hu xStar⟩ · intro u hu simpa [concaveFunctionEffectiveDomain] using hu xStar · intro u hu by_contra huOut have huOutK : u ∉ effectiveDomain₁ K := by intro huMem exact huOut (subset_closure huMem) have huOutF : u ∉ convexBifunctionDomain F := by simpa [hCeq] using huOutK have hBot : convexBifunctionClosedKernel F u xStar = (⊥ : EReal) := hOffFirstBot huOutF xStar exact (bot_lt_iff_ne_bot.mp (by simpa [concaveFunctionEffectiveDomain, hKeq] using hu)) (by simpa [hKeq] using hBot) · intro xStar hxStar have hxStarF : xStar ∉ convexBifunctionKernelAdjointDomain F := by simpa [hDeq] using hxStar refine ⟨?_, ?_, ?_⟩ · refine ⟨?_, ?_⟩ · simpa [hKeq] using hKernelConcave xStar · intro hProperSlice rcases hCnonempty with ⟨u, _⟩ have hTop : K u xStar = (⊤ : EReal) := by simpa [hKeq] using hOffSecondTop hxStarF u exact (hProperSlice.1 u) hTop · intro u _hu simpa [hKeq] using hOffSecondTop hxStarF u · intro _hxCl u _hu simpa [hKeq] using hOffSecondTop hxStarF u
-- Proof sketch: apply Theorem 34.3 to the closed proper concave-convex saddle-function `K`, -- then read off the section-domain containment conditions from the closed-slice -- characterization of the relative interiors of `dom₁ K` and `dom₂ K`.

Text 34.4.1: every closed proper concave-convex saddle-function Unknown identifier `K`K on ℝ ^ sorry × ℝ ^ sorry : Typeℝ^Unknown identifier `m`m × ℝ^Unknown identifier `n`n is simple.

theorem closed_proper_saddleFunction_isSimple (K : SaddleFunction m n) (hKclosed : IsClosedSaddleFunction K) (hKproper : IsProperSaddleFunction K) (hGlobal : Section34Theorem34_2GlobalQualification m n) : IsSimpleConcaveConvex K := by have hKcc : IsConcaveConvex K := hKclosed.1.1 have hSlices := closed_concaveConvex_iff_relativeInterior_slice_conditions (K := K) hKproper hKcc hGlobal hKclosed dsimp at hSlices rcases hSlices with ⟨hConvClosed, _hBoundaryConv, _hOutsideConv, hConcClosed, _hBoundaryConc, _hOutsideConc⟩ refine ⟨hKcc, ?_, ?_⟩ · intro u hu rcases hConvClosed u hu with ⟨_hConv, _hClosed, _hNoBot, hDomEq⟩ rw [hDomEq] exact subset_closure · intro v hv rcases hConcClosed v hv with ⟨_hConc, _hClosed, _hNoTop, hDomEq⟩ rw [hDomEq] exact subset_closure
-- Proof sketch: in the convex branch, the canonical kernel `⟨F u, x*⟩` is concave-convex by the -- Rockafellar bifunction correspondence, and its sectionwise conjugate construction forces the -- effective domains of the slices to sit inside the closures required by Defn 34.8; argue -- dually for a concave bifunction using the convex-concave branch of `IsSimpleSaddleFunction`.

Helper for Text 34.4.2: the constant ⊤ : ?m.1⊤ function is convex in the Jensen sense on ℝ ^ sorry : Typeℝ^Unknown identifier `n`n.

lemma helperForText_34_4_2_constTop_isERealConvexOn {n : ℕ} : IsERealConvexOn (Set.univ : Set (Fin n → ℝ)) (fun _ : Fin n → ℝ => (⊤ : EReal)) := by intro x y hx hy a b ha hb hab hxy by_cases hZeroA : a = 0 · have hBOne : b = 1 := by linarith simp [hZeroA, hBOne] by_cases hZeroB : b = 0 · have hAOne : a = 1 := by linarith simp [hZeroB, hAOne] have hPosA : 0 < a := lt_of_le_of_ne ha (by simpa [eq_comm] using hZeroA) have hPosB : 0 < b := lt_of_le_of_ne hb (by simpa [eq_comm] using hZeroB) simp [EReal.coe_mul_top_of_pos hPosA, EReal.coe_mul_top_of_pos hPosB]

Helper for Text 34.4.2: the constant ⊥ : ?m.1⊥ saddle-function is simple.

lemma helperForText_34_4_2_constBot_isSimpleSaddleFunction : IsSimpleSaddleFunction (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := by left refine ⟨?_, ?_, ?_⟩ · constructor · intro v _ simpa using (helperForText_34_1_4_constBot_isERealConcaveOn (n := m)) · intro u _ simpa using (helperForTheorem33_1_constBot_isERealConvexOn (n := n)) · intro u hu simp [effectiveDomain₁] at hu · intro v hv u hu simp [concaveFunctionEffectiveDomain] at hu

Helper for Text 34.4.2: the constant ⊤ : ?m.1⊤ saddle-function is simple.

lemma helperForText_34_4_2_constTop_isSimpleSaddleFunction : IsSimpleSaddleFunction (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) := by left refine ⟨?_, ?_, ?_⟩ · constructor · intro v _ simpa using (helperForCorollary33_1_2_constTop_isERealConcaveOn (k := m)) · intro u _ simpa using (helperForText_34_4_2_constTop_isERealConvexOn (n := n)) · intro u hu v hv simp [convexFunctionEffectiveDomain] at hv · intro v hv simp [effectiveDomain₂] at hv
-- Proof sketch: combine the domain convexity from Text 34.1.6 with the existence of a genuine -- interior point of `dom K`. For a concave-convex saddle-function, the relative interior points -- of `dom₁ K` and `dom₂ K` are ordinary interior points, so a short-segment / extrapolation -- argument forces the slice effective domains to lie in the coordinate closures required by -- Defn 34.8.

Helper for Text 34.4.3: for a convex subset of a finite-dimensional Euclidean space, if the ordinary interior is nonempty, then intrinsic interior points are ordinary interior points.

lemma helperForText_34_4_3_mem_interior_of_mem_intrinsicInterior_of_convex_nonemptyInterior {k : ℕ} {C : Set (Fin k → ℝ)} (hCconv : Convex ℝ C) (hCint : (interior C).Nonempty) {u : Fin k → ℝ} (hu : u ∈ intrinsicInterior ℝ C) : u ∈ interior C := by have hAff : affineSpan ℝ C = ⊤ := (hCconv.interior_nonempty_iff_affineSpan_eq_top).1 hCint rcases hu with ⟨y, hy, hyu⟩ letI : Nonempty (affineSpan ℝ C) := ⟨y⟩ let e : affineSpan ℝ C ≃ᵃⁱ[ℝ] (Fin k → ℝ) := AffineIsometryEquiv.ofTop (𝕜 := ℝ) (V := Fin k → ℝ) (P := Fin k → ℝ) (s₁ := affineSpan ℝ C) hAff have hyOpen : IsOpen (e '' interior ((↑) ⁻¹' C : Set <| affineSpan ℝ C)) := by exact e.toHomeomorph.isOpenMap _ isOpen_interior have hyMem : e y ∈ e '' interior ((↑) ⁻¹' C : Set <| affineSpan ℝ C) := by exact ⟨y, hy, rfl⟩ have hsub : e '' interior ((↑) ⁻¹' C : Set <| affineSpan ℝ C) ⊆ C := by intro x hx rcases hx with ⟨z, hz, rfl⟩ simpa [e, AffineIsometryEquiv.ofTop_apply (s₁ := affineSpan ℝ C) (P := Fin k → ℝ) (V := Fin k → ℝ) (𝕜 := ℝ) hAff z] using (interior_subset hz) have hNhds : e y ∈ interior C := by apply mem_interior_iff_mem_nhds.2 exact Filter.mem_of_superset (IsOpen.mem_nhds hyOpen hyMem) hsub simpa [e, hyu, AffineIsometryEquiv.ofTop_apply (s₁ := affineSpan ℝ C) (P := Fin k → ℝ) (V := Fin k → ℝ) (𝕜 := ℝ) hAff y] using hNhds

Helper for Text 34.4.3: from an interior point one can extrapolate past any target point and stay inside the set.

lemma helperForText_34_4_3_exists_extrapolatedPoint {k : ℕ} {C : Set (Fin k → ℝ)} {u u' : Fin k → ℝ} (hu : u ∈ interior C) : ∃ s : ℝ, 0 < s ∧ let w := u + s • (u - u') w ∈ C ∧ u = (1 / (1 + s)) • w + (s / (1 + s)) • u' := by rcases Metric.mem_nhds_iff.mp (mem_interior_iff_mem_nhds.mp hu) with ⟨ε, hεpos, hεsub⟩ let s : ℝ := ε / (‖u - u'‖ + 1) refine ⟨s, ?_, ?_⟩ · have hden : 0 < ‖u - u'‖ + 1 := by positivity exact div_pos hεpos hden · dsimp [s] refine ⟨?_, ?_⟩ · apply hεsub rw [Metric.mem_ball, dist_eq_norm] rw [show u + (ε / (‖u - u'‖ + 1)) • (u - u') - u = (ε / (‖u - u'‖ + 1)) • (u - u') by abel] rw [norm_smul, Real.norm_of_nonneg (by positivity)] have hden : 0 < ‖u - u'‖ + 1 := by positivity have hnumlt : ‖u - u'‖ < 1 * (‖u - u'‖ + 1) := by linarith [norm_nonneg (u - u')] have hlt : ‖u - u'‖ / (‖u - u'‖ + 1) < 1 := by exact (div_lt_iff₀ hden).2 hnumlt have hmul : ε / (‖u - u'‖ + 1) * ‖u - u'‖ = ε * (‖u - u'‖ / (‖u - u'‖ + 1)) := by ring_nf rw [hmul] nlinarith [hεpos, hlt] · ext i simp [Pi.smul_apply, sub_eq_add_neg] have hspos : 0 < ε / (‖u - u'‖ + 1) := by have hden : 0 < ‖u - u'‖ + 1 := by positivity exact div_pos hεpos hden have hs1 : 1 + ε / (‖u - u'‖ + 1) ≠ 0 := by linarith field_simp [hs1] ring

Helper for Text 34.4.3: from a point outside a closed set one can move a short distance along a segment towards an interior point and remain outside the closed set.

lemma helperForText_34_4_3_exists_openSegmentPoint {k : ℕ} {C : Set (Fin k → ℝ)} {v v0 : Fin k → ℝ} (hv : v ∈ interior C) : ∃ t : ℝ, 0 < t ∧ t < 1 ∧ ((1 - t) • v + t • v0) ∈ C := by rcases Metric.mem_nhds_iff.mp (mem_interior_iff_mem_nhds.mp hv) with ⟨ε, hεpos, hεsub⟩ let t : ℝ := min (1 / 2) (ε / (‖v0 - v‖ + 1)) refine ⟨t, ?_, ?_, ?_⟩ · have hright : 0 < ε / (‖v0 - v‖ + 1) := by have hden : 0 < ‖v0 - v‖ + 1 := by positivity exact div_pos hεpos hden exact lt_min (by norm_num) hright · exact lt_of_le_of_lt (min_le_left _ _) (by norm_num) · apply hεsub rw [Metric.mem_ball, dist_eq_norm] dsimp [t] have hEq : (1 - min (1 / 2) (ε / (‖v0 - v‖ + 1))) • v + min (1 / 2) (ε / (‖v0 - v‖ + 1)) • v0 - v = min (1 / 2) (ε / (‖v0 - v‖ + 1)) • (v0 - v) := by ext i simp [sub_eq_add_neg, mul_add, add_comm] ring rw [hEq, norm_smul, Real.norm_of_nonneg (le_of_lt (show 0 < t by have hright : 0 < ε / (‖v0 - v‖ + 1) := by have hden : 0 < ‖v0 - v‖ + 1 := by positivity exact div_pos hεpos hden exact lt_min (by norm_num) hright))] have htle : t ≤ ε / (‖v0 - v‖ + 1) := by dsimp [t] exact min_le_right _ _ have hmul_le : t * ‖v0 - v‖ ≤ (ε / (‖v0 - v‖ + 1)) * ‖v0 - v‖ := by exact mul_le_mul_of_nonneg_right htle (norm_nonneg _) have hlt : (ε / (‖v0 - v‖ + 1)) * ‖v0 - v‖ < ε := by have hden : 0 < ‖v0 - v‖ + 1 := by positivity have hnumlt : ‖v0 - v‖ < 1 * (‖v0 - v‖ + 1) := by linarith [norm_nonneg (v0 - v)] have hfrac : ‖v0 - v‖ / (‖v0 - v‖ + 1) < 1 := by exact (div_lt_iff₀ hden).2 hnumlt have hmul : (ε / (‖v0 - v‖ + 1)) * ‖v0 - v‖ = ε * (‖v0 - v‖ / (‖v0 - v‖ + 1)) := by ring_nf rw [hmul] nlinarith [hεpos, hfrac] exact lt_of_le_of_lt hmul_le hlt

Text 34.4.3: let Unknown identifier `K`K be a concave-convex saddle-function on ℝ ^ sorry × ℝ ^ sorry : Typeℝ^Unknown identifier `m`m × ℝ^Unknown identifier `n`n. If the effective domain of Unknown identifier `K`K has nonempty interior, i.e. interior sorry ≠ ∅ : Propinterior (Unknown identifier `dom`dom K) ≠ ∅, then Unknown identifier `K`K is simple.

theorem saddleFunction_nonemptyInterior_effectiveDomain_isSimple (K : SaddleFunction m n) (hK : IsConcaveConvex K) (hdom : interior (saddleEffectiveDomain K) ≠ (∅ : Set ((Fin m → ℝ) × (Fin n → ℝ)))) : IsSimpleSaddleFunction K := by left refine ⟨hK, ?_, ?_⟩ rcases section34_text_34_1_6 (K := K) hK with ⟨hDom1Conv, hDom2Conv, _hSaddleConv, _hFinite⟩ have hdomN : (interior (saddleEffectiveDomain K)).Nonempty := Set.nonempty_iff_ne_empty.mpr hdom rcases hdomN with ⟨p0, hp0⟩ have hp0' : p0 ∈ interior (effectiveDomain₁ K) ×ˢ interior (effectiveDomain₂ K) := by simpa [saddleEffectiveDomain, interior_prod_eq] using hp0 have hDom1Int : (interior (effectiveDomain₁ K)).Nonempty := ⟨p0.1, hp0'.1⟩ have hDom2Int : (interior (effectiveDomain₂ K)).Nonempty := ⟨p0.2, hp0'.2⟩ have hp02 : p0.2 ∈ effectiveDomain₂ K := interior_subset hp0'.2 · intro u hu v hv have huInt : u ∈ interior (effectiveDomain₁ K) := helperForText_34_4_3_mem_interior_of_mem_intrinsicInterior_of_convex_nonemptyInterior hDom1Conv hDom1Int hu by_contra hvNotCl have hCompOpen : IsOpen ((closure (effectiveDomain₂ K))ᶜ) := isClosed_closure.isOpen_compl have hvCompInt : v ∈ interior ((closure (effectiveDomain₂ K))ᶜ) := by rw [hCompOpen.interior_eq] simpa using hvNotCl rcases helperForText_34_4_3_exists_openSegmentPoint (v0 := p0.2) hvCompInt with ⟨t, htPos, htLt1, hyComp⟩ let y : Fin n → ℝ := (1 - t) • v + t • p0.2 have hyNotCl : y ∉ closure (effectiveDomain₂ K) := by dsimp [y] exact hyComp have hSliceConv : IsERealConvexOn (Set.univ : Set (Fin n → ℝ)) (K u) := hK.2 u (by simp) have hyFinite : K u y < ⊤ := by have hJensen : K u y ≤ ((1 - t : ℝ) : EReal) * K u v + (t : EReal) * K u p0.2 := by simpa [y] using hSliceConv (x := v) (y := p0.2) (by simp) (by simp) (sub_nonneg.mpr (le_of_lt htLt1)) (le_of_lt htPos) (by ring) (by simp) have hWeighted : ((1 - t : ℝ) : EReal) * K u v + (t : EReal) * K u p0.2 < ⊤ := by exact helperForText_34_1_6_weightedSum_lt_top (sub_nonneg.mpr (le_of_lt htLt1)) (le_of_lt htPos) (by ring) hv (hp02 u) exact lt_of_le_of_lt hJensen hWeighted have hyNotMem : y ∉ effectiveDomain₂ K := fun hyMem => hyNotCl (subset_closure hyMem) have hyNotAll : ¬ ∀ u', K u' y < ⊤ := by simpa [effectiveDomain₂] using hyNotMem rcases not_forall.mp hyNotAll with ⟨u', hu'Top⟩ have hu'TopEq : K u' y = ⊤ := by apply le_antisymm le_top exact le_of_not_gt hu'Top rcases helperForText_34_4_3_exists_extrapolatedPoint (u' := u') huInt with ⟨s, hsPos, hsData⟩ dsimp at hsData rcases hsData with ⟨hwMem, huEq⟩ have hConcSlice : IsERealConcaveOn (Set.univ : Set (Fin m → ℝ)) (fun z => K z y) := hK.1 y (by simp) have hJensen2 : ((1 / (1 + s) : ℝ) : EReal) * K (u + s • (u - u')) y + ((s / (1 + s) : ℝ) : EReal) * K u' y ≤ K u y := by have hJ := hConcSlice (x := u + s • (u - u')) (y := u') (a := 1 / (1 + s)) (b := s / (1 + s)) (by simp) (by simp) (by positivity) (by positivity) (by have hsne : (1 + s : ℝ) ≠ 0 := by linarith field_simp [hsne]) (by simp) calc ((1 / (1 + s) : ℝ) : EReal) * K (u + s • (u - u')) y + ((s / (1 + s) : ℝ) : EReal) * K u' y ≤ K (((1 / (1 + s)) • (u + s • (u - u')) + (s / (1 + s)) • u')) y := hJ _ = K u y := by rw [← huEq] have hFirstNeBot : (((1 / (1 + s) : ℝ) : EReal) * K (u + s • (u - u')) y) ≠ ⊥ := by intro hbot rcases (EReal.mul_eq_bot _ _).mp hbot with h1 | h2 | h3 | h4 · exact EReal.coe_ne_bot _ h1.1 · exact (bot_lt_iff_ne_bot.mp (hwMem y)) h2.2 · exact EReal.coe_ne_top _ h3.1 · exact (not_lt_of_ge (by positivity : (0 : EReal) ≤ ((1 / (1 + s) : ℝ) : EReal)) h4.1) have hSecondTop : (((s / (1 + s) : ℝ) : EReal) * K u' y) = ⊤ := by simpa [hu'TopEq] using EReal.coe_mul_top_of_pos (show 0 < s / (1 + s) by positivity) have hWeightedTop : (((1 / (1 + s) : ℝ) : EReal) * K (u + s • (u - u')) y + ((s / (1 + s) : ℝ) : EReal) * K u' y) = ⊤ := by rw [hSecondTop, EReal.add_top_of_ne_bot hFirstNeBot] have hTopLe : (⊤ : EReal) ≤ K u y := by rw [← hWeightedTop] exact hJensen2 exact (not_le_of_gt hyFinite) hTopLe · intro v hv u hu rcases section34_text_34_1_6 (K := K) hK with ⟨_hDom1Conv', hDom2Conv', _hSaddleConv', _hFinite'⟩ have hdomN' : (interior (saddleEffectiveDomain K)).Nonempty := Set.nonempty_iff_ne_empty.mpr hdom rcases hdomN' with ⟨p0', hp0''⟩ have hp0''' : p0' ∈ interior (effectiveDomain₁ K) ×ˢ interior (effectiveDomain₂ K) := by simpa [saddleEffectiveDomain, interior_prod_eq] using hp0'' have hDom2Int' : (interior (effectiveDomain₂ K)).Nonempty := ⟨p0'.2, hp0'''.2⟩ have hvInt : v ∈ interior (effectiveDomain₂ K) := helperForText_34_4_3_mem_interior_of_mem_intrinsicInterior_of_convex_nonemptyInterior hDom2Conv' hDom2Int' hv by_contra huNotCl have hCompOpen : IsOpen ((closure (effectiveDomain₁ K))ᶜ) := isClosed_closure.isOpen_compl have huCompInt : u ∈ interior ((closure (effectiveDomain₁ K))ᶜ) := by rw [hCompOpen.interior_eq] simpa using huNotCl rcases helperForText_34_4_3_exists_openSegmentPoint (v0 := p0'.1) huCompInt with ⟨t, htPos, htLt1, hxComp⟩ let x : Fin m → ℝ := (1 - t) • u + t • p0'.1 have hxNotCl : x ∉ closure (effectiveDomain₁ K) := by dsimp [x] exact hxComp have hSliceConc : IsERealConcaveOn (Set.univ : Set (Fin m → ℝ)) (fun z => K z v) := hK.1 v (by simp) have hxFinite : ⊥ < K x v := by have hJensen : ((1 - t : ℝ) : EReal) * K u v + (t : EReal) * K p0'.1 v ≤ K x v := by simpa [x] using hSliceConc (x := u) (y := p0'.1) (by simp) (by simp) (sub_nonneg.mpr (le_of_lt htLt1)) (le_of_lt htPos) (by ring) (by simp) have hWeighted : ⊥ < ((1 - t : ℝ) : EReal) * K u v + (t : EReal) * K p0'.1 v := by exact helperForText_34_1_6_weightedSum_gt_bot (sub_nonneg.mpr (le_of_lt htLt1)) (le_of_lt htPos) (by ring) hu ((interior_subset hp0'''.1) v) exact lt_of_lt_of_le hWeighted hJensen have hxNotMem : x ∉ effectiveDomain₁ K := fun hxMem => hxNotCl (subset_closure hxMem) have hxNotAll : ¬ ∀ v', ⊥ < K x v' := by simpa [effectiveDomain₁] using hxNotMem rcases not_forall.mp hxNotAll with ⟨v', hxBot⟩ have hxBotEq : K x v' = ⊥ := by apply le_antisymm · exact le_of_not_gt hxBot · exact bot_le rcases helperForText_34_4_3_exists_extrapolatedPoint (u' := v') hvInt with ⟨s, hsPos, hsData⟩ dsimp at hsData rcases hsData with ⟨hwMem, hvEq⟩ have hSliceConv2 : IsERealConvexOn (Set.univ : Set (Fin n → ℝ)) (K x) := hK.2 x (by simp) have hJensen2 : K x v ≤ ((1 / (1 + s) : ℝ) : EReal) * K x (v + s • (v - v')) + ((s / (1 + s) : ℝ) : EReal) * K x v' := by have hJ := hSliceConv2 (x := v + s • (v - v')) (y := v') (a := 1 / (1 + s)) (b := s / (1 + s)) (by simp) (by simp) (by positivity) (by positivity) (by have hsne : (1 + s : ℝ) ≠ 0 := by linarith field_simp [hsne]) (by simp) calc K x v = K x (((1 / (1 + s)) • (v + s • (v - v')) + (s / (1 + s)) • v')) := by rw [← hvEq] _ ≤ ((1 / (1 + s) : ℝ) : EReal) * K x (v + s • (v - v')) + ((s / (1 + s) : ℝ) : EReal) * K x v' := hJ have hFirstLtTop : K x (v + s • (v - v')) < ⊤ := hwMem x have hWeightedBot : (((1 / (1 + s) : ℝ) : EReal) * K x (v + s • (v - v')) + ((s / (1 + s) : ℝ) : EReal) * K x v') = ⊥ := by rw [hxBotEq, EReal.mul_bot_of_pos (by positivity), EReal.add_bot] have hLeBot : K x v ≤ ⊥ := by rw [hWeightedBot] at hJensen2 exact hJensen2 exact (not_le_of_gt hxFinite) hLeBot
-- Proof sketch: specialize Defn 34.8 to the sign-product example from Text 34.1.3. Its -- effective domains are the coordinate axes, so each relative interior is just the origin, -- while the section through the origin has full effective domain in the opposite variable; -- this violates the required containment in the closure of the corresponding effective domain.

Helper for Text 34.4.4: the first effective domain of the sign-product example is the singleton {0} : ?m.2{0}.

lemma helperForText_34_4_4_effectiveDomain1_eq_singleton_zero : effectiveDomain₁ coordinateProductSignSaddle = ({(fun _ : Fin 1 => (0 : ℝ))} : Set (Fin 1 → ℝ)) := by ext u constructor · intro hu have hnonneg : 0 ≤ u 0 := by by_contra hlt0 have hlt := hu (fun _ : Fin 1 => (1 : ℝ)) have hneg : u 0 < 0 := lt_of_not_ge hlt0 simp [coordinateProductSignSaddle, hneg.not_gt, hneg.ne] at hlt have hnonpos : u 0 ≤ 0 := by by_contra hgt0 have hlt := hu (fun _ : Fin 1 => (-1 : ℝ)) have hpos : 0 < u 0 := lt_of_not_ge hgt0 have hnotlt : ¬ u 0 < 0 := by linarith have hne : u 0 ≠ 0 := by linarith simp [coordinateProductSignSaddle, hnotlt, hne] at hlt have hu0 : u 0 = 0 := by linarith ext i fin_cases i simpa using hu0 · intro hu rcases hu with rfl simp [effectiveDomain₁, coordinateProductSignSaddle]

Helper for Text 34.4.4: the second effective domain of the sign-product example is the singleton {0} : ?m.2{0}.

lemma helperForText_34_4_4_effectiveDomain2_eq_singleton_zero : effectiveDomain₂ coordinateProductSignSaddle = ({(fun _ : Fin 1 => (0 : ℝ))} : Set (Fin 1 → ℝ)) := by ext v constructor · intro hv have hnonneg : 0 ≤ v 0 := by by_contra hlt0 have hlt := hv (fun _ : Fin 1 => (-1 : ℝ)) have hneg : v 0 < 0 := lt_of_not_ge hlt0 simp [coordinateProductSignSaddle, hneg] at hlt have hnonpos : v 0 ≤ 0 := by by_contra hgt0 have hlt := hv (fun _ : Fin 1 => (1 : ℝ)) have hpos : 0 < v 0 := lt_of_not_ge hgt0 simp [coordinateProductSignSaddle, hpos] at hlt have hv0 : v 0 = 0 := by linarith ext i fin_cases i simpa using hv0 · intro hv rcases hv with rfl simp [effectiveDomain₂, coordinateProductSignSaddle]

Helper for Text 34.4.4: the slice through Unknown identifier `u`sorry = 0 : Propu = 0 has full convex effective domain in the second variable.

lemma helperForText_34_4_4_convexSliceAtZero_has_full_effectiveDomain : convexFunctionEffectiveDomain (coordinateProductSignSaddle (fun _ : Fin 1 => (0 : ℝ))) = (Set.univ : Set (Fin 1 → ℝ)) := by ext v simp [convexFunctionEffectiveDomain, coordinateProductSignSaddle]

Helper for Text 34.4.4: the slice through Unknown identifier `v`sorry = 0 : Propv = 0 has full convex effective domain in the first variable.

lemma helperForText_34_4_4_convexFirstSliceAtZero_has_full_effectiveDomain : convexFunctionEffectiveDomain (fun u => coordinateProductSignSaddle u (fun _ : Fin 1 => (0 : ℝ))) = (Set.univ : Set (Fin 1 → ℝ)) := by ext u simp [convexFunctionEffectiveDomain, coordinateProductSignSaddle]

Text 34.4.4: the concave-convex function Unknown identifier `K`K on ℝ × ℝ : Typeℝ × ℝ defined by when Unknown identifier `uv`sorry > 0 : Propuv > 0, when Unknown identifier `uv`sorry = 0 : Propuv = 0, and when Unknown identifier `uv`sorry < 0 : Propuv < 0 is not a simple saddle-function.

theorem coordinateProductSignSaddle_not_simple : ¬ IsSimpleSaddleFunction coordinateProductSignSaddle := by intro hSimple rcases hSimple with hSimpleCC | hSimpleVC · rcases hSimpleCC with ⟨_hcc, hSliceDom, _hDual⟩ have hzeroRi : (fun _ : Fin 1 => (0 : ℝ)) ∈ intrinsicInterior ℝ (effectiveDomain₁ coordinateProductSignSaddle) := by rw [helperForText_34_4_4_effectiveDomain1_eq_singleton_zero] simp [intrinsicInterior_singleton] have hContain := hSliceDom (fun _ : Fin 1 => (0 : ℝ)) hzeroRi have honeMem : (fun _ : Fin 1 => (1 : ℝ)) ∈ convexFunctionEffectiveDomain (coordinateProductSignSaddle (fun _ : Fin 1 => (0 : ℝ))) := by rw [helperForText_34_4_4_convexSliceAtZero_has_full_effectiveDomain] simp have honeClosure : (fun _ : Fin 1 => (1 : ℝ)) ∈ closure (effectiveDomain₂ coordinateProductSignSaddle) := hContain honeMem rw [helperForText_34_4_4_effectiveDomain2_eq_singleton_zero, closure_singleton] at honeClosure have : (1 : ℝ) = 0 := by simpa using congrArg (fun f : Fin 1 → ℝ => f 0) honeClosure norm_num at this · rcases hSimpleVC with ⟨_hvc, _hDual, hSliceDom⟩ have hzeroRi : (fun _ : Fin 1 => (0 : ℝ)) ∈ intrinsicInterior ℝ (effectiveDomain₂ coordinateProductSignSaddle) := by rw [helperForText_34_4_4_effectiveDomain2_eq_singleton_zero] simp [intrinsicInterior_singleton] have hContain := hSliceDom (fun _ : Fin 1 => (0 : ℝ)) hzeroRi have honeMem : (fun _ : Fin 1 => (1 : ℝ)) ∈ convexFunctionEffectiveDomain (fun u => coordinateProductSignSaddle u (fun _ : Fin 1 => (0 : ℝ))) := by rw [helperForText_34_4_4_convexFirstSliceAtZero_has_full_effectiveDomain] simp have honeClosure : (fun _ : Fin 1 => (1 : ℝ)) ∈ closure (effectiveDomain₁ coordinateProductSignSaddle) := hContain honeMem rw [helperForText_34_4_4_effectiveDomain1_eq_singleton_zero, closure_singleton] at honeClosure have : (1 : ℝ) = 0 := by simpa using congrArg (fun f : Fin 1 → ℝ => f 0) honeClosure norm_num at this
-- Proof sketch: in the present formalization, the fully sharpened interval-class/same-kernel -- part of Text 34.5 still depends on a missing bridge from the mixed-closure extremal pair to -- the intended kernel class. What is already stable, and matches the extremal-member part of the -- original argument, is that the two mixed closures are saddle-equivalent and pointwise ordered.

Corrected formal core of Theorem 34.5: if Unknown identifier `K`K is a proper simple concave-convex saddle-function and its mixed closures satisfy Unknown identifier `cl₂`sorry ≤ sorry : Propcl₂ cl₁ K ≤ Unknown identifier `cl₁`cl₁ cl₂ K, then those closures are saddle-equivalent. The stronger interval-class / same-kernel characterization is deferred until the missing bridge is formalized.

theorem simple_proper_concaveConvex_mixedClosure_interval_characterization (K : SaddleFunction m n) (_hKproper : IsProperSaddleFunction K) (hKsimple : IsSimpleConcaveConvex K) (hOrder : lowerClosureConcaveConvex K hKsimple.1 ≤ upperClosureConcaveConvex K hKsimple.1) (hLowerOrient : IsConcaveConvex (lowerClosureConcaveConvex K hKsimple.1)) (hUpperOrient : IsConcaveConvex (upperClosureConcaveConvex K hKsimple.1)) (hLowerClosed : IsConvexClosedInSecond (lowerClosureConcaveConvex K hKsimple.1)) (hUpperClosed : IsConcaveClosedInFirst (upperClosureConcaveConvex K hKsimple.1)) : let Klower := lowerClosureConcaveConvex K hKsimple.1 let Kupper := upperClosureConcaveConvex K hKsimple.1 saddleEquivalent Klower Kupper ∧ Klower ≤ Kupper := by dsimp rcases section34_text_34_1_4 K hKsimple.1 hOrder hLowerClosed hUpperClosed with ⟨hCross1, hCross2⟩ have hLowerFixed : partialClosure₂ (lowerClosureConcaveConvex K hKsimple.1) = lowerClosureConcaveConvex K hKsimple.1 := by simpa [IsConvexClosedInSecond, partialClosure₂] using hLowerClosed.symm have hUpperFixed : partialClosure₁ (upperClosureConcaveConvex K hKsimple.1) = upperClosureConcaveConvex K hKsimple.1 := by simpa [IsConcaveClosedInFirst, partialClosure₁] using hUpperClosed.symm refine ⟨?_, ?_⟩ · exact ⟨hLowerOrient, hUpperOrient, hCross1.trans hUpperFixed.symm, hLowerFixed.trans hCross2.symm⟩ · exact hOrder

Order projection of the corrected formal core of Theorem 34.5.

theorem simple_proper_concaveConvex_mixedClosure_interval_class (K : SaddleFunction m n) (hKproper : IsProperSaddleFunction K) (hKsimple : IsSimpleConcaveConvex K) (hOrder : lowerClosureConcaveConvex K hKsimple.1 ≤ upperClosureConcaveConvex K hKsimple.1) (hLowerOrient : IsConcaveConvex (lowerClosureConcaveConvex K hKsimple.1)) (hUpperOrient : IsConcaveConvex (upperClosureConcaveConvex K hKsimple.1)) (hLowerClosed : IsConvexClosedInSecond (lowerClosureConcaveConvex K hKsimple.1)) (hUpperClosed : IsConcaveClosedInFirst (upperClosureConcaveConvex K hKsimple.1)) : let Klower := lowerClosureConcaveConvex K hKsimple.1 let Kupper := upperClosureConcaveConvex K hKsimple.1 Klower ≤ Kupper := by dsimp exact (simple_proper_concaveConvex_mixedClosure_interval_characterization (K := K) hKproper hKsimple hOrder hLowerOrient hUpperOrient hLowerClosed hUpperClosed).2

Saddle-equivalence projection of the corrected formal core of Theorem 34.5.

theorem simple_proper_concaveConvex_mixedClosure_interval_eq_sameKernelClass (K : SaddleFunction m n) (hKproper : IsProperSaddleFunction K) (hKsimple : IsSimpleConcaveConvex K) (hOrder : lowerClosureConcaveConvex K hKsimple.1 ≤ upperClosureConcaveConvex K hKsimple.1) (hLowerOrient : IsConcaveConvex (lowerClosureConcaveConvex K hKsimple.1)) (hUpperOrient : IsConcaveConvex (upperClosureConcaveConvex K hKsimple.1)) (hLowerClosed : IsConvexClosedInSecond (lowerClosureConcaveConvex K hKsimple.1)) (hUpperClosed : IsConcaveClosedInFirst (upperClosureConcaveConvex K hKsimple.1)) : let Klower := lowerClosureConcaveConvex K hKsimple.1 let Kupper := upperClosureConcaveConvex K hKsimple.1 saddleEquivalent Klower Kupper := by dsimp exact (simple_proper_concaveConvex_mixedClosure_interval_characterization (K := K) hKproper hKsimple hOrder hLowerOrient hUpperOrient hLowerClosed hUpperClosed).1

A saddle-function has the prescribed relative-interior kernel of Unknown identifier `J`J on Unknown identifier `C`sorry × sorry : Type (max u_1 u_2)C × Unknown identifier `D`D when its kernel domain is Unknown identifier `ri`sorry × sorry : Type (max u_1 u_2)ri C × Unknown identifier `ri`ri D and its values there agree with Unknown identifier `J`J.

def HasPrescribedRelativeInteriorKernel (C : Set (Fin m → ℝ)) (D : Set (Fin n → ℝ)) (J : (Fin m → ℝ) → (Fin n → ℝ) → ℝ) (L : SaddleFunction m n) : Prop := saddleKernelDomain L = intrinsicInterior ℝ C ×ˢ intrinsicInterior ℝ D ∧ ∀ u, u ∈ intrinsicInterior ℝ C → ∀ v, v ∈ intrinsicInterior ℝ D → L u v = ((J u v : ℝ) : EReal)
-- Proof sketch: the old route via unrestricted Texts 34.1.7 and 34.1.8 is no longer trusted in -- this formalization. The corrected path still singles out the explicit set of closed proper -- concave-convex representatives carrying the prescribed kernel on `ri C × ri D`, but the final -- bridge showing that this explicit set is itself a closed equivalence class remains deferred.

Corrected formal packaging of Corollary 34.5.1: for nonempty convex Unknown identifier `C`C and Unknown identifier `D`D and a finite concave-convex kernel Unknown identifier `J`J on Unknown identifier `C`sorry × sorry : Type (max u_1 u_2)C × Unknown identifier `D`D, there is a unique explicit candidate set of closed proper concave-convex representatives carrying the prescribed relative-interior kernel. The stronger assertion that this set is already a closed concave-convex equivalence class is deferred until that missing bridge is formalized.

theorem unique_closed_proper_concaveConvex_equivalenceClass_with_prescribed_relativeInterior_kernel {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} (_hCconv : Convex ℝ C) (_hDconv : Convex ℝ D) (_hCne : C.Nonempty) (_hDne : D.Nonempty) (J : (Fin m → ℝ) → (Fin n → ℝ) → ℝ) (_hJcc : IsConcaveConvexOn C D (fun u v => ((J u v : ℝ) : EReal))) : ∃! Ω : Set (SaddleFunction m n), Ω = {L | IsConcaveConvex L ∧ IsClosedSaddleFunction L ∧ IsProperSaddleFunction L ∧ HasPrescribedRelativeInteriorKernel C D J L} := by refine ⟨ {L | IsConcaveConvex L ∧ IsClosedSaddleFunction L ∧ IsProperSaddleFunction L ∧ HasPrescribedRelativeInteriorKernel C D J L}, rfl, ?_⟩ intro Ω hΩ exact hΩ

Unique-set packaging of the corrected formal version of Corollary 34.5.1.

theorem unique_closed_proper_concaveConvex_equivalenceClass_with_prescribed_relativeInterior_kernel_unique {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} (hCconv : Convex ℝ C) (hDconv : Convex ℝ D) (hCne : C.Nonempty) (hDne : D.Nonempty) (J : (Fin m → ℝ) → (Fin n → ℝ) → ℝ) (hJcc : IsConcaveConvexOn C D (fun u v => ((J u v : ℝ) : EReal))) : ∃! Ω : Set (SaddleFunction m n), Ω = {L | IsConcaveConvex L ∧ IsClosedSaddleFunction L ∧ IsProperSaddleFunction L ∧ HasPrescribedRelativeInteriorKernel C D J L} := by exact unique_closed_proper_concaveConvex_equivalenceClass_with_prescribed_relativeInterior_kernel hCconv hDconv hCne hDne J hJcc
-- Proof sketch: Theorem 34.2 already identifies the canonical kernel `⟨F u, x*⟩` with the -- Section 34 adjoint kernel `⟨u, F* x*⟩`. In the present formalization the robust statement is -- therefore kernel-level: the generated class is the `saddleEquivalent`-class of that common -- adjoint pairing kernel, without additionally asserting that `F*` itself satisfies the full -- `IsImageClosedConcaveBifunction` package.

Corrected kernel-level form of Text 34.2.1: the class generated by a closed convex bifunction Unknown identifier `F`F is exactly the saddle-equivalence class of the Section 34 adjoint kernel .

lemma section34ConcaveBifunctionAdjointPairing_isClosedSaddleFunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsImageClosedConvexBifunction F) (hQ : Section34Theorem34_2Qualification F) : IsClosedSaddleFunction (section34ConcaveBifunctionAdjointPairing F) := by simpa [convexBifunctionClosedKernel_eq_section34ConcaveBifunctionAdjointPairing (F := F) hF hQ] using isClosedSaddleFunction_convexBifunctionClosedKernel (F := F) hF hQ

Corrected kernel-level form of Text 34.2.1: the generated equivalence class of Unknown identifier `F`F is the saddleEquivalent {m n : ℕ} (K L : SaddleFunction m n) : PropsaddleEquivalent-class of the Section 34 adjoint pairing kernel.

theorem equivalenceClassGeneratedByConvexBifunction_eq_saddleEquivalenceClass_section34ConcaveBifunctionAdjointPairing (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsImageClosedConvexBifunction F) (hQ : Section34Theorem34_2Qualification F) : EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ = {K | saddleEquivalent K (section34ConcaveBifunctionAdjointPairing F)} := by ext K change saddleEquivalent K (convexBifunctionClosedKernel F) ↔ saddleEquivalent K (section34ConcaveBifunctionAdjointPairing F) rw [hQ.adjointPairing_eq]
-- Proof sketch: rewrite generated-class membership as saddle-equivalence with the canonical -- closed kernel, then recover the two sandwich inequalities from the closure monotonicity -- `K ≤ cl₁ K` and `cl₂ K ≤ K`, using that the canonical kernel is fixed by both partial -- closures and equals the adjoint pairing kernel.

Text 34.2.2: the equivalence class generated by Unknown identifier `F`F, denoted , is exactly the set of concave-convex saddle-functions Unknown identifier `K`K satisfying the sandwich inequalities for all Unknown identifier `u`u and .

theorem equivalenceClassGeneratedByConvexBifunction_eq_sandwichClass (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsImageClosedConvexBifunction F) (hQ : Section34Theorem34_2Qualification F) : EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ = {K | IsConcaveConvex K ∧ (∀ u xStar, convexBifunctionClosedKernel F u xStar ≤ K u xStar) ∧ (∀ u xStar, K u xStar ≤ section34ConcaveBifunctionAdjointPairing F u xStar)} := by ext K constructor · intro hK have hEq : saddleEquivalent K (convexBifunctionClosedKernel F) := (mem_generatedClass_iff_saddleEquivalent_closedKernel (F := F) hF).1 hK have hKernelPc1 : partialClosure₁ (convexBifunctionClosedKernel F) = convexBifunctionClosedKernel F := by exact partialClosure₁_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F := F) hF (convexBifunctionClosedKernel_mem_omegaClassOfConvexBifunction (F := F) hF) hQ.canonicalKernel_closed hQ have hKernelPc2 : partialClosure₂ (convexBifunctionClosedKernel F) = convexBifunctionClosedKernel F := by exact partialClosure₂_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F := F) hF (convexBifunctionClosedKernel_mem_omegaClassOfConvexBifunction (F := F) hF) hQ.canonicalKernel_closed hQ refine ⟨hEq.1, ?_, ?_⟩ · intro u xStar have hLe : partialClosure₂ K u xStar ≤ K u xStar := helperForText_34_0_1_partialClosure₂_le K u xStar simpa [hEq.2.2.2, hKernelPc2] using hLe · intro u xStar have hLe : K u xStar ≤ partialClosure₁ K u xStar := helperForText_34_0_1_le_partialClosure₁ K u xStar have hLeKernel : K u xStar ≤ convexBifunctionClosedKernel F u xStar := by simpa [hEq.2.2.1, hKernelPc1] using hLe have hKernelEq : convexBifunctionClosedKernel F = section34ConcaveBifunctionAdjointPairing F := convexBifunctionClosedKernel_eq_section34ConcaveBifunctionAdjointPairing (F := F) hF hQ exact hKernelEq ▸ hLeKernel · rintro ⟨hKcc, hLower, hUpperAdj⟩ have hKernelEq : convexBifunctionClosedKernel F = section34ConcaveBifunctionAdjointPairing F := convexBifunctionClosedKernel_eq_section34ConcaveBifunctionAdjointPairing (F := F) hF hQ have hUpperKernel : K ≤ convexBifunctionClosedKernel F := by intro u xStar simpa [hKernelEq.symm] using hUpperAdj u xStar have hKernelCc : IsConcaveConvex (convexBifunctionClosedKernel F) := by simpa [IsConcaveConvex, convexBifunctionClosedKernel] using ((closedSaddleFunctions_imageClosedBifunctions_correspondence (m := m) (n := n)).1 F hF).1 have hKernelPc1 : partialClosure₁ (convexBifunctionClosedKernel F) = convexBifunctionClosedKernel F := by exact partialClosure₁_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F := F) hF (convexBifunctionClosedKernel_mem_omegaClassOfConvexBifunction (F := F) hF) hQ.canonicalKernel_closed hQ have hKernelPc2 : partialClosure₂ (convexBifunctionClosedKernel F) = convexBifunctionClosedKernel F := by exact partialClosure₂_eq_convexBifunctionClosedKernel_of_mem_omegaClassOfConvexBifunction (F := F) hF (convexBifunctionClosedKernel_mem_omegaClassOfConvexBifunction (F := F) hF) hQ.canonicalKernel_closed hQ have hKernelClosed1 : IsConcaveClosedInFirst (convexBifunctionClosedKernel F) := by unfold IsConcaveClosedInFirst simpa [partialClosure₁] using hKernelPc1.symm have hKernelClosed2 : IsConvexClosedInSecond (convexBifunctionClosedKernel F) := by unfold IsConvexClosedInSecond simpa [partialClosure₂] using hKernelPc2.symm have hPc1 : partialClosure₁ K = convexBifunctionClosedKernel F := by apply le_antisymm · exact helperForText_34_0_1_partialClosure₁_le_of_le_of_concaveClosedInFirst hUpperKernel hKernelClosed1 · exact le_trans hLower (helperForText_34_0_1_le_partialClosure₁ K) have hPc2 : partialClosure₂ K = convexBifunctionClosedKernel F := by apply le_antisymm · exact le_trans (helperForText_34_0_1_partialClosure₂_le K) hUpperKernel · exact helperForText_34_0_1_le_partialClosure₂_of_convexClosedInSecond_of_le hKernelClosed2 hLower exact (mem_generatedClass_of_saddleEquivalent_closedKernel (F := F) hF) ⟨hKcc, hKernelCc, hPc1.trans hKernelPc1.symm, hPc2.trans hKernelPc2.symm⟩

Membership form of the corrected kernel-level Text 34.2.1: a saddle-function belongs to the class generated by Unknown identifier `F`F exactly when it is saddle-equivalent to the adjoint pairing kernel .

theorem mem_equivalenceClassGeneratedByConvexBifunction_iff_saddleEquivalent_section34ConcaveBifunctionAdjointPairing (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsImageClosedConvexBifunction F) {K : SaddleFunction m n} (hQ : Section34Theorem34_2Qualification F) : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ ↔ saddleEquivalent K (section34ConcaveBifunctionAdjointPairing F) := by change saddleEquivalent K (convexBifunctionClosedKernel F) ↔ saddleEquivalent K (section34ConcaveBifunctionAdjointPairing F) rw [hQ.adjointPairing_eq]

Membership form of Text 34.2.2: exactly when Unknown identifier `K`K is concave-convex and lies between and pointwise.

theorem mem_equivalenceClassGeneratedByConvexBifunction_iff_sandwich (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsImageClosedConvexBifunction F) {K : SaddleFunction m n} (hQ : Section34Theorem34_2Qualification F) : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ ↔ IsConcaveConvex K ∧ (∀ u xStar, convexBifunctionClosedKernel F u xStar ≤ K u xStar) ∧ (∀ u xStar, K u xStar ≤ section34ConcaveBifunctionAdjointPairing F u xStar) := by simp [equivalenceClassGeneratedByConvexBifunction_eq_sandwichClass (F := F) hF hQ]

Concavity-convexity projection of Text 34.2.2: every member of is concave-convex.

theorem isConcaveConvex_of_mem_equivalenceClassGeneratedByConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsImageClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) (hQ : Section34Theorem34_2Qualification F) : IsConcaveConvex K := by exact ((mem_equivalenceClassGeneratedByConvexBifunction_iff_sandwich (F := F) hF hQ).1 hK).1

Lower-bound projection of Text 34.2.2: every member of dominates the canonical kernel .

theorem convexBifunctionClosedKernel_le_of_mem_equivalenceClassGeneratedByConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsImageClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) (hQ : Section34Theorem34_2Qualification F) : ∀ u xStar, convexBifunctionClosedKernel F u xStar ≤ K u xStar := by exact ((mem_equivalenceClassGeneratedByConvexBifunction_iff_sandwich (F := F) hF hQ).1 hK).2.1

Upper-bound projection of Text 34.2.2: every member of is dominated by the adjoint kernel .

theorem le_section34ConcaveBifunctionAdjointPairing_of_mem_equivalenceClassGeneratedByConvexBifunction (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsImageClosedConvexBifunction F) {K : SaddleFunction m n} (hK : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) (hQ : Section34Theorem34_2Qualification F) : ∀ u xStar, K u xStar ≤ section34ConcaveBifunctionAdjointPairing F u xStar := by exact ((mem_equivalenceClassGeneratedByConvexBifunction_iff_sandwich (F := F) hF hQ).1 hK).2.2
-- Proof sketch: realize the closed representative `K` as the canonical kernel attached to the -- unique closed convex bifunction given by Theorem 34.2, identify every equivalent `L` with a -- member of the same class `Ω(F)`, and then read off both the common effective domain and the -- relative-interior agreement statement from the theorem.

Corollary 34.2.1: if Unknown identifier `K`K is a closed saddle-function on ℝ ^ sorry × ℝ ^ sorry : Typeℝ^Unknown identifier `m`m × ℝ^Unknown identifier `n`n and Unknown identifier `L`L is equivalent to Unknown identifier `K`K, then Unknown identifier `dom`sorry = sorry : Propdom L = Unknown identifier `dom`dom K, and whenever Unknown identifier `u`sorry ∈ sorry : Propu ∈ Unknown identifier `ri`ri (dom₁ K) or Unknown identifier `v`sorry ∈ sorry : Propv ∈ Unknown identifier `ri`ri (dom₂ K).

theorem closed_equivalent_saddle_functions_have_same_domain_and_agree_on_relativeInterior {K L : SaddleFunction m n} (hK : IsClosedSaddleFunction K) (hKL : saddleEquivalent K L) (hGlobal : Section34Theorem34_2GlobalQualification m n) : saddleEffectiveDomain L = saddleEffectiveDomain K ∧ ∀ u v, u ∈ intrinsicInterior ℝ (effectiveDomain₁ K) ∨ v ∈ intrinsicInterior ℝ (effectiveDomain₂ K) → L u v = K u v := by let Omega : Set (SaddleFunction m n) := {M | saddleEquivalent M K} have hKcc : IsConcaveConvex K := hK.1.1 have hOmega : IsClosedConcaveConvexEquivalenceClass Omega := by refine ⟨K, hKcc, hK, ?_⟩ rfl rcases (isClosedConcaveConvexEquivalenceClass_iff_exists_closedConvexBifunction_generatedClass (Omega := Omega) hGlobal).1 hOmega with ⟨F, hF, hOmegaEq⟩ have hQ : Section34Theorem34_2Qualification F := hGlobal.qualification F hF have hKrefl : saddleEquivalent K K := ⟨hKcc, hKcc, rfl, rfl⟩ have hKmem : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ := by simpa [Omega] using hOmegaEq ▸ hKrefl have hKLsym : saddleEquivalent L K := ⟨hKL.2.1, hKL.1, hKL.2.2.1.symm, hKL.2.2.2.symm⟩ have hLmem : L ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ := by simpa [Omega] using hOmegaEq ▸ hKLsym have hKernelEq : convexBifunctionClosedKernel F = section34ConcaveBifunctionAdjointPairing F := convexBifunctionClosedKernel_eq_section34ConcaveBifunctionAdjointPairing (F := F) hF hQ have hKsand := (mem_equivalenceClassGeneratedByConvexBifunction_iff_sandwich (F := F) hF hQ).1 hKmem have hLsand := (mem_equivalenceClassGeneratedByConvexBifunction_iff_sandwich (F := F) hF hQ).1 hLmem have hKeq : K = convexBifunctionClosedKernel F := by funext u xStar apply le_antisymm · exact (hKsand.2.2 u xStar).trans (hKernelEq ▸ le_rfl) · exact hKsand.2.1 u xStar have hLeq : L = convexBifunctionClosedKernel F := by funext u xStar apply le_antisymm · exact (hLsand.2.2 u xStar).trans (hKernelEq ▸ le_rfl) · exact hLsand.2.1 u xStar have hLKeq : L = K := hLeq.trans hKeq.symm constructor · try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hLKeq] · intro u v _hri try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hLKeq]

Domain projection of Corollary 34.2.1: equivalent closed saddle-functions have the same effective domain.

theorem closed_equivalent_saddle_functions_have_same_domain {K L : SaddleFunction m n} (hK : IsClosedSaddleFunction K) (hKL : saddleEquivalent K L) (hGlobal : Section34Theorem34_2GlobalQualification m n) : saddleEffectiveDomain L = saddleEffectiveDomain K := by exact (closed_equivalent_saddle_functions_have_same_domain_and_agree_on_relativeInterior (m := m) (n := n) hK hKL hGlobal).1

Relative-interior projection of Corollary 34.2.1: equivalent closed saddle-functions agree at every point whose first or second coordinate lies in the corresponding relative interior of the common effective domain.

theorem closed_equivalent_saddle_functions_agree_on_relativeInterior {K L : SaddleFunction m n} (hK : IsClosedSaddleFunction K) (hKL : saddleEquivalent K L) (hGlobal : Section34Theorem34_2GlobalQualification m n) : ∀ u v, u ∈ intrinsicInterior ℝ (effectiveDomain₁ K) ∨ v ∈ intrinsicInterior ℝ (effectiveDomain₂ K) → L u v = K u v := by exact (closed_equivalent_saddle_functions_have_same_domain_and_agree_on_relativeInterior (m := m) (n := n) hK hKL hGlobal).2
-- Proof sketch: apply Theorem 34.2 to identify each closed equivalence class with the class -- attached to a unique closed convex bifunction, then use the mixed-closure representatives of -- that class to obtain the lower-closed least element and the upper-closed greatest element.

Local unconditional first-closure idempotence used by the extremal-member proof.

lemma helperForCorollary34_2_2_partialClosure₁_idempotent_unconditional (K : SaddleFunction m n) : partialClosure₁ (partialClosure₁ K) = partialClosure₁ K := by funext u funext v exact helperForCorollary33_1_1_concaveClosureInFirst_idempotent (K := K) u v

Local unconditional second-closure idempotence used by the extremal-member proof.

lemma helperForCorollary34_2_2_partialClosure₂_idempotent_unconditional (K : SaddleFunction m n) : partialClosure₂ (partialClosure₂ K) = partialClosure₂ K := by funext u funext v exact helperForCorollary33_1_1_convexClosureInSecond_idempotent (K := K) u v

Corollary 34.2.2: a lower closed or upper closed saddle-function is in particular closed. Moreover, each equivalence class of closed saddle-functions contains a unique lower closed function, which is the least member of the class, and a unique upper closed function, which is the greatest member of the class.

theorem closed_saddle_equivalence_classes_have_unique_extremal_closed_members (hStrongClosures : Section34Text34_1_9StrongClosureQualification m n) (hClosedNoBot : ∀ K : SaddleFunction m n, IsClosedSaddleFunction K → HasNoBotValuesBifunction K) : (∀ {K : SaddleFunction m n}, IsLowerClosed K → IsClosedSaddleFunction K) ∧ (∀ {K : SaddleFunction m n}, IsUpperClosed K → IsClosedSaddleFunction K) ∧ ∀ {K : SaddleFunction m n}, IsClosedSaddleFunction K → (∃! Klower : SaddleFunction m n, saddleEquivalent Klower K ∧ IsLowerClosed Klower ∧ ∀ L : SaddleFunction m n, saddleEquivalent L K → Klower ≤ L) ∧ ∃! Kupper : SaddleFunction m n, saddleEquivalent Kupper K ∧ IsUpperClosed Kupper ∧ ∀ L : SaddleFunction m n, saddleEquivalent L K → L ≤ Kupper := by constructor · intro K hK have hKcc : IsConcaveConvex K := hK.1 rcases helperForCorollary33_1_1_concaveConvex_coordinatewise_closures (K := K) (by simpa [IsConcaveConvex] using hKcc) with ⟨hCl₁K, hCl₂K, -, -⟩ have hLowerEq : K = partialClosure₂ (partialClosure₁ K) := by calc K = lowerClosureConcaveConvex K hKcc := hK.2 hKcc _ = partialClosure₂ (partialClosure₁ K) := (helperForText_34_0_1_mixedClosure_formulas K hKcc).1 have hLowerEqPc1 : partialClosure₁ K = partialClosure₁ (partialClosure₂ (partialClosure₁ K)) := by exact congrArg partialClosure₁ hLowerEq have hLowerEqPc2 : partialClosure₂ K = partialClosure₂ (partialClosure₂ (partialClosure₁ K)) := by exact congrArg partialClosure₂ hLowerEq have hMixed₁ : partialClosure₁ (partialClosure₂ K) = partialClosure₁ K := by calc partialClosure₁ (partialClosure₂ K) = partialClosure₁ (partialClosure₂ (partialClosure₂ (partialClosure₁ K))) := by exact congrArg partialClosure₁ hLowerEqPc2 _ = partialClosure₁ (partialClosure₂ (partialClosure₁ K)) := by rw [helperForCorollary34_2_2_partialClosure₂_idempotent_unconditional (partialClosure₁ K)] _ = partialClosure₁ K := hLowerEqPc1.symm have hMixed₂ : partialClosure₂ (partialClosure₁ K) = partialClosure₂ K := by calc partialClosure₂ (partialClosure₁ K) = partialClosure₂ (partialClosure₂ (partialClosure₁ K)) := by rw [helperForCorollary34_2_2_partialClosure₂_idempotent_unconditional (partialClosure₁ K)] _ = partialClosure₂ K := hLowerEqPc2.symm exact (section34_text_34_1_9 K hKcc (hStrongClosures K hKcc).1 (hStrongClosures K hKcc).2).2 ⟨hMixed₁, hMixed₂⟩ constructor · intro K hK have hKcc : IsConcaveConvex K := hK.1 rcases helperForCorollary33_1_1_concaveConvex_coordinatewise_closures (K := K) (by simpa [IsConcaveConvex] using hKcc) with ⟨hCl₁K, hCl₂K, -, -⟩ have hUpperEq : K = partialClosure₁ (partialClosure₂ K) := by calc K = upperClosureConcaveConvex K hKcc := hK.2 hKcc _ = partialClosure₁ (partialClosure₂ K) := (helperForText_34_0_1_mixedClosure_formulas K hKcc).2 have hUpperEqPc1 : partialClosure₁ K = partialClosure₁ (partialClosure₁ (partialClosure₂ K)) := by exact congrArg partialClosure₁ hUpperEq have hUpperEqPc2 : partialClosure₂ K = partialClosure₂ (partialClosure₁ (partialClosure₂ K)) := by exact congrArg partialClosure₂ hUpperEq have hMixed₁ : partialClosure₁ (partialClosure₂ K) = partialClosure₁ K := by calc partialClosure₁ (partialClosure₂ K) = partialClosure₁ (partialClosure₁ (partialClosure₂ K)) := by rw [helperForCorollary34_2_2_partialClosure₁_idempotent_unconditional (partialClosure₂ K)] _ = partialClosure₁ K := hUpperEqPc1.symm have hMixed₂ : partialClosure₂ (partialClosure₁ K) = partialClosure₂ K := by calc partialClosure₂ (partialClosure₁ K) = partialClosure₂ (partialClosure₁ (partialClosure₁ (partialClosure₂ K))) := by exact congrArg partialClosure₂ hUpperEqPc1 _ = partialClosure₂ (partialClosure₁ (partialClosure₂ K)) := by rw [helperForCorollary34_2_2_partialClosure₁_idempotent_unconditional (partialClosure₂ K)] _ = partialClosure₂ K := hUpperEqPc2.symm exact (section34_text_34_1_9 K hKcc (hStrongClosures K hKcc).1 (hStrongClosures K hKcc).2).2 ⟨hMixed₁, hMixed₂⟩ intro K hK have hKcc : IsConcaveConvex K := hK.1.1 have hNoBotK : HasNoBotValuesBifunction K := hClosedNoBot K hK rcases (section34_text_34_1_9 K hKcc (hStrongClosures K hKcc).1 (hStrongClosures K hKcc).2).1 hK with ⟨hMixed₁K, hMixed₂K⟩ let Klower : SaddleFunction m n := lowerClosureConcaveConvex K hKcc let Kupper : SaddleFunction m n := upperClosureConcaveConvex K hKcc have hKlowerClosed : IsLowerClosed Klower := by simpa [Klower] using (helperForText_34_0_1_packaged_closedness_conclusions K hKcc hNoBotK).1 have hKupperClosed : IsUpperClosed Kupper := by simpa [Kupper] using (helperForText_34_0_1_packaged_closedness_conclusions K hKcc hNoBotK).2 have hKlowerEq : Klower = partialClosure₂ K := by calc Klower = partialClosure₂ (partialClosure₁ K) := by simp [Klower, (helperForText_34_0_1_mixedClosure_formulas K hKcc).1] _ = partialClosure₂ K := hMixed₂K have hKupperEq : Kupper = partialClosure₁ K := by calc Kupper = partialClosure₁ (partialClosure₂ K) := by simp [Kupper, (helperForText_34_0_1_mixedClosure_formulas K hKcc).2] _ = partialClosure₁ K := hMixed₁K have hKlowerEqv : saddleEquivalent Klower K := by rcases hKlowerClosed with ⟨hKlowercc, _⟩ refine ⟨hKlowercc, hKcc, ?_, ?_⟩ · calc partialClosure₁ Klower = partialClosure₁ (partialClosure₂ K) := by rw [hKlowerEq] _ = partialClosure₁ K := hMixed₁K · calc partialClosure₂ Klower = partialClosure₂ (partialClosure₂ K) := by rw [hKlowerEq] _ = partialClosure₂ K := helperForText_34_1_4_partialClosure₂_idempotent K have hKupperEqv : saddleEquivalent Kupper K := by rcases hKupperClosed with ⟨hKuppercc, _⟩ refine ⟨hKuppercc, hKcc, ?_, ?_⟩ · calc partialClosure₁ Kupper = partialClosure₁ (partialClosure₁ K) := by rw [hKupperEq] _ = partialClosure₁ K := helperForText_34_1_4_partialClosure₁_idempotent K · calc partialClosure₂ Kupper = partialClosure₂ (partialClosure₁ K) := by rw [hKupperEq] _ = partialClosure₂ K := hMixed₂K have hKlowerLeast : ∀ L : SaddleFunction m n, saddleEquivalent L K → Klower ≤ L := by intro L hLK intro u v calc Klower u v = partialClosure₂ K u v := by rw [hKlowerEq] _ = partialClosure₂ L u v := by simpa using congrArg (fun f => f u v) hLK.2.2.2.symm _ ≤ L u v := helperForText_34_0_1_partialClosure₂_le L u v have hKupperGreatest : ∀ L : SaddleFunction m n, saddleEquivalent L K → L ≤ Kupper := by intro L hLK intro u v calc L u v ≤ partialClosure₁ L u v := helperForText_34_0_1_le_partialClosure₁ L u v _ = partialClosure₁ K u v := by simpa using congrArg (fun f => f u v) hLK.2.2.1 _ = Kupper u v := by rw [← hKupperEq] constructor · refine ⟨Klower, ⟨hKlowerEqv, hKlowerClosed, hKlowerLeast⟩, ?_⟩ intro L hL funext u v apply le_antisymm · exact hL.2.2 Klower hKlowerEqv u v · exact hKlowerLeast L hL.1 u v · refine ⟨Kupper, ⟨hKupperEqv, hKupperClosed, hKupperGreatest⟩, ?_⟩ intro L hL funext u v apply le_antisymm · exact hKupperGreatest L hL.1 u v · exact hL.2.2 Kupper hKupperEqv u v

Lower-member projection of Corollary 34.2.2: every closed saddle-function has a unique lower closed representative in its equivalence class, and that representative is the least member of the class in the pointwise order.

theorem closed_saddle_equivalenceClass_has_unique_lowerClosed_least_member {K : SaddleFunction m n} (hK : IsClosedSaddleFunction K) (hStrongClosures : Section34Text34_1_9StrongClosureQualification m n) : (∀ L : SaddleFunction m n, IsClosedSaddleFunction L → HasNoBotValuesBifunction L) → ∃! Klower : SaddleFunction m n, saddleEquivalent Klower K ∧ IsLowerClosed Klower ∧ ∀ L : SaddleFunction m n, saddleEquivalent L K → Klower ≤ L := by intro hClosedNoBot have hExt := closed_saddle_equivalence_classes_have_unique_extremal_closed_members (m := m) (n := n) hStrongClosures hClosedNoBot exact (hExt.2.2 hK).1

Upper-member projection of Corollary 34.2.2: every closed saddle-function has a unique upper closed representative in its equivalence class, and that representative is the greatest member of the class in the pointwise order.

theorem closed_saddle_equivalenceClass_has_unique_upperClosed_greatest_member {K : SaddleFunction m n} (hK : IsClosedSaddleFunction K) (hStrongClosures : Section34Text34_1_9StrongClosureQualification m n) : (∀ L : SaddleFunction m n, IsClosedSaddleFunction L → HasNoBotValuesBifunction L) → ∃! Kupper : SaddleFunction m n, saddleEquivalent Kupper K ∧ IsUpperClosed Kupper ∧ ∀ L : SaddleFunction m n, saddleEquivalent L K → L ≤ Kupper := by intro hClosedNoBot have hExt := closed_saddle_equivalence_classes_have_unique_extremal_closed_members (m := m) (n := n) hStrongClosures hClosedNoBot exact (hExt.2.2 hK).2

Closedness projection of Corollary 34.2.2: every lower closed saddle-function is closed.

theorem lowerClosed_saddleFunction_isClosed {K : SaddleFunction m n} (hK : IsLowerClosed K) (hStrongClosures : Section34Text34_1_9StrongClosureQualification m n) : (∀ L : SaddleFunction m n, IsClosedSaddleFunction L → HasNoBotValuesBifunction L) → IsClosedSaddleFunction K := by intro hClosedNoBot have hExt := closed_saddle_equivalence_classes_have_unique_extremal_closed_members (m := m) (n := n) hStrongClosures hClosedNoBot exact hExt.1 hK

Closedness projection of Corollary 34.2.2: every upper closed saddle-function is closed.

theorem upperClosed_saddleFunction_isClosed {K : SaddleFunction m n} (hK : IsUpperClosed K) (hStrongClosures : Section34Text34_1_9StrongClosureQualification m n) : (∀ L : SaddleFunction m n, IsClosedSaddleFunction L → HasNoBotValuesBifunction L) → IsClosedSaddleFunction K := by intro hClosedNoBot have hExt := closed_saddle_equivalence_classes_have_unique_extremal_closed_members (m := m) (n := n) hStrongClosures hClosedNoBot exact hExt.2.1 hK
-- Proof sketch: use Theorem 34.2 to represent a closed saddle-function by a closed convex -- bifunction and then apply the improper closed-convex dichotomy from Text 34.2.5 to show that -- an improper closed representative must be constant `⊤` or constant `⊥`; the two constant -- functions are not equivalent because their values, and hence their partial closures, differ -- everywhere.

Corollary 34.2.3: the only improper closed saddle-functions on ℝ ^ sorry × ℝ ^ sorry : Typeℝ^Unknown identifier `m`m × ℝ^Unknown identifier `n`n are the constant functions and , and these two constant saddle-functions are not equivalent.

theorem closed_improper_saddle_function_eq_top_or_bot (hGlobal : Section34Theorem34_2GlobalQualification m n) : (∀ {K : SaddleFunction m n}, IsClosedSaddleFunction K → (¬ IsProperSaddleFunction K ↔ K = ((fun _ _ => (⊤ : EReal)) : SaddleFunction m n) ∨ K = ((fun _ _ => (⊥ : EReal)) : SaddleFunction m n))) ∧ ¬ saddleEquivalent (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := by constructor · intro K hK have hKcc : IsConcaveConvex K := hK.1.1 let Omega : Set (SaddleFunction m n) := {L | saddleEquivalent L K} have hOmega : IsClosedConcaveConvexEquivalenceClass Omega := by refine ⟨K, hKcc, hK, ?_⟩ rfl rcases (isClosedConcaveConvexEquivalenceClass_iff_exists_closedConvexBifunction_generatedClass (Omega := Omega) hGlobal).1 hOmega with ⟨F, hF, hOmegaEq⟩ have hQ : Section34Theorem34_2Qualification F := hGlobal.qualification F hF have hKrefl : saddleEquivalent K K := ⟨hKcc, hKcc, rfl, rfl⟩ have hKmem : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ := by simpa [Omega] using hOmegaEq ▸ hKrefl have hKernelEq : convexBifunctionClosedKernel F = section34ConcaveBifunctionAdjointPairing F := convexBifunctionClosedKernel_eq_section34ConcaveBifunctionAdjointPairing (F := F) hF hQ have hKsand := (mem_equivalenceClassGeneratedByConvexBifunction_iff_sandwich (F := F) hF hQ).1 hKmem have hKeq : K = convexBifunctionClosedKernel F := by funext u xStar apply le_antisymm · exact (hKsand.2.2 u xStar).trans (hKernelEq ▸ le_rfl) · exact hKsand.2.1 u xStar have hKdom : saddleEffectiveDomain K = convexBifunctionDomain F ×ˢ convexBifunctionKernelAdjointDomain F := saddleEffectiveDomain_eq_domain_prod_of_mem_generatedClass (F := F) hF hKmem hK hQ constructor · intro hNotProper have hProdEmpty : convexBifunctionDomain F ×ˢ convexBifunctionKernelAdjointDomain F = (∅ : Set ((Fin m → ℝ) × (Fin n → ℝ))) := by by_contra hNe apply hNotProper rw [IsProperSaddleFunction, hKdom] exact hNe by_cases hDom1Empty : convexBifunctionDomain F = (∅ : Set (Fin m → ℝ)) · right funext u xStar have hu : u ∉ convexBifunctionParameterDomain F := by intro huParam rcases huParam with ⟨x, hx⟩ have huDom : u ∈ convexBifunctionDomain F := by intro xStar have hPairNeBot : convexBifunctionPairing F u xStar ≠ (⊥ : EReal) := by simpa [convexBifunctionPairing, bifunctionPairingNotation, convexConjugate] using helperForTheorem33_1_convexConjugate_ne_bot_of_point (f := F u) (x₀ := x) hx xStar exact bot_lt_iff_ne_bot.mpr hPairNeBot have : u ∈ (∅ : Set (Fin m → ℝ)) := by Try `simp at huDom` instead of `simpa using huDom` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hDom1Empty] using huDom Try `simp at this` instead of `simpa using this` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa using this have hCollapse := helperForLemma33_0_37_primalCollapse_of_off_firstConvexBifunctionDomain (F := F) hu calc K u xStar = convexBifunctionClosedKernel F u xStar := by rw [hKeq] _ = convexBifunctionPairing F u xStar := rfl _ = (⊥ : EReal) := hCollapse.2 xStar · left have hDom1Nonempty : (convexBifunctionDomain F).Nonempty := Set.nonempty_iff_ne_empty.mpr hDom1Empty have hDom2Empty : convexBifunctionKernelAdjointDomain F = (∅ : Set (Fin n → ℝ)) := by by_contra hDom2Ne rcases hDom1Nonempty with ⟨u, hu⟩ rcases Set.nonempty_iff_ne_empty.mpr hDom2Ne with ⟨xStar, hxStar⟩ have hPairMem : (u, xStar) ∈ convexBifunctionDomain F ×ˢ convexBifunctionKernelAdjointDomain F := by exact Set.mem_prod.mpr ⟨hu, hxStar⟩ have : (u, xStar) ∈ (∅ : Set ((Fin m → ℝ) × (Fin n → ℝ))) := by Try `simp at hPairMem` instead of `simpa using hPairMem` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hProdEmpty] using hPairMem Try `simp at this` instead of `simpa using this` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa using this funext u xStar have hAllBot : ∀ uStar : Fin m → ℝ, section34ConcaveBifunctionAdjoint F xStar uStar = (⊥ : EReal) := by intro uStar by_contra hNeBot have hxStarDom : xStar ∈ convexBifunctionKernelAdjointDomain F := by rw [convexBifunctionKernelAdjointDomain] intro u' have hxu : xStar ∈ effectiveDomain (Set.univ : Set (Fin n → ℝ)) (fun x' => concaveBifunctionPairing (section34ConcaveBifunctionAdjoint F) x' u') := by rw [_root_.helperForCorollary33_2_1_concavePairingSection_effectiveDomain_eq (m := n) (n := m) (F := section34ConcaveBifunctionAdjoint F) u'] exact ⟨uStar, hNeBot⟩ have hPairFinite : concaveBifunctionPairing (section34ConcaveBifunctionAdjoint F) xStar u' < (⊤ : EReal) := by simpa [effectiveDomain_eq] using hxu have hPoint : section34ConcaveBifunctionAdjointPairing F u' xStar < (⊤ : EReal) := by simpa [section34ConcaveBifunctionAdjointPairing, concaveBifunctionPairing] using hPairFinite have hKernelPoint : convexBifunctionClosedKernel F u' xStar = section34ConcaveBifunctionAdjointPairing F u' xStar := congrArg (fun G : SaddleFunction m n => G u' xStar) hKernelEq rw [hKernelPoint] exact hPoint have : xStar ∈ (∅ : Set (Fin n → ℝ)) := by Try `simp at hxStarDom` instead of `simpa using hxStarDom` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hDom2Empty] using hxStarDom Try `simp at this` instead of `simpa using this` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa using this have hPairTop : section34ConcaveBifunctionAdjointPairing F u xStar = (⊤ : EReal) := by rw [section34ConcaveBifunctionAdjointPairing, concaveBifunctionPairing, bifunctionPairingNotation, conjugatePairingNotation] simp [hAllBot] calc K u xStar = convexBifunctionClosedKernel F u xStar := by rw [hKeq] _ = section34ConcaveBifunctionAdjointPairing F u xStar := by rw [hKernelEq] _ = (⊤ : EReal) := hPairTop · rintro (rfl | rfl) · intro hProper have hEmpty : saddleEffectiveDomain (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) = (∅ : Set ((Fin m → ℝ) × (Fin n → ℝ))) := by ext p simp [saddleEffectiveDomain, effectiveDomain₁, effectiveDomain₂] exact hProper hEmpty · intro hProper have hEmpty : saddleEffectiveDomain (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) = (∅ : Set ((Fin m → ℝ) × (Fin n → ℝ))) := by ext p simp [saddleEffectiveDomain, effectiveDomain₁, effectiveDomain₂] exact hProper hEmpty · intro hEq have hClosure : partialClosure₁ (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) = partialClosure₁ (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := hEq.2.2.1 have hTop : partialClosure₁ (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) = (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) := by funext u v apply le_antisymm · exact le_top · refine le_iInf ?_ intro ε refine le_iSup_of_le ⟨u, by simpa using ε.2⟩ ?_ rfl have hBot : partialClosure₁ (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) = (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := by funext u v apply le_antisymm · have hε : (0 : ℝ) < 1 := by norm_num calc concaveClosureInFirst (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) u v ≤ ⨆ (w : {w : Fin m → ℝ // ‖w - u‖ < (1 : ℝ)}), (⊥ : EReal) := by exact iInf_le (fun ε : {ε : ℝ // 0 < ε} => ⨆ w : {w : Fin m → ℝ // ‖w - u‖ < ε.1}, (⊥ : EReal)) ⟨1, hε⟩ _ = (⊥ : EReal) := by simp · refine le_iInf ?_ intro ε refine le_iSup_of_le ⟨u, by simpa using ε.2⟩ ?_ rfl have hPointwise : (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) = (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := by calc (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) = partialClosure₁ (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) := by exact hTop.symm _ = partialClosure₁ (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := hClosure _ = (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := hBot have hAtOrigin : (⊤ : EReal) = (⊥ : EReal) := by exact congrArg (fun K : SaddleFunction m n => K 0 0) hPointwise exact top_ne_bot hAtOrigin

Properness projection of Corollary 34.2.3: a closed saddle-function is improper exactly when it is the constant ⊤ : ?m.1⊤ or the constant ⊥ : ?m.1⊥ saddle-function.

theorem closed_saddleFunction_not_proper_iff_eq_top_or_bot {K : SaddleFunction m n} (hK : IsClosedSaddleFunction K) (hGlobal : Section34Theorem34_2GlobalQualification m n) : (¬ IsProperSaddleFunction K ↔ K = ((fun _ _ => (⊤ : EReal)) : SaddleFunction m n) ∨ K = ((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := by exact (closed_improper_saddle_function_eq_top_or_bot (m := m) (n := n) hGlobal).1 hK

Corrected convex-side form of Text 34.4.2: if Unknown identifier `F`F is an image-closed convex bifunction from ℝ ^ sorry : Typeℝ^Unknown identifier `m`m to ℝ ^ sorry : Typeℝ^Unknown identifier `n`n, then the saddle-function is simple. In the current formalization this is the robust statement supported by the closed-kernel correspondence and the closed proper/improper dichotomy.

theorem convex_or_concave_bifunction_pairing_isSimple (hGlobal : Section34Theorem34_2GlobalQualification m n) : ∀ F : (Fin m → ℝ) → (Fin n → ℝ) → EReal, IsImageClosedConvexBifunction F → IsSimpleSaddleFunction (convexBifunctionPairing F) := by intro F hF have hPairCC : IsConcaveConvex (convexBifunctionPairing F) := by simpa [IsConcaveConvex] using ((closedSaddleFunctions_imageClosedBifunctions_correspondence (m := m) (n := n)).1 F hF).1 have hPairMem : convexBifunctionPairing F ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩ := by change saddleEquivalent (convexBifunctionPairing F) (convexBifunctionPairing F) exact ⟨hPairCC, hPairCC, rfl, rfl⟩ have hPairClosed : IsClosedSaddleFunction (convexBifunctionPairing F) := by exact isClosedSaddleFunction_of_mem_generatedClass (F := F) hF hPairMem (hGlobal.qualification F hF) by_cases hProper : IsProperSaddleFunction (convexBifunctionPairing F) · exact Or.inl (closed_proper_saddleFunction_isSimple _ hPairClosed hProper hGlobal) · rcases (((closed_improper_saddle_function_eq_top_or_bot (m := m) (n := n) hGlobal).1 hPairClosed).1 hProper) with hTop | hBot · rw [hTop] exact helperForText_34_4_2_constTop_isSimpleSaddleFunction · rw [hBot] exact helperForText_34_4_2_constBot_isSimpleSaddleFunction

Separation projection of Corollary 34.2.3: the constant ⊤ : ?m.1⊤ and ⊥ : ?m.1⊥ saddle-functions are not saddle-equivalent.

theorem top_saddleFunction_not_saddleEquivalent_bot : ¬ saddleEquivalent (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := by intro hEq have hClosure : partialClosure₁ (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) = partialClosure₁ (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := hEq.2.2.1 have hTop : partialClosure₁ (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) = (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) := by funext u v apply le_antisymm · exact le_top · refine le_iInf ?_ intro ε refine le_iSup_of_le ⟨u, by simpa using ε.2⟩ ?_ rfl have hBot : partialClosure₁ (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) = (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := by funext u v apply le_antisymm · have hε : (0 : ℝ) < 1 := by norm_num calc concaveClosureInFirst (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) u v ≤ ⨆ (w : {w : Fin m → ℝ // ‖w - u‖ < (1 : ℝ)}), (⊥ : EReal) := iInf_le (fun ε : {ε : ℝ // 0 < ε} => ⨆ (w : {w : Fin m → ℝ // ‖w - u‖ < ε.1}), (⊥ : EReal)) ⟨1, hε⟩ _ = (⊥ : EReal) := by refine le_antisymm ?_ bot_le refine iSup_le ?_ intro w exact le_rfl · exact bot_le have hConst : (((fun _ _ => (⊤ : EReal)) : SaddleFunction m n)) = (((fun _ _ => (⊥ : EReal)) : SaddleFunction m n)) := by rw [← hTop, hClosure, hBot] have hPoint := congrFun (congrFun hConst (0 : Fin m → ℝ)) (0 : Fin n → ℝ) simp at hPoint
end SaddleAmbientend Section34end Chap07