A convex function of one variable is the integral of its derivative #

On an open interval where it is finite, a convex function is recovered from either of its one-sided derivatives by integration, f y - f x = ∫ₓʸ f'₊(t) dt = ∫ₓʸ f'₋(t) dt.

Main results #

sub_eq_intervalIntegral_derivWithin_Ioi — the statement for a real-valued convex function on an open convex subset of the line. This is the theorem; the rest is translation.
rightDeriv_eq_coe_derivWithin — at an interior point of dom f, the EReal-valued rightDeriv is the coercion of Mathlib's derivWithin f (Ioi t) t.
sub_eq_intervalIntegral_rightDeriv, sub_eq_intervalIntegral_leftDeriv — both halves for an EReal-valued f (Corollary 24.2.1 in [^1]).

Implementation notes #

The fundamental theorem of calculus applies unchanged: a convex function is continuous on the interior of its domain, has a right derivative at every interior point, and that derivative is nondecreasing, hence integrable on compacts. No a.e. differentiability is needed. rightDeriv f t is an infimum of difference quotients where Mathlib's right derivative is a limit; the two agree at interior points of dom f, which is why interiority rather than finiteness of f t is asked.

References #

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

The real-valued case #

source

theorem Tdaf.ConvexAnalysis.sub_eq_intervalIntegral_derivWithin_Ioi {S : Set ℝ} {g : ℝ → ℝ} {x y : ℝ} (hg : ConvexOn ℝ S g) (hS : IsOpen S) (hx : x ∈ S) (hy : y ∈ S) :

g y - g x = ∫ (t : ℝ) in x..y, derivWithin g (Set.Ioi t) t

A real-valued convex function on an open convex subset of the line is the integral of its right derivative. S is asked to be open and convex rather than a non-empty open interval; in ℝ these are the same.

The bridge to `rightDeriv` #

source

theorem Tdaf.ConvexAnalysis.sub_div_eq_coe_slope {f : ℝ → EReal} {t : ℝ} (hb : f t ≠ ⊥) (ht : f t ≠ ⊤) {z : ℝ} (hz : z ∈ dom f) (hzb : f z ≠ ⊥) :

(f (t + (z - t) • 1) - f t) / ↑(z - t) = ↑(slope (fun (w : ℝ) => (f w).toReal) t z)

A difference quotient of f in the direction 1, taken between two points where f is finite, is the coercion of Mathlib's slope. No order relation between the points is needed.

source

theorem Tdaf.ConvexAnalysis.rightDeriv_eq_coe_derivWithin {f : ℝ → EReal} {t : ℝ} (hf : ConvexFn f) (hp : Proper f) (ht : t ∈ interior (dom f)) :

rightDeriv f t = ↑(derivWithin (fun (z : ℝ) => (f z).toReal) (Set.Ioi t) t)

At an interior point of dom f, the EReal infimum of difference quotients rightDeriv f t is the coercion of Mathlib's derivWithin f (Ioi t) t. Both are the infimum of the slopes slope f t z over the z > t at which f is finite.