theorem helperForText_34_1_6_weightedSum_gt_bot {x y : EReal} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (_hab : a + b = 1) (hx : ⊥ < x) (hy : ⊥ < y) : ⊥ < ↑a * x + ↑b * y

Helper for Text 34.1.6: a nonnegative weighted sum of two EReal values strictly above ⊥ is still strictly above ⊥.

theorem helperForText_34_1_6_weightedSum_lt_top {x y : EReal} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (_hab : a + b = 1) (hx : x < ⊤) (hy : y < ⊤) : ↑a * x + ↑b * y < ⊤

Helper for Text 34.1.6: a nonnegative weighted sum of two EReal values strictly below ⊤ is still strictly below ⊤.

theorem helperForText_34_1_6_concaveSlice_effectiveDomain_convex {k : ℕ} {f : (Fin k → ℝ) → EReal} (hConc : IsERealConcaveOn Set.univ f) : Convex ℝ (concaveFunctionEffectiveDomain f)

Helper for Text 34.1.6: the effective domain of a globally concave EReal slice is convex.

theorem helperForText_34_1_6_effectiveDomain1_eq_iInter_concaveSlices {m n : ℕ} (K : SaddleFunction m n) : effectiveDomain₁ K = ⋂ (v : Fin n → ℝ), concaveFunctionEffectiveDomain fun (u : Fin m → ℝ) => K u v

Helper for Text 34.1.6: the first effective domain is the intersection of the concave slice domains dom (u ↦ K u v).

theorem helperForText_34_1_6_effectiveDomain2_eq_iInter_convexSlices {m n : ℕ} (K : SaddleFunction m n) : effectiveDomain₂ K = ⋂ (u : Fin m → ℝ), effectiveDomain Set.univ (K u)

Helper for Text 34.1.6: the second effective domain is the intersection of the convex slice domains dom (v ↦ K u v).

