The convex primitive of a nondecreasing function on the line

A nondecreasing φ : ℝ → [-∞, +∞] that is finite somewhere is squeezed between the two one-sided derivatives of a closed proper convex function on ℝ, uniquely determined up to an additive constant. The uniqueness clause is in Subgradient/OneDim.lean; this module supplies the existence clause.

The object that carries the construction is the region

Γ(φ) = {(x, y) ∈ ℝ × ℝ | φ⁻(x) ≤ y ≤ φ⁺(x)},   φ⁻(x) = ⨆_{z < x} φ z,  φ⁺(x) = ⨅_{z > x} φ z,

a complete non-decreasing curve. It is a chain for the coordinatewise order and it meets every antidiagonal {(u, v) | u + v = s}, which is exactly what makes it a maximal chain. A maximal monotone relation on the line is a subdifferential, so this yields a closed proper convex f with ∂f = Γ(φ); reading the endpoints of Γ(φ)ₓ off ∂f(x) gives f'₋ = φ⁻ ≤ φ ≤ φ⁺ = f'₊. No integral appears anywhere: the classical f(x) = ∫ₐˣ φ(t) dt is replaced by ∂f itself.

Main results

• monotoneCurve — the region Γ(φ) above; isMaximalMonotoneRel_monotoneCurve says it is a maximal monotone mapping, and subgradientRel_eq_monotoneCurve_rightDeriv is the converse, that every ∂f on the line is the curve of its own right derivative.
• exists_monotone_ne_bot_ne_top_monotoneCurve_eq — every ∂f is Γ(φ) for a φ finite at a point, since moving φ at one point changes neither its monotonicity nor Γ(φ).
• exists_closedProperConvexFn_leftDeriv_eq_rightDeriv_eq — the existence clause, with the identification f'₋ = φ⁻ and f'₊ = φ⁺.
• exists_closedProperConvexFn_forall_le_le — existence with uniqueness (Theorem 24.2 in [^1]).

Implementation notes

Maximality of Γ(φ) is proved from the antidiagonal statement rather than by case analysis on the places where φ is ±∞: if p is comparable with every element of Γ(φ), then a q ∈ Γ(φ) with the same coordinate sum must equal it. Γ(φ)ₓ can be empty — to the left of a point where φ = -∞ — so the identity Γ(φ) = ∂f says nothing pointwise there; what settles the endpoints is that an empty extended-real interval has both of them -∞ or both +∞, the two alternatives being separated by comparison with a fibre that is not empty.

References

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

Extended-real intervals

theorem Tdaf.ConvexAnalysis.eq_and_eq_of_forall_coe_mem_iff {A₁ B₁ A₂ B₂ : EReal} (hne : ∃ (y : ℝ), A₁ ≤ ↑y ∧ ↑y ≤ B₁) (h : ∀ (y : ℝ), A₁ ≤ ↑y ∧ ↑y ≤ B₁ ↔ A₂ ≤ ↑y ∧ ↑y ≤ B₂) : A₁ = A₂ ∧ B₁ = B₂

Two extended-real intervals with the same real points have the same endpoints, as soon as one of them contains a real point.

theorem Tdaf.ConvexAnalysis.eq_bot_or_eq_top_of_forall_not_coe_mem {A B : EReal} (hAB : A ≤ B) (h : ∀ (y : ℝ), ¬(A ≤ ↑y ∧ ↑y ≤ B)) : A = ⊥ ∧ B = ⊥ ∨ A = ⊤ ∧ B = ⊤

An extended-real interval with no real point is degenerate at one end of the line. If A ≤ B and no real y satisfies A ≤ y ≤ B, then A = B = -∞ or A = B = +∞: a finite A would be such a y, and A = -∞ with B ≠ -∞ leaves room for one.

The complete non-decreasing curve of a nondecreasing function

def Tdaf.ConvexAnalysis.monotoneCurve (φ : ℝ → EReal) : SetRel ℝ ℝ

