Continuous midpoint-convex functions are convex

A function f is midpoint convex on a set s when f (midpoint ℝ x y) ≤ (f x + f y) / 2 for all x, y ∈ s. Jensen's theorem says that on a convex set a continuous midpoint-convex function is convex. This is how convexity is usually checked when only a two-point inequality at midpoints is available, as in the Bruhat--Tits form of nonpositive curvature in metric geometry.

Main results

• TauCeti.le_chord_of_midpoint — on [0, 1], a continuous midpoint-convex real function lies below the chord joining its values at 0 and 1.
• TauCeti.convexOn_of_midpoint — on a convex subset of a real topological vector space, a continuous midpoint-convex function is convex.

References

• J. L. W. V. Jensen, Sur les fonctions convexes et les inégalités entre les valeurs moyennes, Acta Math. 30 (1906), 175--193.

theorem TauCeti.le_chord_of_midpoint {g : ℝ → ℝ} (hg : ContinuousOn g (Set.Icc 0 1)) (h : ∀ s ∈ Set.Icc 0 1, ∀ t ∈ Set.Icc 0 1, g (midpoint ℝ s t) ≤ (g s + g t) / 2) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : g t ≤ (1 - t) * g 0 + t * g 1

On [0, 1], a continuous midpoint-convex function lies below its chord: its value at t is at most (1 - t) * g 0 + t * g 1.

theorem TauCeti.convexOn_of_midpoint {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} {f : E → ℝ} (hs : Convex ℝ s) (hf : ContinuousOn f s) (h : ∀ x ∈ s, ∀ y ∈ s, f (midpoint ℝ x y) ≤ (f x + f y) / 2) : ConvexOn ℝ s f

Jensen's theorem. On a convex subset of a real topological vector space, a continuous function that is midpoint convex is convex.