Convexity along a line

Restricting a function to a line through x in direction d — t ↦ f (x + t • d), on the set of steps that keep the point inside S — preserves convexity, and for convex S it detects it. The converse is what makes the reduction useful: it turns a statement about a function on a vector space into a statement about functions of one real variable, where the calculus of a single derivative applies. That is how the second-derivative criterion for convexity on ℝⁿ is proved from the one on an interval.

Main results

• convexOn_comp_line, concaveOn_comp_line — the restriction stays convex, resp. concave.
• convexOn_iff_lines, concaveOn_iff_lines — for convex S, the restrictions detect convexity.
• isOpen_line_steps — the step set is open when S is.
• continuousAt_comp_line_of_convexOn, …_of_concaveOn — continuity along a line through an interior point.

Implementation notes

The step set is written {t | x + t • d ∈ S} rather than as an interval: it is an interval only when S is convex, and the forward lemmas do not need that hypothesis.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §4.

The restriction to a line

theorem Tdaf.ConvexAnalysis.convexOn_comp_line {E : Type u_1} [AddCommGroup E] [Module ℝ E] {S : Set E} {f : E → ℝ} (hf : ConvexOn ℝ S f) (x d : E) : ConvexOn ℝ {t : ℝ | x + t • d ∈ S} fun (t : ℝ) => f (x + t • d)

A convex function stays convex along a line: t ↦ f (x + t • d) is convex on the set of steps that keep x + t • d inside S.

theorem Tdaf.ConvexAnalysis.concaveOn_comp_line {E : Type u_1} [AddCommGroup E] [Module ℝ E] {S : Set E} {f : E → ℝ} (hf : ConcaveOn ℝ S f) (x d : E) : ConcaveOn ℝ {t : ℝ | x + t • d ∈ S} fun (t : ℝ) => f (x + t • d)

A concave function stays concave along a line. This is convexOn_comp_line for -f.

theorem Tdaf.ConvexAnalysis.convexOn_iff_lines {E : Type u_1} [AddCommGroup E] [Module ℝ E] {S : Set E} {f : E → ℝ} (hS : Convex ℝ S) : ConvexOn ℝ S f ↔ ∀ (x d : E), ConvexOn ℝ {t : ℝ | x + t • d ∈ S} fun (t : ℝ) => f (x + t • d)

The restrictions to lines detect convexity. For convex S, f is convex on S exactly when every line restriction is convex on its step set. Given x, y ∈ S, the line through x in direction y - x carries the convexity inequality for that pair, with steps 0 and 1.

theorem Tdaf.ConvexAnalysis.concaveOn_iff_lines {E : Type u_1} [AddCommGroup E] [Module ℝ E] {S : Set E} {f : E → ℝ} (hS : Convex ℝ S) : ConcaveOn ℝ S f ↔ ∀ (x d : E), ConcaveOn ℝ {t : ℝ | x + t • d ∈ S} fun (t : ℝ) => f (x + t • d)

The concave form of convexOn_iff_lines.

Topology along a line

theorem Tdaf.ConvexAnalysis.isOpen_line_steps {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {S : Set E} (hS : IsOpen S) (x d : E) : IsOpen {t : ℝ | x + t • d ∈ S}

The steps t with x + t • d ∈ S form an open set when S is open.

theorem Tdaf.ConvexAnalysis.continuousAt_comp_line_of_convexOn {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {S : Set E} {f : E → ℝ} {x : E} (hS : IsOpen S) (hf : ConvexOn ℝ S f) (hx : x ∈ S) (d : E) : ContinuousAt (fun (t : ℝ) => f (x + t • d)) 0

A convex function is continuous along a line through an interior point of the set on which it is convex: this is the one-dimensional case of ConvexOn.continuousOn.

theorem Tdaf.ConvexAnalysis.continuousAt_comp_line_of_concaveOn {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {S : Set E} {f : E → ℝ} {x : E} (hS : IsOpen S) (hf : ConcaveOn ℝ S f) (hx : x ∈ S) (d : E) : ContinuousAt (fun (t : ℝ) => f (x + t • d)) 0

A concave function is continuous along a line through an interior point.