noncomputable def classicalDecidablePredPart3 {α : Type u_1} (p : α → Prop) : DecidablePred p

Predicates on coordinate spaces in this section are treated classically when needed in piecewise definitions.

theorem helperForText_34_1_4_openBall_reverseMinimax_of_localConcaveConvexOn_of_saddlePointOn {m n : ℕ} (K : SaddleFunction m n) (u : Fin m → ℝ) (xStar : Fin n → ℝ) (ε δ : { δ : ℝ // 0 < δ }) (hLocal : IsConcaveConvexOn {w : Fin m → ℝ | ‖w - u‖ < ↑ε} {z : Fin n → ℝ | ‖z - xStar‖ < ↑δ} K) (w0 : Fin m → ℝ) (hw0 : ‖w0 - u‖ < ↑ε) (z0 : Fin n → ℝ) (hz0 : ‖z0 - xStar‖ < ↑δ) (hS : IsSaddlePointOn {z : Fin n → ℝ | ‖z - xStar‖ < ↑δ} {w : Fin m → ℝ | ‖w - u‖ < ↑ε} (fun (z : Fin n → ℝ) (w : Fin m → ℝ) => K w z) z0 w0) : ⨅ (z : { z : Fin n → ℝ // ‖z - xStar‖ < ↑δ }), ⨆ (w : { w : Fin m → ℝ // ‖w - u‖ < ↑ε }), K ↑w ↑z ≤ ⨆ (w : { w : Fin m → ℝ // ‖w - u‖ < ↑ε }), ⨅ (z : { z : Fin n → ℝ // ‖z - xStar‖ < ↑δ }), K ↑w ↑z

Helper for Text 34.1.4: reverse-minimax inequality on a pair of open balls, derived from local concave-convexity on those balls.

This lemma is the true upstream minimax/duality input required by the current proof route. Once it is available, helperForText_34_1_4_reverseMinimax_closedBallRadiusEnvelope follows by deterministic rewriting to the closed-ball-radius envelope form.

noncomputable def helperForText_34_1_4_coordKernel : SaddleFunction 1 1

Helper for Text 34.1.4: a one-dimensional coordinate kernel used to exhibit that Jensen-style concave-convexity on open balls does not force existence of a saddle point.

theorem helperForText_34_1_4_coordKernel_concaveConvexOn_openBalls (u xStar : Fin 1 → ℝ) (ε δ : { δ : ℝ // 0 < δ }) : IsConcaveConvexOn {w : Fin 1 → ℝ | ‖w - u‖ < ↑ε} {z : Fin 1 → ℝ | ‖z - xStar‖ < ↑δ} helperForText_34_1_4_coordKernel

Helper for Text 34.1.4: the coordinate kernel is concave-convex on every pair of open balls.

The first-variable Jensen inequality holds by equality for the linear map w ↦ w 0, while the second-variable inequality holds because the kernel is constant in the second variable.

theorem helperForText_34_1_4_coordKernel_isConcaveConvex : IsConcaveConvex helperForText_34_1_4_coordKernel

Helper for Text 34.1.4: the one-dimensional coordinate kernel is globally concave-convex.

theorem helperForText_34_1_4_coordKernel_firstClosure_at_origin (z : Fin 1 → ℝ) : partialClosure₁ helperForText_34_1_4_coordKernel 0 z = 0

Helper for Text 34.1.4: the first-variable closure of the coordinate kernel vanishes at the origin of the first variable.

theorem helperForText_34_1_4_coordKernel_lowerClosure_at_origin (z : Fin 1 → ℝ) : lowerClosureConcaveConvex helperForText_34_1_4_coordKernel helperForText_34_1_4_coordKernel_isConcaveConvex 0 z = 0

Helper for Text 34.1.4: the mixed lower closure of the coordinate kernel also vanishes at the origin of the first variable.

noncomputable def helperForText_34_1_4_secondCoordKernel : SaddleFunction 1 1

Helper for Text 34.1.4: a one-dimensional coordinate kernel in the second variable, used to test the right closed-ball bridge.

theorem helperForText_34_1_4_secondCoordKernel_isConcaveConvex : IsConcaveConvex helperForText_34_1_4_secondCoordKernel

Helper for Text 34.1.4: the second-coordinate kernel is globally concave-convex.

theorem helperForText_34_1_4_secondCoordKernel_firstClosure (u z : Fin 1 → ℝ) : partialClosure₁ helperForText_34_1_4_secondCoordKernel u z = ↑(z 0)

Helper for Text 34.1.4: the first closure of the second-coordinate kernel is trivial because the kernel is constant in the first variable.

theorem helperForText_34_1_4_secondCoordKernel_secondClosure_at_origin (u : Fin 1 → ℝ) : partialClosure₂ helperForText_34_1_4_secondCoordKernel u 0 = 0

Helper for Text 34.1.4: the second closure of the second-coordinate kernel vanishes at the origin of the second variable.

theorem helperForText_34_1_4_secondCoordKernel_lowerClosure_at_origin (u : Fin 1 → ℝ) : lowerClosureConcaveConvex helperForText_34_1_4_secondCoordKernel helperForText_34_1_4_secondCoordKernel_isConcaveConvex u 0 = 0

Helper for Text 34.1.4: the mixed lower closure of the second-coordinate kernel also vanishes at the origin of the second variable.

theorem helperForText_34_1_4_exists_mem_openBall_gt_coord_fin1 (u : Fin 1 → ℝ) (ε : ℝ) (w0 : Fin 1 → ℝ) (hw0 : ‖w0 - u‖ < ε) : ∃ (w : Fin 1 → ℝ), ‖w - u‖ < ε ∧ w0 0 < w 0

Helper for Text 34.1.4: any point in a nontrivial open ball in Fin 1 → ℝ can be moved to a nearby point in the same ball with strictly larger 0-th coordinate.

theorem helperForText_34_1_4_coordKernel_no_saddlePointOn_openBalls (u xStar : Fin 1 → ℝ) (ε δ : { δ : ℝ // 0 < δ }) : ¬∃ (w0 : Fin 1 → ℝ), ‖w0 - u‖ < ↑ε ∧ ∃ (z0 : Fin 1 → ℝ), ‖z0 - xStar‖ < ↑δ ∧ IsSaddlePointOn {z : Fin 1 → ℝ | ‖z - xStar‖ < ↑δ} {w : Fin 1 → ℝ | ‖w - u‖ < ↑ε} (fun (z w : Fin 1 → ℝ) => helperForText_34_1_4_coordKernel w z) z0 w0

Helper for Text 34.1.4: the coordinate kernel admits no saddle point on open balls.

This gives a concrete counterexample to the naive implication IsConcaveConvexOn (openBall u ε) (openBall xStar δ) K → ∃ saddle point, so the corresponding step in the proof pipeline must be replaced by a genuine minimax/duality theorem with additional hypotheses (compactness/attainment, semicontinuity, etc.).

theorem helperForText_34_1_4_counterexample_openBall_exists_saddlePointOn_false (u xStar : Fin 1 → ℝ) (ε δ : { δ : ℝ // 0 < δ }) : IsConcaveConvexOn {w : Fin 1 → ℝ | ‖w - u‖ < ↑ε} {z : Fin 1 → ℝ | ‖z - xStar‖ < ↑δ} helperForText_34_1_4_coordKernel ∧ ¬∃ (w0 : Fin 1 → ℝ), ‖w0 - u‖ < ↑ε ∧ ∃ (z0 : Fin 1 → ℝ), ‖z0 - xStar‖ < ↑δ ∧ IsSaddlePointOn {z : Fin 1 → ℝ | ‖z - xStar‖ < ↑δ} {w : Fin 1 → ℝ | ‖w - u‖ < ↑ε} (fun (z w : Fin 1 → ℝ) => helperForText_34_1_4_coordKernel w z) z0 w0

Helper for Text 34.1.4: counterexample showing that the open-ball saddle-point existence step cannot be proved from IsConcaveConvexOn alone.

theorem helperForText_34_1_4_no_uniform_openBall_saddlePointExistence_in_dim1 : ¬∀ (K : SaddleFunction 1 1) (u xStar : Fin 1 → ℝ) (ε δ : { δ : ℝ // 0 < δ }), IsConcaveConvexOn {w : Fin 1 → ℝ | ‖w - u‖ < ↑ε} {z : Fin 1 → ℝ | ‖z - xStar‖ < ↑δ} K → ∃ (w0 : Fin 1 → ℝ), ‖w0 - u‖ < ↑ε ∧ ∃ (z0 : Fin 1 → ℝ), ‖z0 - xStar‖ < ↑δ ∧ IsSaddlePointOn {z : Fin 1 → ℝ | ‖z - xStar‖ < ↑δ} {w : Fin 1 → ℝ | ‖w - u‖ < ↑ε} (fun (z w : Fin 1 → ℝ) => K w z) z0 w0

Helper for Text 34.1.4: the abandoned open-ball route is already false in dimension 1.

Concretely, there is no uniform theorem saying that local concave-convexity on open balls forces existence of a saddle point on those balls.

theorem helperForText_34_1_4_coordKernel_reverseMinimax_openBalls (u xStar : Fin 1 → ℝ) (ε δ : { δ : ℝ // 0 < δ }) : ⨅ (z : { z : Fin 1 → ℝ // ‖z - xStar‖ < ↑δ }), ⨆ (w : { w : Fin 1 → ℝ // ‖w - u‖ < ↑ε }), helperForText_34_1_4_coordKernel ↑w ↑z ≤ ⨆ (w : { w : Fin 1 → ℝ // ‖w - u‖ < ↑ε }), ⨅ (z : { z : Fin 1 → ℝ // ‖z - xStar‖ < ↑δ }), helperForText_34_1_4_coordKernel ↑w ↑z

Helper for Text 34.1.4: the coordinate kernel satisfies the reverse-minimax inequality on open balls even though it has no saddle point there.

This emphasizes that failure of saddle-point attainment does not by itself refute reverse minimax; what is missing for the general theorem is a genuine minimax/duality input, not the simple saddle-point existence step.

theorem helperForText_34_1_4_closedConvexBifunction_of_graphFunctionClosed {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hRock : IsRockafellarConvexBifunction F) (hNoBot : HasNoBotValuesBifunction F) (hGraphClosed : IsFunctionConvexClosed (graphFunctionOfBifunction F)) : ClosedConvexBifunction F

Helper for Text 34.1.4: graph-function closedness upgrades a Rockafellar convex bifunction to a closed convex bifunction.

structure Section34CanonicalClosureRealizationQualification (m n : ℕ) : Prop

Dimension-wide realization qualification for the converse direction of Corollary 33.3.1. The forward closure theorem does not construct a bifunction witness from an arbitrary closure pair, so the two canonical realization clauses are recorded explicitly.

• upper (K : SaddleFunction m n) (h : IsConcaveConvex K) : HasNoBotValuesBifunction K → HasNoTopOrBotValuesBifunction (lowerClosureConcaveConvex K h) → ∃! F : (Fin m → ℝ) → (Fin n → ℝ) → EReal, ClosedConvexBifunction F ∧ HasNoBotValuesBifunction F ∧ (∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), lowerClosureConcaveConvex K h u xStar = convexBifunctionPairing F u xStar) ∧ ∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), partialClosure₁ (lowerClosureConcaveConvex K h) u xStar = convexBifunctionCanonicalAdjointPairing F xStar u
• lower (K : SaddleFunction m n) (h : IsConcaveConvex K) : HasNoBotValuesBifunction K → HasNoTopOrBotValuesBifunction (partialClosure₂ (upperClosureConcaveConvex K h)) → ∃! F : (Fin m → ℝ) → (Fin n → ℝ) → EReal, ClosedConvexBifunction F ∧ HasNoBotValuesBifunction F ∧ (∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), partialClosure₂ (upperClosureConcaveConvex K h) u xStar = convexBifunctionPairing F u xStar) ∧ ∀ (u : Fin m → ℝ) (xStar : Fin n → ℝ), upperClosureConcaveConvex K h u xStar = convexBifunctionCanonicalAdjointPairing F xStar u

theorem helperForText_34_1_4_closedConvexWitness_exists_for_canonicalUpperPartner {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hKNoBot : HasNoBotValuesBifunction K) (hLowerNoTopBot : HasNoTopOrBotValuesBifunction (lowerClosureConcaveConvex K h)) (hRealization : Section34CanonicalClosureRealizationQualification m n) : ∃ (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal), ClosedConvexBifunction F ∧ HasNoBotValuesBifunction F ∧ lowerClosureConcaveConvex K h = convexBifunctionPairing F ∧ partialClosure₁ (lowerClosureConcaveConvex K h) = helperForText_34_0_1_convexAdjointPairingKernel F

Helper for Text 34.1.4: the qualified converse of Corollary 33.3.1 gives a closed convex witness for the canonical pair (underline(K), cl₁ underline(K)) once the primal side is assumed to avoid both ⊥ and ⊤.

theorem helperForText_34_1_4_closedConvexWitness_exists_for_canonicalLowerPartner {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (hKNoBot : HasNoBotValuesBifunction K) (hCanonicalLowerNoTopBot : HasNoTopOrBotValuesBifunction (partialClosure₂ (upperClosureConcaveConvex K h))) (hRealization : Section34CanonicalClosureRealizationQualification m n) : ∃ (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal), ClosedConvexBifunction F ∧ partialClosure₂ (upperClosureConcaveConvex K h) = convexBifunctionPairing F ∧ upperClosureConcaveConvex K h = helperForText_34_0_1_convexAdjointPairingKernel F

Helper for Text 34.1.4: the corrected Corollary 33.3.1 likewise gives a closed convex witness for the canonical pair (cl₂ overline(K), overline(K)) once the lower partner is assumed to avoid both ⊥ and ⊤.

theorem helperForText_34_1_4_graphFunction_isFunctionConvexClosed_of_closedConvexBifunction {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConvexBifunction F) : IsFunctionConvexClosed (graphFunctionOfBifunction F)

Helper for Text 34.1.4: a closed convex bifunction already has graph function fixed by the raw convex-closure operator.

theorem helperForText_34_1_4_constBot_isERealConcaveOn {n : ℕ} : IsERealConcaveOn Set.univ fun (x : Fin n → ℝ) => ⊥

Helper for Text 34.1.4: the constant ⊥ function is concave in the Jensen sense on ℝ^n.

theorem helperForText_34_1_4_zeroDimensional_constBot_lowerClosure_eq_bot : let K := fun (x x_1 : Fin 0 → ℝ) => ⊥; have h := ⋯; lowerClosureConcaveConvex K h 0 0 = ⊥

Route correction for Text 34.1.4: the zero-dimensional constant-⊥ kernel is concave-convex, and its mixed lower closure still equals ⊥ at the unique point.

theorem helperForText_34_1_4_zeroDimensional_constBot_refutes_lowerClosure_hasNoBot_statement : let K := fun (x x_1 : Fin 0 → ℝ) => ⊥; have h := ⋯; ¬HasNoBotValuesBifunction (lowerClosureConcaveConvex K h)

Route correction for Text 34.1.4: the statement HasNoBotValuesBifunction (lowerClosureConcaveConvex K h) is false in general. The zero-dimensional constant-⊥ kernel already refutes it.

theorem helperForText_34_1_4_lowerClosure_hasNoBot_of_closedConvexLowerRepresentation {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hRock : IsRockafellarConvexBifunction F) (hNoBot : HasNoBotValuesBifunction F) (hClosed : ClosedConvexBifunction F) (hLowerRep : lowerClosureConcaveConvex K h = convexBifunctionPairing F) (hFiniteSections : ∀ (u : Fin m → ℝ), ∃ (x : Fin n → ℝ), F u x < ⊤) : HasNoBotValuesBifunction (lowerClosureConcaveConvex K h)

Helper for Text 34.1.4: although underline(K) need not avoid ⊥ in general, any actual closed-convex witness for underline(K) forces the represented mixed lower closure to have no ⊥ values.

theorem helperForText_34_1_4_lowerClosure_hasNoBot {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hRock : IsRockafellarConvexBifunction F) (hNoBot : HasNoBotValuesBifunction F) (hClosed : ClosedConvexBifunction F) (hLowerRep : lowerClosureConcaveConvex K h = convexBifunctionPairing F) (hFiniteSections : ∀ (u : Fin m → ℝ), ∃ (x : Fin n → ℝ), F u x < ⊤) : HasNoBotValuesBifunction (lowerClosureConcaveConvex K h)

Helper for Text 34.1.4: the usable no-⊥ statement for underline(K) is the witness-local one. The naive global version is false by the constant-⊥ counterexample above, so the remaining development only uses this corrected interface.

theorem helperForText_34_1_4_witness_sections_notTop_of_lowerRepresentation {m n : ℕ} {K : SaddleFunction m n} {h : IsConcaveConvex K} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hLowerNoBot : HasNoBotValuesBifunction (lowerClosureConcaveConvex K h)) (hLowerRep : lowerClosureConcaveConvex K h = convexBifunctionPairing F) (u : Fin m → ℝ) : ∃ (x : Fin n → ℝ), F u x ≠ ⊤

Helper for Text 34.1.4: if a convex bifunction represents underline(K), then none of its parameter sections can be identically ⊤; otherwise the pairing would force underline(K) to take the value ⊥.

theorem helperForText_34_1_4_strictParameterDomain_eq_univ_of_lowerRepresentation {m n : ℕ} {K : SaddleFunction m n} {h : IsConcaveConvex K} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hLowerNoBot : HasNoBotValuesBifunction (lowerClosureConcaveConvex K h)) (hLowerRep : lowerClosureConcaveConvex K h = convexBifunctionPairing F) : {u' : Fin m → ℝ | ∃ (x : Fin n → ℝ), F u' x < ⊤} = Set.univ

Helper for Text 34.1.4: any convex bifunction representing underline(K) already has full strict parameter domain, because underline(K) never takes the value ⊥.

theorem helperForText_34_1_4_parameterDomain_eq_univ_of_lowerRepresentation {m n : ℕ} {K : SaddleFunction m n} {h : IsConcaveConvex K} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hLowerNoBot : HasNoBotValuesBifunction (lowerClosureConcaveConvex K h)) (hLowerRep : lowerClosureConcaveConvex K h = convexBifunctionPairing F) : convexBifunctionParameterDomain F = Set.univ

Helper for Text 34.1.4: any convex bifunction representing underline(K) has full Section 33 parameter domain, not just the strict < ⊤ variant.