Differentiability of extended-real convex functions

A convex function f : E → EReal is one whose real epigraph {(x, r) | f x ≤ r} is convex, the convention of TauCeti.convex_epigraph_fenchelConjugate; Legendre–Fenchel conjugates are the basic examples. This file connects such functions to Mathlib's real-valued convexity and differentiability theory.

The effective-domain and real-representative convexity bridges are in TauCeti.Analysis.Convex.EffectiveDomain. In finite dimension, Rademacher's theorem for convex functions applies: at almost every point of the effective domain, f is finite on a neighbourhood and the real representative is differentiable (TauCeti.ae_eventually_ne_top_and_differentiableAt_toReal). This is the almost-everywhere differentiability of convex potentials used to turn optimal plans into transport maps, as in Brenier's theorem.

At such a point the subdifferential of f for a pairing B reduces to the derivative: every subgradient y satisfies D f (x) v = B v y for all v (TauCeti.hasFDerivAt_apply_eq_of_mem_subdifferential). This needs neither convexity nor finite dimension. On a real inner product space, with the inner product as pairing, the subgradient is then the gradient (TauCeti.hasGradientAt_toReal_of_mem_subdifferential): this is how the gradient of a convex potential becomes a transport map. Conversely, for a convex f the derivative at any point of the effective domain where the real representative is differentiable is a subgradient (TauCeti.mem_subdifferential_of_hasFDerivAt), since a convex function of one variable lies above its tangent lines; this is how the gradient of a convex potential is shown to be an optimal transport map.

Main statements

• TauCeti.ae_eventually_ne_top_and_differentiableAt_toReal — Rademacher's theorem for extended-real convex functions: at almost every point of the effective domain, f is finite nearby and differentiable;
• TauCeti.hasFDerivAt_apply_eq_of_mem_subdifferential and TauCeti.fderiv_apply_eq_of_mem_subdifferential — at an interior point of the effective domain where f is differentiable, every subgradient is the derivative;
• TauCeti.hasGradientAt_toReal_of_mem_subdifferential and TauCeti.gradient_toReal_eq_of_mem_subdifferential — the same statement for the inner product, where every subgradient is the gradient;
• TauCeti.mem_subdifferential_of_hasFDerivAt and TauCeti.gradient_toReal_mem_subdifferential — for a convex function, the derivative, respectively the gradient, at a point of differentiability in the effective domain is a subgradient.

References

• R. T. Rockafellar, Convex Analysis, Princeton Mathematical Series 28, 1970, §4 (effective domains), Theorem 25.1 (subgradients at points of differentiability) and Theorem 25.5 (almost-everywhere differentiability).
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §2.1, for the use of these facts in the proof of Brenier's theorem.

theorem TauCeti.ae_eventually_ne_top_and_differentiableAt_toReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) : ∀ᵐ (x : E) ∂μ, f x ≠ ⊤ → (∀ᶠ (x' : E) in nhds x, f x' ≠ ⊤) ∧ DifferentiableAt ℝ (fun (x' : E) => (f x').toReal) x

Rademacher's theorem for extended-real convex functions. Let f : E → EReal have convex real epigraph and never take the value ⊥, on a finite-dimensional real normed space E with an additive Haar measure μ. Then at μ-almost every point x of the effective domain, f is finite on a neighbourhood of x and its real representative x ↦ (f x).toReal is differentiable at x.

theorem TauCeti.hasFDerivAt_apply_eq_of_mem_subdifferential {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {F : Type u_2} [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {x : E} {y : F} {f' : E →L[ℝ] ℝ} (hy : y ∈ subdifferential B f x) (hdom : ∀ᶠ (x' : E) in nhds x, f x' ≠ ⊤) (hf : HasFDerivAt (fun (x' : E) => (f x').toReal) f' x) (v : E) : f' v = (B v) y

Subgradients at a point of differentiability. If f : E → EReal is finite near x, its real representative has derivative f' at x, and y is a subgradient of f at x for the pairing B, then f' v = B v y for every v: the subdifferential at x consists of representatives of the derivative.

theorem TauCeti.fderiv_apply_eq_of_mem_subdifferential {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {F : Type u_2} [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {x : E} {y : F} (hy : y ∈ subdifferential B f x) (hdom : ∀ᶠ (x' : E) in nhds x, f x' ≠ ⊤) (hf : DifferentiableAt ℝ (fun (x' : E) => (f x').toReal) x) (v : E) : (fderiv ℝ (fun (x' : E) => (f x').toReal) x) v = (B v) y

The fderiv form of TauCeti.hasFDerivAt_apply_eq_of_mem_subdifferential: at a point where f is finite nearby and differentiable, every subgradient y satisfies fderiv ℝ (fun x' => (f x').toReal) x v = B v y for every v.

theorem TauCeti.mem_subdifferential_of_hasFDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {F : Type u_2} [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {x : E} {y : F} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) (hx : f x ≠ ⊤) {f' : E →L[ℝ] ℝ} (hd : HasFDerivAt (fun (x' : E) => (f x').toReal) f' x) (hy : ∀ (v : E), f' v = (B v) y) : y ∈ subdifferential B f x

Derivatives of convex functions are subgradients. Let f : E → EReal have convex real epigraph and never take the value ⊥, and let x be a point of the effective domain at which the real representative x' ↦ (f x').toReal has derivative f'. If y represents f' for the pairing B, that is f' v = B v y for every v, then y is a subgradient of f at x.

theorem TauCeti.hasGradientAt_toReal_of_mem_subdifferential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {x y : E} (hy : y ∈ subdifferential (innerₗ E) f x) (hdom : ∀ᶠ (x' : E) in nhds x, f x' ≠ ⊤) (hf : DifferentiableAt ℝ (fun (x' : E) => (f x').toReal) x) : HasGradientAt (fun (x' : E) => (f x').toReal) y x

Subgradients at a point of differentiability are gradients. If f : E → EReal is finite near x, its real representative is differentiable at x, and y is a subgradient of f at x for the inner product, then y is the gradient of the real representative at x.

theorem TauCeti.gradient_toReal_eq_of_mem_subdifferential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {x y : E} (hy : y ∈ subdifferential (innerₗ E) f x) (hdom : ∀ᶠ (x' : E) in nhds x, f x' ≠ ⊤) (hf : DifferentiableAt ℝ (fun (x' : E) => (f x').toReal) x) : gradient (fun (x' : E) => (f x').toReal) x = y

The gradient form of TauCeti.hasGradientAt_toReal_of_mem_subdifferential: at a point where f is finite nearby and differentiable, every subgradient for the inner product is the gradient of the real representative.

theorem TauCeti.gradient_toReal_mem_subdifferential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {x : E} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) (hx : f x ≠ ⊤) (hd : DifferentiableAt ℝ (fun (x' : E) => (f x').toReal) x) : gradient (fun (x' : E) => (f x').toReal) x ∈ subdifferential (innerₗ E) f x

Gradients of convex functions are subgradients. If f : E → EReal has convex real epigraph, never takes the value ⊥, and is finite at x, where its real representative is differentiable, then the gradient of the real representative at x is a subgradient of f at x for the inner product.