Differentiability almost everywhere of a saddle-function

A finite concave-convex function on an open rectangle C × D is differentiable almost everywhere there, its points of differentiability are dense, and the gradient mapping is continuous on them. Gradients also converge wherever the functions converge pointwise, uniformly on every compact subset.

Convexity supplies only a local Lipschitz constant on a ball, after which Rademacher's theorem does the analysis. The convergence statements come from upper semicontinuity of the saddle subdifferential, with the subdifferentials collapsed to singletons at points of differentiability; in particular the pointwise clause needs differentiability only at the point in question.

Main results

• ConcaveConvexOn.exists_lipschitzOnWith_ball — a Lipschitz constant on a ball, which is what Rademacher's theorem needs: differentiability within an open set is differentiability.
• ae_differentiableAt_of_concaveConvexOn, measure_diff_differentiableAt_of_concaveConvexOn, subset_closure_differentiableAt_of_concaveConvexOn, continuousOn_saddleGradient — differentiability almost everywhere in two forms, then density and continuity of the gradient (Theorem 35.9 in [^1]).
• tendsto_of_hasSaddleGradientAt, tendstoUniformlyOn_saddleGradient — gradients converge under pointwise convergence, uniformly on compact sets (Theorem 35.10 in [^1]).

Implementation notes

HasSaddleGradientAt K q p says ∇K p = q for a pair q : U × X, and there is no canonical ∇K without choice, so the continuity and convergence statements take any G with HasSaddleGradientAt K (G p) p on the set in question; prodInnerL is injective, so such a G is unique there. The εB is the supremum ball of U × X; the Euclidean ball differs from it by a bounded factor, and every statement quantifies over all ε > 0.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §35.

A Lipschitz constant on a ball

theorem Tdaf.ConvexAnalysis.ConcaveConvexOn.exists_lipschitzOnWith_ball {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} {p : U × X} (hCo : IsOpen C) (hCc : Convex ℝ C) (hDo : IsOpen D) (hDc : Convex ℝ D) (hK : ConcaveConvexOn C D K) (hp : p ∈ C ×ˢ D) : ∃ r > 0, Metric.ball p r ⊆ C ×ˢ D ∧ ∃ (k : NNReal), LipschitzOnWith k K (Metric.ball p r)

A finite concave-convex function on an open rectangle is Lipschitz on a whole ball around each of its points. Local Lipschitzness gives a constant on a product of compact sets; shrinking to an open ball makes it open as well, which is what upgrades DifferentiableWithinAt to DifferentiableAt.

Differentiability almost everywhere

theorem Tdaf.ConvexAnalysis.ae_differentiableAt_of_concaveConvexOn {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} [MeasurableSpace (U × X)] [BorelSpace (U × X)] {μ : MeasureTheory.Measure (U × X)} [μ.IsAddHaarMeasure] (hCo : IsOpen C) (hCc : Convex ℝ C) (hDo : IsOpen D) (hDc : Convex ℝ D) (hK : ConcaveConvexOn C D K) : ∀ᵐ (p : U × X) ∂μ, p ∈ C ×ˢ D → DifferentiableAt ℝ K p

A finite concave-convex function on an open rectangle is differentiable at almost every point of it.

theorem Tdaf.ConvexAnalysis.measure_diff_differentiableAt_of_concaveConvexOn {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} [MeasurableSpace (U × X)] [BorelSpace (U × X)] {μ : MeasureTheory.Measure (U × X)} [μ.IsAddHaarMeasure] (hCo : IsOpen C) (hCc : Convex ℝ C) (hDo : IsOpen D) (hDc : Convex ℝ D) (hK : ConcaveConvexOn C D K) : μ (C ×ˢ D \ {p : U × X | DifferentiableAt ℝ K p}) = 0

The points of the open rectangle at which K is not differentiable form a null set.

theorem Tdaf.ConvexAnalysis.subset_closure_differentiableAt_of_concaveConvexOn {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} (hCo : IsOpen C) (hCc : Convex ℝ C) (hDo : IsOpen D) (hDc : Convex ℝ D) (hK : ConcaveConvexOn C D K) : C ×ˢ D ⊆ closure {p : U × X | DifferentiableAt ℝ K p}

The points of differentiability are dense in the open rectangle. No measure appears in the statement; the proof borrows one.