theorem helperForText_34_1_6_convex_concaveSlice_for_fixedSecond {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (v : Fin n → ℝ) : Convex ℝ (concaveFunctionEffectiveDomain fun (u : Fin m → ℝ) => K u v)

Helper for Text 34.1.6: fixing the second variable yields a convex first-variable slice domain.

theorem helperForText_34_1_6_convex_effectiveDomainSlice_for_fixedFirst {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (u : Fin m → ℝ) : Convex ℝ (effectiveDomain Set.univ (K u))

Helper for Text 34.1.6: fixing the first variable yields a convex second-variable slice domain.

theorem helperForText_34_1_6_domainPoint_isFinite {m n : ℕ} (K : SaddleFunction m n) {u : Fin m → ℝ} {v : Fin n → ℝ} (hu : u ∈ effectiveDomain₁ K) (hv : v ∈ effectiveDomain₂ K) : K u v ≠ ⊤ ∧ K u v ≠ ⊥

Helper for Text 34.1.6: every point of dom₁ K × dom₂ K is a finite-valued point of K.

theorem helperForText_34_1_6_mem_saddleEffectiveDomain_iff {m n : ℕ} (K : SaddleFunction m n) {p : (Fin m → ℝ) × (Fin n → ℝ)} : p ∈ saddleEffectiveDomain K ↔ p.1 ∈ effectiveDomain₁ K ∧ p.2 ∈ effectiveDomain₂ K

Helper for Text 34.1.6: membership in the saddle effective domain is exactly coordinatewise membership in the two effective domains.

theorem helperForText_34_1_6_mem_finitenessDomain_of_mem_saddleEffectiveDomain {m n : ℕ} (K : SaddleFunction m n) {p : (Fin m → ℝ) × (Fin n → ℝ)} (hp : p ∈ saddleEffectiveDomain K) : p ∈ finitenessDomain K

Helper for Text 34.1.6: every point of dom K lies in the finiteness domain of K.

theorem helperForText_34_1_6_convex_saddleEffectiveDomain {m n : ℕ} (K : SaddleFunction m n) (hDom1 : Convex ℝ (effectiveDomain₁ K)) (hDom2 : Convex ℝ (effectiveDomain₂ K)) : Convex ℝ (saddleEffectiveDomain K)

Helper for Text 34.1.6: the saddle effective domain is convex once the two coordinate effective domains are convex.

theorem helperForText_34_1_6_concaveSlice_jensen {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (v : Fin n → ℝ) {u₁ u₂ : Fin m → ℝ} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : ↑a * K u₁ v + ↑b * K u₂ v ≤ K (a • u₁ + b • u₂) v

Helper for Text 34.1.6: the concavity side of a saddle-function gives Jensen's inequality on each fixed-second-variable slice.

theorem helperForText_34_1_6_convexSlice_jensen {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) (u : Fin m → ℝ) {v₁ v₂ : Fin n → ℝ} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : K u (a • v₁ + b • v₂) ≤ ↑a * K u v₁ + ↑b * K u v₂

Helper for Text 34.1.6: the convexity side of a saddle-function gives Jensen's inequality on each fixed-first-variable slice.

theorem helperForText_34_1_6_mem_effectiveDomain1_of_convexCombination {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) {u₁ u₂ : Fin m → ℝ} (hu₁ : u₁ ∈ effectiveDomain₁ K) (hu₂ : u₂ ∈ effectiveDomain₁ K) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • u₁ + b • u₂ ∈ effectiveDomain₁ K

Helper for Text 34.1.6: convex combinations of points in dom₁ K stay in dom₁ K.

theorem helperForText_34_1_6_mem_effectiveDomain2_of_convexCombination {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) {v₁ v₂ : Fin n → ℝ} (hv₁ : v₁ ∈ effectiveDomain₂ K) (hv₂ : v₂ ∈ effectiveDomain₂ K) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • v₁ + b • v₂ ∈ effectiveDomain₂ K

Helper for Text 34.1.6: convex combinations of points in dom₂ K stay in dom₂ K.

theorem helperForText_34_1_6_mem_saddleEffectiveDomain_of_convexCombination {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) {p₁ p₂ : (Fin m → ℝ) × (Fin n → ℝ)} (hp₁ : p₁ ∈ saddleEffectiveDomain K) (hp₂ : p₂ ∈ saddleEffectiveDomain K) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • p₁ + b • p₂ ∈ saddleEffectiveDomain K

Helper for Text 34.1.6: convex combinations of points in dom K stay in dom K.

theorem helperForText_34_1_6_convex_effectiveDomain1 {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) : Convex ℝ (effectiveDomain₁ K)

Helper for Text 34.1.6: the first effective domain is convex for a concave-convex saddle function.

theorem helperForText_34_1_6_convex_effectiveDomain2 {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) : Convex ℝ (effectiveDomain₂ K)

Helper for Text 34.1.6: the second effective domain is convex for a concave-convex saddle function.

theorem section34_text_34_1_6 {m n : ℕ} (K : SaddleFunction m n) (h : IsConcaveConvex K) : Convex ℝ (effectiveDomain₁ K) ∧ Convex ℝ (effectiveDomain₂ K) ∧ Convex ℝ (saddleEffectiveDomain K) ∧ saddleEffectiveDomain K ⊆ finitenessDomain K

Text 34.1.6: if K is concave-convex on ℝ^m × ℝ^n, then dom₁ K is convex in ℝ^m and dom₂ K is convex in ℝ^n; consequently dom K is convex in ℝ^m × ℝ^n, and K is finite at every point of dom K.

theorem helperForText_34_1_7_secondSection_not_concave_at_half : ¬IsERealConcaveOn Set.univ fun (v : Fin 1 → ℝ) => openUnitSquarePowerSaddle (fun (x : Fin 1) => 1 / 2) v

Helper for Text 34.1.7: the v-section of the open-unit-square power upper simple extension at u = 1 / 2 fails concavity on all of ℝ, because two off-domain points have an in-domain midpoint.

theorem helperForText_34_1_7_openUnitSquarePowerSaddle_not_convexConcave : ¬IsConvexConcave openUnitSquarePowerSaddle

Helper for Text 34.1.7: the open-unit-square power upper simple extension is not convex-concave on all of ℝ × ℝ.

theorem helperForText_34_1_7_openUnitSquarePowerSaddle_not_saddle : ¬IsSaddleFunctionOn Set.univ Set.univ openUnitSquarePowerSaddle

Helper for Text 34.1.7: the open-unit-square power upper simple extension is not a global saddle-function, so it cannot satisfy the theorem's upper-extension conclusion.

theorem helperForText_34_1_7_openUnitInterval_convex : Convex ℝ {u : Fin 1 → ℝ | InOpenUnitInterval u}

Helper for Text 34.1.7: the open unit interval subset of Fin 1 → ℝ is convex.

theorem helperForText_34_1_7_openUnitInterval_nonempty : {u : Fin 1 → ℝ | InOpenUnitInterval u}.Nonempty

Helper for Text 34.1.7: the open unit interval subset of Fin 1 → ℝ is nonempty.

theorem helperForText_34_1_7_oneDimensionalPowerKernel_isConcaveConvexOn : IsConcaveConvexOn {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel

Helper for Text 34.1.7: on the open unit square, the real power kernel carries the concave-convex saddle orientation used by the textbook example.

theorem helperForText_34_1_7_upperSimpleExtension_eq_openUnitSquarePowerSaddle : upperSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel = openUnitSquarePowerSaddle

Helper for Text 34.1.7: the upper simple extension of the open-unit-square power kernel is definitionally the openUnitSquarePowerSaddle counterexample.

def helperForText_34_1_7_targetTheoremClaim : Prop

Helper for Text 34.1.7: the exact universal theorem claim, isolated as a single proposition so the open-unit-square counterexample can specialize it.

theorem helperForText_34_1_7_openUnitPowerKernel_satisfiesTargetHypotheses : Convex ℝ {u : Fin 1 → ℝ | InOpenUnitInterval u} ∧ Convex ℝ {v : Fin 1 → ℝ | InOpenUnitInterval v} ∧ {u : Fin 1 → ℝ | InOpenUnitInterval u}.Nonempty ∧ {v : Fin 1 → ℝ | InOpenUnitInterval v}.Nonempty ∧ IsSaddleFunctionOn {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel ∧ ∀ u ∈ {u : Fin 1 → ℝ | InOpenUnitInterval u}, ∀ v ∈ {v : Fin 1 → ℝ | InOpenUnitInterval v}, ⊥ < oneDimensionalPowerKernel u v ∧ oneDimensionalPowerKernel u v < ⊤

Helper for Text 34.1.7: the open-unit-square power example satisfies every hypothesis in the isolated theorem claim.

theorem helperForText_34_1_7_specializedUpperSimpleExtension_not_saddle : ¬IsSaddleFunctionOn Set.univ Set.univ (upperSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel)

Helper for Text 34.1.7: the specialized upper simple extension for the open-unit-square power kernel is already not a global saddle-function.

theorem helperForText_34_1_7_specializedConclusion_false : ¬(IsSaddleFunctionOn Set.univ Set.univ (lowerSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel) ∧ effectiveDomain₁ (lowerSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel) = {u : Fin 1 → ℝ | InOpenUnitInterval u} ∧ effectiveDomain₂ (lowerSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel) = {v : Fin 1 → ℝ | InOpenUnitInterval v} ∧ saddleEffectiveDomain (lowerSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel) = {u : Fin 1 → ℝ | InOpenUnitInterval u} ×ˢ {v : Fin 1 → ℝ | InOpenUnitInterval v} ∧ IsProperSaddleFunction (lowerSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel) ∧ IsSaddleFunctionOn Set.univ Set.univ (upperSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel) ∧ effectiveDomain₁ (upperSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel) = {u : Fin 1 → ℝ | InOpenUnitInterval u} ∧ effectiveDomain₂ (upperSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel) = {v : Fin 1 → ℝ | InOpenUnitInterval v} ∧ saddleEffectiveDomain (upperSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel) = {u : Fin 1 → ℝ | InOpenUnitInterval u} ×ˢ {v : Fin 1 → ℝ | InOpenUnitInterval v} ∧ IsProperSaddleFunction (upperSimpleExtension {u : Fin 1 → ℝ | InOpenUnitInterval u} {v : Fin 1 → ℝ | InOpenUnitInterval v} oneDimensionalPowerKernel))

Helper for Text 34.1.7: the full specialized conclusion is false, because its upper simple extension branch is the already refuted open-unit-square counterexample.