One-sided derivatives of a convex function on the line

On the line a convex function has a right derivative f'₊ and a left derivative f'₋ at every point, with values in [-∞, +∞], and they carry all the first-order information: ∂f(x) = {x* ∈ ℝ | f'₋(x) ≤ x* ≤ f'₊(x)}. Both are nondecreasing, interlaced as f'₊(z₁) ≤ f'₋(x) ≤ f'₊(x) ≤ f'₋(z₂) for z₁ < x < z₂, and both are real exactly on int (dom f). When f is closed each is the one-sided limit of the other — f'₊(z) and f'₋(z) both tend to f'₊(x) as z ↓ x, and to f'₋(x) as z ↑ x — so f'₊ is right-continuous, f'₋ is left-continuous, and either determines the other. Hence any nondecreasing φ with f'₋ ≤ φ ≤ f'₊ determines ∂f, and so determines f up to a constant.

One dimension also collapses the two monotonicity notions of Subgradient/Monotone.lean into one. A monotone relation on ℝ is exactly a set totally ordered by the coordinatewise order of ℝ × ℝ, a non-decreasing curve, and any cycle through such a set may be rotated to start at its largest pair, which dominates the cycle in both coordinates and may therefore be deleted without decreasing the telescoping sum. So monotone and cyclically monotone agree on the line, and the maximal monotone relations — the complete non-decreasing curves — are precisely the graphs of the subdifferentials of the closed proper convex functions.

Main definitions

• rightDeriv f x, leftDeriv f x — the two one-sided derivatives, extended by +∞ to the right of dom f and by -∞ to its left.
• cycleVal B L — the telescoping sum around a cycle presented as a single list of pairs, the form in which rotation invariance is expressible.

Main results

• mem_subgradient_iff_le_rightDeriv — ∂f(x) is the interval [f'₋(x), f'₊(x)].
• iInf_rightDeriv_Ioi, iSup_leftDeriv_Iio, iInf_leftDeriv_Ioi, iSup_rightDeriv_Iio and their Tendsto forms — the four limit formulas, for a closed proper convex f.
• exists_eq_add_coe_of_le_le — two closed proper convex functions squeezed around a common φ differ by a constant.
• IsMonotoneRel.isCyclicallyMonotone — on the line the two monotonicity notions coincide.
• isMaximalMonotoneRel_iff_exists_closedProperConvexFn — the maximal monotone relations on the line are exactly the subdifferentials of closed proper convex functions (Theorem 24.3 in [^1]).

Implementation notes

f'₊ is f'(x; 1) and f'₋ is -f'(x; -1), so the whole theory of dirDeriv is available and nothing is redefined. Both are guarded: f'₊(x) is f'(x; 1) provided some point of dom f lies to the right of x, and +∞ otherwise. The guard is needed because where f x = ⊤ every difference quotient is ⊤ - ⊤ = ⊥, so the unguarded infimum would be -∞ on both sides of dom f, and the two sides must be told apart. Where f is finite the guard is inert.

References

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

The directional derivative at a point outside the effective domain