The region between the two one-sided limits of φ,

Γ(φ) = {(x, y) | ⨆_{z < x} φ z ≤ y ≤ ⨅_{z > x} φ z},

a complete non-decreasing curve. For nondecreasing φ it is a chain for the coordinatewise order on ℝ × ℝ, and it is the graph of ∂f for a closed proper convex f.

Equations

• Tdaf.ConvexAnalysis.monotoneCurve φ = {p : ℝ × ℝ | ⨆ z ∈ Set.Iio p.1, φ z ≤ ↑p.2 ∧ ↑p.2 ≤ ⨅ z ∈ Set.Ioi p.1, φ z}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_monotoneCurve {φ : ℝ → EReal} {x y : ℝ} : (x, y) ∈ monotoneCurve φ ↔ ⨆ z ∈ Set.Iio x, φ z ≤ ↑y ∧ ↑y ≤ ⨅ z ∈ Set.Ioi x, φ z

theorem Tdaf.ConvexAnalysis.isMonotoneRel_monotoneCurve (φ : ℝ → EReal) : IsMonotoneRel (innerₗ ℝ) (monotoneCurve φ)

The curve is a monotone mapping, for every φ, monotone or not: between two of its points with distinct abscissas sits a value of φ itself, which bounds the left ordinate from above and the right ordinate from below.

theorem Tdaf.ConvexAnalysis.exists_mem_monotoneCurve_sub {φ : ℝ → EReal} (hφ : Monotone φ) {a : ℝ} (hb : φ a ≠ ⊥) (ht : φ a ≠ ⊤) (s : ℝ) : ∃ (u : ℝ), (u, s - u) ∈ monotoneCurve φ

The curve meets every antidiagonal: for each s : ℝ there is a u with (u, s - u) ∈ Γ(φ). Equivalently (x, y) ↦ x + y maps a complete non-decreasing curve onto ℝ, and that is what makes the curve a maximal chain. The point is u = sup {t | φ t ≤ s - t}.

theorem Tdaf.ConvexAnalysis.isMaximalMonotoneRel_monotoneCurve {φ : ℝ → EReal} (hφ : Monotone φ) {a : ℝ} (hb : φ a ≠ ⊥) (ht : φ a ≠ ⊤) : IsMaximalMonotoneRel (innerₗ ℝ) (monotoneCurve φ)

The curve of a nondecreasing φ finite at one point is a maximal monotone mapping: a pair p comparable with everything on the curve equals the point of the curve with the same coordinate sum.

theorem Tdaf.ConvexAnalysis.subgradientRel_eq_monotoneCurve_rightDeriv {f : ℝ → EReal} (hf : ClosedProperConvexFn f) : subgradientRel (innerₗ ℝ) f = monotoneCurve (rightDeriv f)

Every subdifferential on the line is such a curve, namely the one of its own right derivative. This is the two crossed one-sided limit formulas read through mem_subgradientRel_iff.

Perturbing φ at a single point

Γ(φ) reads φ only through its two one-sided limits, so the value of φ at one isolated point is invisible to it — provided the new value stays between those limits, so that monotonicity survives. This is what lets a φ that is ±∞ everywhere be replaced by one that is finite somewhere.

theorem Tdaf.ConvexAnalysis.monotone_of_forall_ne_of_le_of_le {φ ψ : ℝ → EReal} {a : ℝ} (hφ : Monotone φ) (heq : ∀ (z : ℝ), z ≠ a → ψ z = φ z) (h₁ : ⨆ z ∈ Set.Iio a, φ z ≤ ψ a) (h₂ : ψ a ≤ ⨅ z ∈ Set.Ioi a, φ z) : Monotone ψ

A nondecreasing φ stays nondecreasing when its value at one point is moved anywhere between the two one-sided limits there.

