theorem helperForTheorem_35_9_gradientPair_continuousOn_E {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hC_open : IsOpen C) (hD_open : IsOpen D) (hC_conv : Convex ℝ C) (hD_conv : Convex ℝ D) (hK : IsRealConcaveConvexOn C D K) : have E := {p : (Fin m → ℝ) × (Fin n → ℝ) | p ∈ C ×ˢ D ∧ DifferentiableAt ℝ (packedRealSaddleKernel K) (Fin.append p.1 p.2)}; Continuous fun (p : { p : (Fin m → ℝ) × (Fin n → ℝ) // p ∈ E }) => packedRealSaddleKernelGradientPair K (↑p).1 (↑p).2

Helper for Theorem 35.9: the packed gradient pair varies continuously on the differentiability locus because nearby saddle subgradients stay close to the singleton base subgradient.

theorem section35_theorem35_9 {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hC_open : IsOpen C) (hD_open : IsOpen D) (hC_conv : Convex ℝ C) (hD_conv : Convex ℝ D) (hK : IsRealConcaveConvexOn C D K) : have E := {p : (Fin m → ℝ) × (Fin n → ℝ) | p ∈ C ×ˢ D ∧ DifferentiableAt ℝ (packedRealSaddleKernel K) (Fin.append p.1 p.2)}; C ×ˢ D ⊆ closure E ∧ MeasureTheory.volume (C ×ˢ D \ E) = 0 ∧ Continuous fun (p : { p : (Fin m → ℝ) × (Fin n → ℝ) // p ∈ E }) => packedRealSaddleKernelGradientPair K (↑p).1 (↑p).2

Theorem 35.9: let C × D be an open convex set in ℝ^m × ℝ^n, and let K be a concave-convex real-valued function on C × D. If E is the subset of C × D where K is differentiable, then E is dense in C × D, the complement (C × D) \ E has Lebesgue measure zero, and the gradient mapping is continuous on E. The differentiability and gradient are expressed below via the packed map z ↦ K(z₁, z₂) on ℝ^(m+n), which is equivalent to differentiability of K on the product space.

theorem helperForTheorem_35_10_limitGradient_continuousOn_product {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hC_open : IsOpen C) (hD_open : IsOpen D) (hC_conv : Convex ℝ C) (hD_conv : Convex ℝ D) (hK : IsRealConcaveConvexOn C D K) (hK_diff : ∀ u ∈ C, ∀ v ∈ D, DifferentiableAt ℝ (packedRealSaddleKernel K) (Fin.append u v)) : ContinuousOn (fun (p : (Fin m → ℝ) × (Fin n → ℝ)) => packedRealSaddleKernelGradientPair K p.1 p.2) (C ×ˢ D)

Helper for Theorem 35.10: since K is differentiable at every point of C × D, Theorem 35.9 identifies the packed gradient pair as a continuous map on the whole product domain.

theorem helperForTheorem_35_10_moving_gradientPair_tendsto {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {KSeq : ℕ → (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hC_open : IsOpen C) (hD_open : IsOpen D) (hC_conv : Convex ℝ C) (hD_conv : Convex ℝ D) (hK : IsRealConcaveConvexOn C D K) (hK_diff : ∀ u ∈ C, ∀ v ∈ D, DifferentiableAt ℝ (packedRealSaddleKernel K) (Fin.append u v)) (hKSeq : ∀ (i : ℕ), IsRealConcaveConvexOn C D (KSeq i)) (hKSeq_diff : ∀ (i : ℕ), ∀ u ∈ C, ∀ v ∈ D, DifferentiableAt ℝ (packedRealSaddleKernel (KSeq i)) (Fin.append u v)) (hpointwise : ∀ u ∈ C, ∀ v ∈ D, Filter.Tendsto (fun (i : ℕ) => KSeq i u v) Filter.atTop (nhds (K u v))) {u : Fin m → ℝ} {v : Fin n → ℝ} (hu : u ∈ C) (hv : v ∈ D) (uSeq : ℕ → Fin m → ℝ) (vSeq : ℕ → Fin n → ℝ) (huSeq : ∀ (i : ℕ), uSeq i ∈ C) (hvSeq : ∀ (i : ℕ), vSeq i ∈ D) (huSeq_tendsto : Filter.Tendsto uSeq Filter.atTop (nhds u)) (hvSeq_tendsto : Filter.Tendsto vSeq Filter.atTop (nhds v)) : Filter.Tendsto (fun (i : ℕ) => packedRealSaddleKernelGradientPair (KSeq i) (uSeq i) (vSeq i)) Filter.atTop (nhds (packedRealSaddleKernelGradientPair K u v))

Helper for Theorem 35.10: Theorem 35.7 turns moving-point convergence of kernels into convergence of the corresponding packed gradient pairs.

theorem helperForTheorem_35_10_pointwise_gradientPair_tendsto {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {KSeq : ℕ → (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hC_open : IsOpen C) (hD_open : IsOpen D) (hC_conv : Convex ℝ C) (hD_conv : Convex ℝ D) (hK : IsRealConcaveConvexOn C D K) (hK_diff : ∀ u ∈ C, ∀ v ∈ D, DifferentiableAt ℝ (packedRealSaddleKernel K) (Fin.append u v)) (hKSeq : ∀ (i : ℕ), IsRealConcaveConvexOn C D (KSeq i)) (hKSeq_diff : ∀ (i : ℕ), ∀ u ∈ C, ∀ v ∈ D, DifferentiableAt ℝ (packedRealSaddleKernel (KSeq i)) (Fin.append u v)) (hpointwise : ∀ u ∈ C, ∀ v ∈ D, Filter.Tendsto (fun (i : ℕ) => KSeq i u v) Filter.atTop (nhds (K u v))) {u : Fin m → ℝ} {v : Fin n → ℝ} (hu : u ∈ C) (hv : v ∈ D) : Filter.Tendsto (fun (i : ℕ) => packedRealSaddleKernelGradientPair (KSeq i) u v) Filter.atTop (nhds (packedRealSaddleKernelGradientPair K u v))

Helper for Theorem 35.10: the fixed-point convergence statement is the constant-sequence specialization of the moving-point gradient-pair convergence lemma.

theorem section35_theorem35_10 {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {KSeq : ℕ → (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hC_open : IsOpen C) (hD_open : IsOpen D) (hC_conv : Convex ℝ C) (hD_conv : Convex ℝ D) (hK : IsRealConcaveConvexOn C D K) (hK_diff : ∀ u ∈ C, ∀ v ∈ D, DifferentiableAt ℝ (packedRealSaddleKernel K) (Fin.append u v)) (hKSeq : ∀ (i : ℕ), IsRealConcaveConvexOn C D (KSeq i)) (hKSeq_diff : ∀ (i : ℕ), ∀ u ∈ C, ∀ v ∈ D, DifferentiableAt ℝ (packedRealSaddleKernel (KSeq i)) (Fin.append u v)) (hpointwise : ∀ u ∈ C, ∀ v ∈ D, Filter.Tendsto (fun (i : ℕ) => KSeq i u v) Filter.atTop (nhds (K u v))) : (∀ u ∈ C, ∀ v ∈ D, Filter.Tendsto (fun (i : ℕ) => packedRealSaddleKernelGradientPair (KSeq i) u v) Filter.atTop (nhds (packedRealSaddleKernelGradientPair K u v))) ∧ ∀ S ⊆ C ×ˢ D, IsClosed S → Bornology.IsBounded S → TendstoUniformlyOn (fun (i : ℕ) (p : (Fin m → ℝ) × (Fin n → ℝ)) => packedRealSaddleKernelGradientPair (KSeq i) p.1 p.2) (fun (p : (Fin m → ℝ) × (Fin n → ℝ)) => packedRealSaddleKernelGradientPair K p.1 p.2) Filter.atTop S

Theorem 35.10: let C × D be an open convex set in ℝ^m × ℝ^n, let K be a finite differentiable concave-convex function on C × D, and let K₁, K₂, ... be finite differentiable concave-convex functions on C × D converging pointwise to K. Then the split gradient maps ∇Kᵢ(u, v) converge pointwise to ∇K(u, v) for every (u, v) ∈ C × D, and in fact converge uniformly on every closed bounded subset of C × D.

theorem helperForText_35_10_1_denseWitness_existsLimits {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] {C : Set E} {D : Set F} {K : E → F → ℝ} {KSeq : ℕ → E → F → ℝ} (hDense : ∃ (C' : Set E) (D' : Set F), C' ⊆ C ∧ D' ⊆ D ∧ C ⊆ closure C' ∧ D ⊆ closure D' ∧ ∀ u ∈ C', ∀ v ∈ D', Filter.Tendsto (fun (i : ℕ) => KSeq i u v) Filter.atTop (nhds (K u v))) : ∃ (C' : Set E) (D' : Set F), C' ⊆ C ∧ D' ⊆ D ∧ C ⊆ closure C' ∧ D ⊆ closure D' ∧ ∀ u ∈ C', ∀ v ∈ D', ∃ (l : ℝ), Filter.Tendsto (fun (i : ℕ) => KSeq i u v) Filter.atTop (nhds l)

Helper for Text 35.10.1: repackage the dense convergence hypothesis into the existential limit format required by Theorem 35.4.

theorem helperForText_35_10_1_eqOn_product_of_denseEq {m n : ℕ} {C : Set (EuclideanSpace ℝ (Fin m))} {D : Set (EuclideanSpace ℝ (Fin n))} {K L : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n) → ℝ} (hC : IsRelativelyOpenConvex C) (hD : IsRelativelyOpenConvex D) (hK : IsRealConcaveConvexOn C D K) (hL : IsRealConcaveConvexOn C D L) {C' : Set (EuclideanSpace ℝ (Fin m))} {D' : Set (EuclideanSpace ℝ (Fin n))} (hC'sub : C' ⊆ C) (hD'sub : D' ⊆ D) (hCclosure : C ⊆ closure C') (hDclosure : D ⊆ closure D') (hEqDense : ∀ u ∈ C', ∀ v ∈ D', L u v = K u v) (u : EuclideanSpace ℝ (Fin m)) : u ∈ C → ∀ v ∈ D, L u v = K u v

Helper for Text 35.10.1: two finite concave-convex kernels that agree on a dense product subset of an open convex rectangle agree on the whole rectangle.

theorem helperForText_35_10_1_pointwiseTendsto_to_prescribedKernel {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {KSeq : ℕ → (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hC_open : IsOpen C) (hD_open : IsOpen D) (hC_conv : Convex ℝ C) (hD_conv : Convex ℝ D) (hK : IsRealConcaveConvexOn C D K) (hKSeq : ∀ (i : ℕ), IsRealConcaveConvexOn C D (KSeq i)) (hDense : ∃ (C' : Set (Fin m → ℝ)) (D' : Set (Fin n → ℝ)), C' ⊆ C ∧ D' ⊆ D ∧ C ⊆ closure C' ∧ D ⊆ closure D' ∧ ∀ u ∈ C', ∀ v ∈ D', Filter.Tendsto (fun (i : ℕ) => KSeq i u v) Filter.atTop (nhds (K u v))) (u : Fin m → ℝ) : u ∈ C → ∀ v ∈ D, Filter.Tendsto (fun (i : ℕ) => KSeq i u v) Filter.atTop (nhds (K u v))

Helper for Text 35.10.1: the dense convergence hypothesis already forces pointwise convergence of Kᵢ to the prescribed kernel K on all of C × D.

theorem section35_text35_10_1 {m n : ℕ} {C : Set (Fin m → ℝ)} {D : Set (Fin n → ℝ)} {K : (Fin m → ℝ) → (Fin n → ℝ) → ℝ} {KSeq : ℕ → (Fin m → ℝ) → (Fin n → ℝ) → ℝ} (hNonempty : (C ×ˢ D).Nonempty) (hC_open : IsOpen C) (hD_open : IsOpen D) (hC_conv : Convex ℝ C) (hD_conv : Convex ℝ D) (hK : IsRealConcaveConvexOn C D K) (hK_diff : ∀ u ∈ C, ∀ v ∈ D, DifferentiableAt ℝ (packedRealSaddleKernel K) (Fin.append u v)) (hKSeq : ∀ (i : ℕ), IsRealConcaveConvexOn C D (KSeq i)) (hKSeq_diff : ∀ (i : ℕ), ∀ u ∈ C, ∀ v ∈ D, DifferentiableAt ℝ (packedRealSaddleKernel (KSeq i)) (Fin.append u v)) (hDense : ∃ (C' : Set (Fin m → ℝ)) (D' : Set (Fin n → ℝ)), C' ⊆ C ∧ D' ⊆ D ∧ C ⊆ closure C' ∧ D ⊆ closure D' ∧ ∀ u ∈ C', ∀ v ∈ D', Filter.Tendsto (fun (i : ℕ) => KSeq i u v) Filter.atTop (nhds (K u v))) : (∀ u ∈ C, ∀ v ∈ D, Filter.Tendsto (fun (i : ℕ) => KSeq i u v) Filter.atTop (nhds (K u v))) ∧ (∀ u ∈ C, ∀ v ∈ D, Filter.Tendsto (fun (i : ℕ) => packedRealSaddleKernelGradientPair (KSeq i) u v) Filter.atTop (nhds (packedRealSaddleKernelGradientPair K u v))) ∧ ∀ S ⊆ C ×ˢ D, IsClosed S → Bornology.IsBounded S → TendstoUniformlyOn (fun (i : ℕ) (p : (Fin m → ℝ) × (Fin n → ℝ)) => packedRealSaddleKernelGradientPair (KSeq i) p.1 p.2) (fun (p : (Fin m → ℝ) × (Fin n → ℝ)) => packedRealSaddleKernelGradientPair K p.1 p.2) Filter.atTop S

Text 35.10.1: let C × D be a nonempty open convex subset of ℝ^m × ℝ^n, let K be a finite differentiable concave-convex function on C × D, and let K₁, K₂, ... be finite differentiable concave-convex functions on C × D. If there exist dense subsets C' ⊆ C and D' ⊆ D such that (A) Kᵢ(u, v) → K(u, v) for every (u, v) ∈ C' × D', then (B) Kᵢ(u, v) → K(u, v) for every (u, v) ∈ C × D. Consequently, the conclusion of Theorem 35.10 holds: the split gradient maps converge pointwise on C × D and uniformly on each closed bounded subset of C × D.