Continuity of the gradient

theorem Tdaf.ConvexAnalysis.continuousOn_saddleGradient {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} (hCo : IsOpen C) (hCc : Convex ℝ C) (hDo : IsOpen D) (hDc : Convex ℝ D) (hK : ConcaveConvexOn C D K) {S : Set (U × X)} (hS : S ⊆ C ×ˢ D) {G : U × X → U × X} (hG : ∀ p ∈ S, HasSaddleGradientAt K (G p) p) : ContinuousOn G S

The gradient mapping is continuous on any set of points of the open rectangle at which it exists: upper semicontinuity of ∂K with both subdifferentials collapsed to singletons.

Convergence of gradients

theorem Tdaf.ConvexAnalysis.dist_le_of_subgradientSaddle_subset {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] {C : Set U} {D : Set X} {p : U × X} (hCo : IsOpen C) (hDo : IsOpen D) {L M : U × X → ℝ} {p' a b : U × X} {ε : ℝ} (hL : ConcaveConvexOn C D L) (hM : ConcaveConvexOn C D M) (hp : p ∈ C ×ˢ D) (hp' : p' ∈ C ×ˢ D) (ha : HasSaddleGradientAt L a p) (hb : HasSaddleGradientAt M b p') (hsub : subgradientSaddle C D L p ⊆ subgradientSaddle C D M p' + Metric.closedBall 0 ε) : dist a b ≤ ε

An inclusion of singleton subdifferentials is a bound on gradients. If ∇L(p) = a, ∇M(p') = b and ∂L(p) ⊆ ∂M(p') + εB, then ‖a - b‖ ≤ ε.

theorem Tdaf.ConvexAnalysis.tendsto_of_hasSaddleGradientAt {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} {Ks : ℕ → U × X → ℝ} {p : U × X} (hCo : IsOpen C) (hCc : Convex ℝ C) (hDo : IsOpen D) (hDc : Convex ℝ D) (hKs : ∀ (i : ℕ), ConcaveConvexOn C D (Ks i)) (hK : ConcaveConvexOn C D K) (hconv : ∀ q ∈ C ×ˢ D, Filter.Tendsto (fun (i : ℕ) => Ks i q) Filter.atTop (nhds (K q))) (hp : p ∈ C ×ˢ D) {G : ℕ → U × X} {G' : U × X} (hG : ∀ (i : ℕ), HasSaddleGradientAt (Ks i) (G i) p) (hG' : HasSaddleGradientAt K G' p) : Filter.Tendsto G Filter.atTop (nhds G')

The gradients of finite concave-convex functions converging pointwise on an open rectangle converge at every point of it. Subdifferential convergence along the constant sequence of points, with the subdifferentials collapsed to singletons; differentiability is needed only at the point in question.

theorem Tdaf.ConvexAnalysis.tendstoUniformlyOn_saddleGradient {U : Type u_1} {X : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] {C : Set U} {D : Set X} {K : U × X → ℝ} {Ks : ℕ → U × X → ℝ} (hCo : IsOpen C) (hCc : Convex ℝ C) (hDo : IsOpen D) (hDc : Convex ℝ D) (hKs : ∀ (i : ℕ), ConcaveConvexOn C D (Ks i)) (hK : ConcaveConvexOn C D K) (hconv : ∀ q ∈ C ×ˢ D, Filter.Tendsto (fun (i : ℕ) => Ks i q) Filter.atTop (nhds (K q))) {Gs : ℕ → U × X → U × X} {G : U × X → U × X} (hGs : ∀ (i : ℕ), ∀ q ∈ C ×ˢ D, HasSaddleGradientAt (Ks i) (Gs i q) q) (hG : ∀ q ∈ C ×ˢ D, HasSaddleGradientAt K (G q) q) {S : Set (U × X)} (hS : IsCompact S) (hSU : S ⊆ C ×ˢ D) : TendstoUniformlyOn Gs G Filter.atTop S

On every compact subset of the open rectangle the gradients converge uniformly.

A failure of uniform convergence on a compact S produces indices φ n and points zₙ ∈ S with ‖∇K(zₙ) - ∇K_{φ n}(zₙ)‖ ≥ ε; a convergent subsequence zₙ → w ∈ S turns subdifferential convergence along the subsequence and upper semicontinuity at w into two ε/3 bounds that contradict it.