theorem Tdaf.ConvexAnalysis.monotoneCurve_eq_of_forall_ne {φ ψ : ℝ → EReal} {a : ℝ} (hφ : Monotone φ) (heq : ∀ (z : ℝ), z ≠ a → ψ z = φ z) (h₁ : ⨆ z ∈ Set.Iio a, φ z ≤ ψ a) (h₂ : ψ a ≤ ⨅ z ∈ Set.Ioi a, φ z) : monotoneCurve ψ = monotoneCurve φ

Such a perturbation leaves the curve unchanged: neither ⨆_{z < x} φ z nor ⨅_{z > x} φ z can see the value at a, since ψ a is squeezed between values of φ at points strictly between a and x, which are themselves in the range of the supremum. This is what turns subgradientRel_eq_monotoneCurve_rightDeriv into a statement about a φ finite at a point.

theorem Tdaf.ConvexAnalysis.exists_monotone_ne_bot_ne_top_monotoneCurve_eq {f : ℝ → EReal} (hf : ClosedProperConvexFn f) : ∃ (φ : ℝ → EReal), Monotone φ ∧ (∃ (a : ℝ), φ a ≠ ⊥ ∧ φ a ≠ ⊤) ∧ subgradientRel (innerₗ ℝ) f = monotoneCurve φ

Every subdifferential on the line is the curve of a nondecreasing function that is finite somewhere — the implication from the order-theoretic characterisation of a complete non-decreasing curve back to the usual definition of one.

subgradientRel_eq_monotoneCurve_rightDeriv gives ∂f = Γ(f'₊) with f'₊ nondecreasing, so only finiteness at a point is missing. f'₊ is finite on int (dom f); the one case that does not cover is dom f a single point a, and there f'₊ is replaced at one point of ri (dom f) by a subgradient, which the curve does not notice.

The convex primitive

theorem Tdaf.ConvexAnalysis.exists_closedProperConvexFn_leftDeriv_eq_rightDeriv_eq {φ : ℝ → EReal} (hφ : Monotone φ) {a : ℝ} (hb : φ a ≠ ⊥) (ht : φ a ≠ ⊤) : ∃ (f : ℝ → EReal), ClosedProperConvexFn f ∧ (∀ (x : ℝ), leftDeriv f x = ⨆ z ∈ Set.Iio x, φ z) ∧ ∀ (x : ℝ), rightDeriv f x = ⨅ z ∈ Set.Ioi x, φ z

The existence clause, in its sharpest form: a nondecreasing φ : ℝ → [-∞, +∞] finite at one point is the derivative of a closed proper convex function on the line, in the precise sense that the one-sided limits of φ are the one-sided derivatives of f.

Maximality of Γ(φ) turns it into an f with ∂f = Γ(φ); at a fixed x that says the intervals [φ⁻(x), φ⁺(x)] and [f'₋(x), f'₊(x)] have the same real points, hence the same endpoints whenever either has a real point at all. Where neither has, both are {-∞} or both {+∞}, decided by comparison across the point where φ is finite.

theorem Tdaf.ConvexAnalysis.exists_closedProperConvexFn_forall_le_le {φ : ℝ → EReal} (hφ : Monotone φ) {a : ℝ} (hb : φ a ≠ ⊥) (ht : φ a ≠ ⊤) : ∃ (f : ℝ → EReal), ClosedProperConvexFn f ∧ (∀ (x : ℝ), leftDeriv f x ≤ φ x) ∧ (∀ (x : ℝ), φ x ≤ rightDeriv f x) ∧ ∀ (g : ℝ → EReal), ClosedProperConvexFn g → (∀ (x : ℝ), leftDeriv g x ≤ φ x) → (∀ (x : ℝ), φ x ≤ rightDeriv g x) → ∃ (α : ℝ), ∀ (x : ℝ), g x = f x + ↑α

A nondecreasing φ : ℝ → [-∞, +∞] that is finite at one point lies between the one-sided derivatives of a closed proper convex function on the line, and that function is unique up to an additive constant.