theorem Tdaf.ConvexAnalysis.dirDeriv_eq_bot_of_eq_top {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {x : E} (hx : f x = ⊤) (y : E) : dirDeriv f x y = ⊥

Where f is +∞ every difference quotient is -∞, so the directional derivative is -∞ in every direction. This is the value wanted to the left of dom f and the one overrides to the right.

The right and left derivatives

noncomputable def Tdaf.ConvexAnalysis.rightDeriv (f : ℝ → EReal) (x : ℝ) : EReal

The right derivative of an extended-real-valued function on the line,

f'₊(x) = lim_{z ↓ x} (f z - f x) / (z - x),

with the convention that it is +∞ at every point lying to the right of dom f. Without that override the difference quotients would all be -∞ there, which is the value belonging to the points on the left.

Equations

• Tdaf.ConvexAnalysis.rightDeriv f x = ⨅ (_ : ∃ (z : ℝ), x < z ∧ f z < ⊤), Tdaf.ConvexAnalysis.dirDeriv f x 1

noncomputable def Tdaf.ConvexAnalysis.leftDeriv (f : ℝ → EReal) (x : ℝ) : EReal

The left derivative

f'₋(x) = lim_{z ↑ x} (f z - f x) / (z - x),

-∞ at every point lying to the left of dom f. It is -f'(x; -1) because the increment z - x is negative.

Equations

• Tdaf.ConvexAnalysis.leftDeriv f x = ⨆ (_ : ∃ z < x, f z < ⊤), -Tdaf.ConvexAnalysis.dirDeriv f x (-1)

theorem Tdaf.ConvexAnalysis.rightDeriv_of_exists {f : ℝ → EReal} {x : ℝ} (h : ∃ (z : ℝ), x < z ∧ f z < ⊤) : rightDeriv f x = dirDeriv f x 1

theorem Tdaf.ConvexAnalysis.rightDeriv_of_not_exists {f : ℝ → EReal} {x : ℝ} (h : ¬∃ (z : ℝ), x < z ∧ f z < ⊤) : rightDeriv f x = ⊤

theorem Tdaf.ConvexAnalysis.leftDeriv_of_exists {f : ℝ → EReal} {x : ℝ} (h : ∃ z < x, f z < ⊤) : leftDeriv f x = -dirDeriv f x (-1)

theorem Tdaf.ConvexAnalysis.leftDeriv_of_not_exists {f : ℝ → EReal} {x : ℝ} (h : ¬∃ z < x, f z < ⊤) : leftDeriv f x = ⊥

theorem Tdaf.ConvexAnalysis.rightDeriv_eq_bot_of_eq_top {f : ℝ → EReal} {x : ℝ} (hx : f x = ⊤) (h : ∃ (z : ℝ), x < z ∧ f z < ⊤) : rightDeriv f x = ⊥

To the right of dom f the right derivative is +∞ by fiat; to the left of it, -∞.

theorem Tdaf.ConvexAnalysis.leftDeriv_eq_top_of_eq_top {f : ℝ → EReal} {x : ℝ} (hx : f x = ⊤) (h : ∃ z < x, f z < ⊤) : leftDeriv f x = ⊤

To the left of dom f the left derivative is -∞ by fiat; to the right of it, +∞.

Monotonicity

theorem Tdaf.ConvexAnalysis.ConvexFn.lt_top_of_le_of_le {f : ℝ → EReal} {x : ℝ} (hf : ConvexFn f) {z₁ z₂ : ℝ} (h₁ : f z₁ < ⊤) (h₂ : f z₂ < ⊤) (hz₁ : z₁ ≤ x) (hz₂ : x ≤ z₂) : f x < ⊤

On the line, the effective domain of a convex function is an interval: a point between two points of dom f lies in dom f.

theorem Tdaf.ConvexAnalysis.leftDeriv_le_neg_dirDeriv (f : ℝ → EReal) (x : ℝ) : leftDeriv f x ≤ -dirDeriv f x (-1)

theorem Tdaf.ConvexAnalysis.dirDeriv_le_rightDeriv (f : ℝ → EReal) (x : ℝ) : dirDeriv f x 1 ≤ rightDeriv f x

theorem Tdaf.ConvexAnalysis.leftDeriv_le_rightDeriv {f : ℝ → EReal} (hf : ConvexFn f) (hp : Proper f) (x : ℝ) : leftDeriv f x ≤ rightDeriv f x

f'₋(x) ≤ f'₊(x) at every point of the line.

theorem Tdaf.ConvexAnalysis.dirDeriv_one_le_slope {f : ℝ → EReal} {y z p q : ℝ} (hyz : y < z) (hfy : f y = ↑p) (hfz : f z = ↑q) : dirDeriv f y 1 ≤ ↑((q - p) / (z - y))

The right derivative at the left end of an interval is at most the slope across it. This is one instance of the defining infimum, with the step z - y.

theorem Tdaf.ConvexAnalysis.dirDeriv_neg_one_le_slope {f : ℝ → EReal} {y z p q : ℝ} (hyz : y < z) (hfy : f y = ↑p) (hfz : f z = ↑q) : dirDeriv f z (-1) ≤ ↑((p - q) / (z - y))

The mirror image of dirDeriv_one_le_slope, at the right end of the interval.

theorem Tdaf.ConvexAnalysis.rightDeriv_le_leftDeriv {f : ℝ → EReal} (hp : Proper f) {y z : ℝ} (hyz : y < z) : rightDeriv f y ≤ leftDeriv f z

The step from one point to the next: f'₊(y) ≤ f'₋(z) whenever y < z. Together with f'₋ ≤ f'₊ this is the chain f'₊(z₁) ≤ f'₋(x) ≤ f'₊(x) ≤ f'₋(z₂) for z₁ < x < z₂, and it makes both functions nondecreasing. Convexity is not needed: dirDeriv is an infimum of difference quotients rather than a limit of them, so the two quotients across [y, z] bound it from above whatever f is. Only f'₋ ≤ f'₊ at a single point uses convexity.

theorem Tdaf.ConvexAnalysis.monotone_rightDeriv {f : ℝ → EReal} (hf : ConvexFn f) (hp : Proper f) : Monotone (rightDeriv f)

f'₊ is nondecreasing on the whole line.

theorem Tdaf.ConvexAnalysis.monotone_leftDeriv {f : ℝ → EReal} (hf : ConvexFn f) (hp : Proper f) : Monotone (leftDeriv f)

f'₋ is nondecreasing on the whole line.

Finiteness

theorem Tdaf.ConvexAnalysis.rightDeriv_lt_top_iff {f : ℝ → EReal} {x : ℝ} (hp : Proper f) : rightDeriv f x < ⊤ ↔ ∃ (z : ℝ), x < z ∧ f z < ⊤

f'₊(x) is < +∞ exactly when some point of dom f lies to the right of x — that is, exactly when x lies strictly to the left of the right endpoint of dom f.

theorem Tdaf.ConvexAnalysis.bot_lt_leftDeriv_iff {f : ℝ → EReal} {x : ℝ} (hp : Proper f) : ⊥ < leftDeriv f x ↔ ∃ z < x, f z < ⊤

f'₋(x) is > -∞ exactly when some point of dom f lies to the left of x.

theorem Tdaf.ConvexAnalysis.bot_lt_leftDeriv_and_rightDeriv_lt_top_iff {f : ℝ → EReal} {x : ℝ} (hf : ConvexFn f) (hp : Proper f) : ⊥ < leftDeriv f x ∧ rightDeriv f x < ⊤ ↔ x ∈ interior (dom f)

Both one-sided derivatives are finite exactly on the interior of dom f. The two halves are usually stated separately, as f'₊ < +∞ to the left of the right endpoint and f'₋ > -∞ to the right of the left endpoint; on the line those two conditions together are interiority.

theorem Tdaf.ConvexAnalysis.leftDeriv_finite_of_mem_interior_dom {f : ℝ → EReal} {x : ℝ} (hf : ConvexFn f) (hp : Proper f) (hx : x ∈ interior (dom f)) : leftDeriv f x ≠ ⊥ ∧ leftDeriv f x ≠ ⊤

Both one-sided derivatives are real at an interior point of dom f.

theorem Tdaf.ConvexAnalysis.rightDeriv_finite_of_mem_interior_dom {f : ℝ → EReal} {x : ℝ} (hf : ConvexFn f) (hp : Proper f) (hx : x ∈ interior (dom f)) : rightDeriv f x ≠ ⊥ ∧ rightDeriv f x ≠ ⊤

Both one-sided derivatives are real at an interior point of dom f.

The subdifferential on the line

theorem Tdaf.ConvexAnalysis.rightDeriv_eq_dirDeriv {f : ℝ → EReal} {x : ℝ} (hx : f x < ⊤) (hb : f x ≠ ⊥) : rightDeriv f x = dirDeriv f x 1

Where f is finite the guard in the definition of f'₊ is inert: the difference quotients already produce +∞ beyond the right end of dom f.

theorem Tdaf.ConvexAnalysis.leftDeriv_eq_neg_dirDeriv {f : ℝ → EReal} {x : ℝ} (hx : f x < ⊤) (hb : f x ≠ ⊥) : leftDeriv f x = -dirDeriv f x (-1)

The mirror image: where f is finite, f'₋(x) = -f'(x; -1) with no guard.

theorem Tdaf.ConvexAnalysis.mem_subgradient_iff_le_rightDeriv_of_lt_top {f : ℝ → EReal} {x : ℝ} (hx : f x < ⊤) (hb : f x ≠ ⊥) {y : ℝ} : y ∈ subgradient (innerₗ ℝ) f x ↔ leftDeriv f x ≤ ↑y ∧ ↑y ≤ rightDeriv f x

The subdifferential on the line is the interval between the one-sided derivatives:

∂f(x) = {x* ∈ ℝ | f'₋(x) ≤ x* ≤ f'₊(x)}.

This follows from the description of ∂f x by f'(x; ·): only the directions +1 and -1 carry information, because f'(x; ·) is positively homogeneous.

theorem Tdaf.ConvexAnalysis.lt_top_of_leftDeriv_le_of_le_rightDeriv {f : ℝ → EReal} {x : ℝ} (hp : Proper f) {y : ℝ} (h₁ : leftDeriv f x ≤ ↑y) (h₂ : ↑y ≤ rightDeriv f x) : f x < ⊤

A real number squeezed between the two one-sided derivatives forces x into dom f: outside dom f one of the two is ±∞ on the wrong side.

theorem Tdaf.ConvexAnalysis.mem_subgradient_iff_le_rightDeriv {f : ℝ → EReal} {x : ℝ} (hp : Proper f) {y : ℝ} : y ∈ subgradient (innerₗ ℝ) f x ↔ leftDeriv f x ≤ ↑y ∧ ↑y ≤ rightDeriv f x

The subdifferential on the line, with no hypothesis on x: outside dom f both sides are false.

One-sided limits of a monotone function

theorem Tdaf.ConvexAnalysis.tendsto_nhdsWithin_Ioi_of_monotone {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {g : α → β} (hg : Monotone g) (x : α) : Filter.Tendsto g (nhdsWithin x (Set.Ioi x)) (nhds (⨅ z ∈ Set.Ioi x, g z))

A monotone map into a complete linear order converges from the right, to the infimum of its values there.

theorem Tdaf.ConvexAnalysis.tendsto_nhdsWithin_Iio_of_monotone {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {g : α → β} (hg : Monotone g) (x : α) : Filter.Tendsto g (nhdsWithin x (Set.Iio x)) (nhds (⨆ z ∈ Set.Iio x, g z))

A monotone map into a complete linear order converges from the left, to the supremum of its values there.

The limit formulas

theorem Tdaf.ConvexAnalysis.le_coe_of_lt_rightDeriv {f : ℝ → EReal} {x : ℝ} (hf : ClosedProperConvexFn f) {y : ℝ} (hxy : x < y) {q : ℝ} (hq : f y = ↑q) {μ : ℝ} (hμ : ∀ (z : ℝ), x < z → ↑μ < rightDeriv f z) : f x ≤ ↑(q - μ * (y - x))

The estimate behind the right-hand limit formulas: if a real μ lies strictly below f'₊(z) for every z > x, then f x is bounded by the affine function of slope μ through (y, f y). Along the segment from y down to x, each interior point z has μ < f'₊(z) ≤ the slope from z to y, which bounds f z above; closedness lets the bound pass to the endpoint x.

theorem Tdaf.ConvexAnalysis.iInf_rightDeriv_Ioi {f : ℝ → EReal} (hf : ClosedProperConvexFn f) (x : ℝ) : ⨅ z ∈ Set.Ioi x, rightDeriv f z = rightDeriv f x

Right-continuity of f'₊. For a closed proper convex function on the line the right derivative is the limit of its own values from the right, in the monotone sense f'₊(x) = ⨅ {f'₊(z) | z > x}. Closedness cannot be dropped: for f equal to 1 at 0, to 0 on (0, ∞) and to ⊤ on (-∞, 0) — convex and proper, but not closed — f'₊ jumps at 0.

theorem Tdaf.ConvexAnalysis.le_coe_of_leftDeriv_lt {f : ℝ → EReal} {x : ℝ} (hf : ClosedProperConvexFn f) {y : ℝ} (hyx : y < x) {q : ℝ} (hq : f y = ↑q) {μ : ℝ} (hμ : ∀ z < x, leftDeriv f z < ↑μ) : f x ≤ ↑(q + μ * (x - y))

The estimate behind the left-hand limit formulas, the mirror image of le_coe_of_lt_rightDeriv.

theorem Tdaf.ConvexAnalysis.iSup_leftDeriv_Iio {f : ℝ → EReal} (hf : ClosedProperConvexFn f) (x : ℝ) : ⨆ z ∈ Set.Iio x, leftDeriv f z = leftDeriv f x

Left-continuity of f'₋: f'₋(x) = ⨆ {f'₋(z) | z < x} for a closed proper convex function on the line.

theorem Tdaf.ConvexAnalysis.iInf_leftDeriv_Ioi {f : ℝ → EReal} (hf : ClosedProperConvexFn f) (x : ℝ) : ⨅ z ∈ Set.Ioi x, leftDeriv f z = rightDeriv f x

The crossed limit formula: the left derivative also has f'₊(x) as its limit from the right.

theorem Tdaf.ConvexAnalysis.iSup_rightDeriv_Iio {f : ℝ → EReal} (hf : ClosedProperConvexFn f) (x : ℝ) : ⨆ z ∈ Set.Iio x, rightDeriv f z = leftDeriv f x

The crossed limit formula: the right derivative has f'₋(x) as its limit from the left.

The four limit formulas

theorem Tdaf.ConvexAnalysis.tendsto_rightDeriv_nhdsWithin_Ioi {f : ℝ → EReal} (hf : ClosedProperConvexFn f) (x : ℝ) : Filter.Tendsto (rightDeriv f) (nhdsWithin x (Set.Ioi x)) (nhds (rightDeriv f x))

lim_{z ↓ x} f'₊(z) = f'₊(x).

theorem Tdaf.ConvexAnalysis.tendsto_rightDeriv_nhdsWithin_Iio {f : ℝ → EReal} (hf : ClosedProperConvexFn f) (x : ℝ) : Filter.Tendsto (rightDeriv f) (nhdsWithin x (Set.Iio x)) (nhds (leftDeriv f x))

lim_{z ↑ x} f'₊(z) = f'₋(x).

theorem Tdaf.ConvexAnalysis.tendsto_leftDeriv_nhdsWithin_Ioi {f : ℝ → EReal} (hf : ClosedProperConvexFn f) (x : ℝ) : Filter.Tendsto (leftDeriv f) (nhdsWithin x (Set.Ioi x)) (nhds (rightDeriv f x))

lim_{z ↓ x} f'₋(z) = f'₊(x).

theorem Tdaf.ConvexAnalysis.tendsto_leftDeriv_nhdsWithin_Iio {f : ℝ → EReal} (hf : ClosedProperConvexFn f) (x : ℝ) : Filter.Tendsto (leftDeriv f) (nhdsWithin x (Set.Iio x)) (nhds (leftDeriv f x))

lim_{z ↑ x} f'₋(z) = f'₋(x).

A nondecreasing function between the two derivatives

theorem Tdaf.ConvexAnalysis.monotone_of_leftDeriv_le_of_le_rightDeriv {f : ℝ → EReal} (hp : Proper f) {φ : ℝ → EReal} (h₁ : ∀ (z : ℝ), leftDeriv f z ≤ φ z) (h₂ : ∀ (z : ℝ), φ z ≤ rightDeriv f z) : Monotone φ

Any φ squeezed between the two one-sided derivatives is nondecreasing — immediately from f'₊(y) ≤ f'₋(z) for y < z.

theorem Tdaf.ConvexAnalysis.iInf_Ioi_eq_rightDeriv {f : ℝ → EReal} (hf : ClosedProperConvexFn f) {φ : ℝ → EReal} (h₁ : ∀ (z : ℝ), leftDeriv f z ≤ φ z) (h₂ : ∀ (z : ℝ), φ z ≤ rightDeriv f z) (x : ℝ) : ⨅ z ∈ Set.Ioi x, φ z = rightDeriv f x

φ determines f'₊: any nondecreasing φ between f'₋ and f'₊ has f'₊ as its limit from the right.

theorem Tdaf.ConvexAnalysis.iSup_Iio_eq_leftDeriv {f : ℝ → EReal} (hf : ClosedProperConvexFn f) {φ : ℝ → EReal} (h₁ : ∀ (z : ℝ), leftDeriv f z ≤ φ z) (h₂ : ∀ (z : ℝ), φ z ≤ rightDeriv f z) (x : ℝ) : ⨆ z ∈ Set.Iio x, φ z = leftDeriv f x

φ determines f'₋: it has f'₋ as its limit from the left.

theorem Tdaf.ConvexAnalysis.subgradientRel_eq_of_deriv_eq {f g : ℝ → EReal} (hpf : Proper f) (hpg : Proper g) (hr : ∀ (x : ℝ), rightDeriv f x = rightDeriv g x) (hl : ∀ (x : ℝ), leftDeriv f x = leftDeriv g x) : subgradientRel (innerₗ ℝ) f = subgradientRel (innerₗ ℝ) g

Two proper functions on the line with the same one-sided derivatives have the same subdifferential — the subdifferential is the interval between them.

theorem Tdaf.ConvexAnalysis.exists_eq_add_coe_of_deriv_eq {f g : ℝ → EReal} (hf : ClosedProperConvexFn f) (hg : ClosedProperConvexFn g) (hr : ∀ (x : ℝ), rightDeriv f x = rightDeriv g x) (hl : ∀ (x : ℝ), leftDeriv f x = leftDeriv g x) : ∃ (α : ℝ), ∀ (x : ℝ), g x = f x + ↑α

Two closed proper convex functions on the line with the same one-sided derivatives differ by a constant.

theorem Tdaf.ConvexAnalysis.exists_eq_add_coe_of_le_le {f g : ℝ → EReal} (hf : ClosedProperConvexFn f) (hg : ClosedProperConvexFn g) {φ : ℝ → EReal} (hf₁ : ∀ (z : ℝ), leftDeriv f z ≤ φ z) (hf₂ : ∀ (z : ℝ), φ z ≤ rightDeriv f z) (hg₁ : ∀ (z : ℝ), leftDeriv g z ≤ φ z) (hg₂ : ∀ (z : ℝ), φ z ≤ rightDeriv g z) : ∃ (α : ℝ), ∀ (x : ℝ), g x = f x + ↑α

Uniqueness: a nondecreasing φ between the one-sided derivatives pins down a closed proper convex function on the line up to an additive constant.

Cycles as lists, and rotation

def Tdaf.ConvexAnalysis.cycleVal {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : List (E × F) → ℝ

The telescoping sum around the closed cycle through a list of pairs: chainVal with the head of the list as both the start and the free endpoint. The empty cycle has sum 0.

Equations

• Tdaf.ConvexAnalysis.cycleVal B [] = 0
• Tdaf.ConvexAnalysis.cycleVal B (p :: l) = Tdaf.ConvexAnalysis.chainVal B p l p.1

@[simp]

theorem Tdaf.ConvexAnalysis.cycleVal_nil {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} : cycleVal B [] = 0

@[simp]

theorem Tdaf.ConvexAnalysis.cycleVal_singleton {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (p : E × F) : cycleVal B [p] = 0

theorem Tdaf.ConvexAnalysis.isCyclicallyMonotone_iff_cycleVal {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (ρ : SetRel E F) : IsCyclicallyMonotone B ρ ↔ ∀ (L : List (E × F)), (∀ q ∈ L, q ∈ ρ) → cycleVal B L ≤ 0

Cyclic monotonicity in terms of cycleVal.

theorem Tdaf.ConvexAnalysis.cycleVal_cons {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (p : E × F) (l : List (E × F)) : cycleVal B (p :: l) = cycleVal B (l ++ [p])

A cycle may be rotated by one step without changing its sum: the last edge of the rotated cycle is the first edge of the original.

theorem Tdaf.ConvexAnalysis.cycleVal_append_comm {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (A C : List (E × F)) : cycleVal B (A ++ C) = cycleVal B (C ++ A)

A cycle may be rotated arbitrarily, in the form cycleVal (A ++ C) = cycleVal (C ++ A).

theorem Tdaf.ConvexAnalysis.exists_chainVal_eq_mem {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (l : List (E × F)) (s : E × F) : ∃ (r : E × F) (c : ℝ), r ∈ s :: l ∧ ∀ (x : E), chainVal B s l x = (B x) r.2 - c

A chain is affine in its free endpoint, with the slope realised by a pair of the chain. This sharpens exists_chainVal_eq, and it is what makes the last edge of a cycle land on a pair to which monotonicity applies.

theorem Tdaf.ConvexAnalysis.exists_cycleVal_cons_eq {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (p q : E × F) (l : List (E × F)) : ∃ r ∈ q :: l, cycleVal B (p :: q :: l) = cycleVal B (q :: l) + (B (q.1 - p.1)) (p.2 - r.2)

Deleting the head of a cycle changes the sum by one product. This is the induction step of the one-dimensional theorem: if the head dominates the rest of the cycle in both coordinates, the product is ≤ 0.

Monotone relations on the line

theorem Tdaf.ConvexAnalysis.innerₗ_real_apply (a b : ℝ) : ((innerₗ ℝ) a) b = a * b

The pairing of the line with itself is multiplication.

theorem Tdaf.ConvexAnalysis.exists_max_mem_of_ne_nil {α : Type u_1} (g : α → ℝ) (l : List α) : l ≠ [] → ∃ a ∈ l, ∀ b ∈ l, g b ≤ g a

A finite nonempty list attains the maximum of a real-valued function along the list.

theorem Tdaf.ConvexAnalysis.isMonotoneRel_iff_forall_le_or_le {ρ : SetRel ℝ ℝ} : IsMonotoneRel (innerₗ ℝ) ρ ↔ ∀ p ∈ ρ, ∀ q ∈ ρ, p ≤ q ∨ q ≤ p

On the line, monotonicity is total ordering: a mapping is monotone exactly when its graph is a chain for the coordinatewise order on ℝ × ℝ, that is, a non-decreasing curve.

theorem Tdaf.ConvexAnalysis.cycleVal_cons_le_cycleVal {M : ℝ × ℝ} {L : List (ℝ × ℝ)} (hdom : ∀ q ∈ L, q.1 ≤ M.1 ∧ q.2 ≤ M.2) : cycleVal (innerₗ ℝ) (M :: L) ≤ cycleVal (innerₗ ℝ) L

Deleting a dominating head of a cycle does not decrease its sum. On the line this is the whole content of the passage from monotonicity to cyclic monotonicity: the deleted edge runs backwards in the first coordinate and forwards in the second.

theorem Tdaf.ConvexAnalysis.IsMonotoneRel.isCyclicallyMonotone {ρ : SetRel ℝ ℝ} (h : IsMonotoneRel (innerₗ ℝ) ρ) : IsCyclicallyMonotone (innerₗ ℝ) ρ

On the line, monotone mappings are cyclically monotone. A cycle may be rotated so that the pair maximizing x + y comes first; monotonicity makes that pair dominate the whole cycle in both coordinates, so deleting it does not decrease the sum, and induction on the length finishes.

In higher dimensions this fails: cyclic monotonicity is strictly stronger.

theorem Tdaf.ConvexAnalysis.isMaximalMonotoneRel_iff_isMaximalCyclicallyMonotone {ρ : SetRel ℝ ℝ} : IsMaximalMonotoneRel (innerₗ ℝ) ρ ↔ IsMaximalCyclicallyMonotone (innerₗ ℝ) ρ

On the line the two maximality notions agree, since the two monotonicity notions do.

theorem Tdaf.ConvexAnalysis.isMaximalMonotoneRel_iff_exists_closedProperConvexFn {ρ : SetRel ℝ ℝ} : IsMaximalMonotoneRel (innerₗ ℝ) ρ ↔ ∃ (f : ℝ → EReal), ClosedProperConvexFn f ∧ ρ = subgradientRel (innerₗ ℝ) f

On the line the maximal monotone mappings — the maximal chains for the coordinatewise order, the complete non-decreasing curves — are exactly the subdifferentials of the closed proper convex functions. With mem_subgradientRel_iff, a complete non-decreasing curve is always the region f'₋(x) ≤ y ≤ f'₊(x) between two one-sided derivatives, and conversely.

theorem Tdaf.ConvexAnalysis.mem_subgradientRel_iff {f : ℝ → EReal} (hp : Proper f) {x y : ℝ} : (x, y) ∈ subgradientRel (innerₗ ℝ) f ↔ leftDeriv f x ≤ ↑y ∧ ↑y ≤ rightDeriv f x

The graph of the subdifferential of a proper convex function on the line is the region between the two one-sided derivatives.