Convex functions with the same derivative differ by a constant

Two differentiable functions with the same derivative on a connected open set differ by a constant there (IsOpen.exists_eq_add_of_fderiv_eq). This file proves the analogue for convex functions, which are only differentiable almost everywhere: if two extended-real convex functions u v : E → EReal are finite on a connected open set Ω and have the same derivative at almost every point of Ω, then u = v + c on Ω for a real constant c.

This is the uniqueness of the convex potential in Brenier's theorem: the optimal transport map ∇ u determines u up to an additive constant on every connected open set carrying the source law, as soon as that law charges every Lebesgue-positive subset of it.

The one-variable slope comparison lemmas are in TauCeti.Analysis.Convex.Deriv. The proof restricts u and v to lines. Where both functions have a common derivative f', the one-variable convexity inequalities along a line in direction h give slope u a b ≤ f' h ≤ slope v b c for parameters a < b < c, and by continuity this cross-slope inequality persists at every point of the closure of the common-derivative set. Letting the slopes shrink, the right derivatives of the two restrictions agree, so their difference has right derivative zero and is constant along the line. The difference is therefore locally constant, hence constant on the connected set Ω. Only density of the common-derivative set is used; in finite dimension Rademacher's theorem for convex functions (TauCeti.ae_eventually_ne_top_and_differentiableAt_toReal) supplies it from an almost everywhere hypothesis.

As elsewhere, a convex function f : E → EReal is one with convex real epigraph {(x, r) | f x ≤ r} that never takes the value ⊥, and its derivative is that of the real representative x ↦ (f x).toReal.

Main statements

• IsOpen.exists_eq_add_of_subset_closure_hasFDerivAt_eq — on a real normed space, convex functions finite and continuous on a connected open set Ω that have a common derivative on a dense subset of Ω differ by a constant on Ω;
• IsOpen.exists_eq_add_of_fderiv_ae_eq — in finite dimension, convex functions finite on a connected open set Ω whose derivatives agree μ-almost everywhere, for a measure μ with respect to which Lebesgue measure on Ω is absolutely continuous, differ by a constant on Ω;
• IsOpen.exists_eq_add_of_gradient_ae_eq — the same statement for gradients on a finite-dimensional real inner product space.

References

• R. T. Rockafellar, Convex Analysis, Princeton Mathematical Series 28, 1970, §24 (one-sided derivatives of convex functions) and Theorem 25.5 (almost-everywhere differentiability).
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, Theorem 2.12, for the uniqueness of the Brenier potential.

theorem IsOpen.exists_eq_add_of_subset_closure_hasFDerivAt_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {u v : E → EReal} {Ω : Set E} (hΩ : IsOpen Ω) (hΩc : IsPreconnected Ω) (hu : Convex ℝ {p : E × ℝ | u p.1 ≤ ↑p.2}) (hubot : ∀ (x : E), u x ≠ ⊥) (hv : Convex ℝ {p : E × ℝ | v p.1 ≤ ↑p.2}) (hvbot : ∀ (x : E), v x ≠ ⊥) (huΩ : ∀ x ∈ Ω, u x ≠ ⊤) (hvΩ : ∀ x ∈ Ω, v x ≠ ⊤) (huc : ContinuousOn (fun (x : E) => (u x).toReal) Ω) (hvc : ContinuousOn (fun (x : E) => (v x).toReal) Ω) (hD : Ω ⊆ closure {x : E | ∃ (f' : E →L[ℝ] ℝ), HasFDerivAt (fun (x : E) => (u x).toReal) f' x ∧ HasFDerivAt (fun (x : E) => (v x).toReal) f' x}) : ∃ (c : ℝ), Set.EqOn u (fun (x : E) => v x + ↑c) Ω

Convex functions with the same derivative on a dense set differ by a constant. Let u v : E → EReal be convex functions (convex real epigraph, never ⊥) on a real normed space, finite on a connected open set Ω, with real representatives continuous on Ω. If every point of Ω is a limit of points at which the real representatives of u and v have a common derivative, then u = v + c on Ω for some real constant c.

theorem IsOpen.exists_eq_add_of_fderiv_ae_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {u v : E → EReal} {Ω : Set E} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ρ μ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] (hΩ : IsOpen Ω) (hΩc : IsPreconnected Ω) (hu : Convex ℝ {p : E × ℝ | u p.1 ≤ ↑p.2}) (hubot : ∀ (x : E), u x ≠ ⊥) (hv : Convex ℝ {p : E × ℝ | v p.1 ≤ ↑p.2}) (hvbot : ∀ (x : E), v x ≠ ⊥) (huΩ : ∀ x ∈ Ω, u x ≠ ⊤) (hvΩ : ∀ x ∈ Ω, v x ≠ ⊤) (hμ : (ρ.restrict Ω).AbsolutelyContinuous μ) (h : (fderiv ℝ fun (x : E) => (u x).toReal) =ᵐ[μ] fderiv ℝ fun (x : E) => (v x).toReal) : ∃ (c : ℝ), Set.EqOn u (fun (x : E) => v x + ↑c) Ω

Convex functions with almost everywhere equal derivatives differ by a constant. Let u v : E → EReal be convex functions (convex real epigraph, never ⊥) on a finite-dimensional real normed space, finite on a connected open set Ω. Let ρ be an additive Haar measure and μ a measure such that the restriction of ρ to Ω is absolutely continuous with respect to μ, as when μ restricted to Ω is equivalent to Lebesgue measure on Ω. If the derivatives of the real representatives of u and v agree μ-almost everywhere, then u = v + c on Ω for some real constant c.

theorem IsOpen.exists_eq_add_of_gradient_ae_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ρ μ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] {u v : E → EReal} {Ω : Set E} (hΩ : IsOpen Ω) (hΩc : IsPreconnected Ω) (hu : Convex ℝ {p : E × ℝ | u p.1 ≤ ↑p.2}) (hubot : ∀ (x : E), u x ≠ ⊥) (hv : Convex ℝ {p : E × ℝ | v p.1 ≤ ↑p.2}) (hvbot : ∀ (x : E), v x ≠ ⊥) (huΩ : ∀ x ∈ Ω, u x ≠ ⊤) (hvΩ : ∀ x ∈ Ω, v x ≠ ⊤) (hμ : (ρ.restrict Ω).AbsolutelyContinuous μ) (h : (gradient fun (x : E) => (u x).toReal) =ᵐ[μ] gradient fun (x : E) => (v x).toReal) : ∃ (c : ℝ), Set.EqOn u (fun (x : E) => v x + ↑c) Ω

Uniqueness of a convex potential up to a constant. Let u v : E → EReal be convex functions (convex real epigraph, never ⊥) on a finite-dimensional real inner product space, finite on a connected open set Ω, and let μ be a measure with respect to which Lebesgue measure on Ω (any additive Haar measure ρ restricted to Ω) is absolutely continuous. If the gradients of the real representatives of u and v agree μ-almost everywhere, then u = v + c on Ω for some real constant c. In particular a Brenier map ∇ u determines its convex potential u up to an additive constant on such a set.