The effective domain of an extended-real convex function

For a function f : E → EReal with convex real epigraph, the effective domain {x | f x ≠ ⊤} is convex. If f never takes the value ⊥, its real representative x ↦ (f x).toReal is convex on that domain and agrees there with f by EReal.coe_toReal.

Main statements

• TauCeti.le_coe_of_convex_epigraph — the epigraph gives a convex-combination bound;
• TauCeti.convex_setOf_ne_top — the effective domain is convex;
• TauCeti.convexOn_toReal — the real representative is convex on the effective domain.

References

• R. T. Rockafellar, Convex Analysis, Princeton Mathematical Series 28, 1970, §4.

theorem TauCeti.le_coe_of_convex_epigraph {E : Type u_1} [AddCommMonoid E] [SMul ℝ E] {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) {x y : E} (hx : f x ≠ ⊤) (hy : f y ≠ ⊤) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : f (a • x + b • y) ≤ ↑(a * (f x).toReal + b * (f y).toReal)

A convex real epigraph bounds the value at a convex combination by the corresponding combination of the real representatives of its endpoint values.

theorem TauCeti.convex_setOf_ne_top {E : Type u_1} [AddCommMonoid E] [SMul ℝ E] {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) : Convex ℝ {x : E | f x ≠ ⊤}

The effective domain {x | f x ≠ ⊤} of a function with convex real epigraph is convex: it is closed under convex combinations.

theorem TauCeti.convexOn_toReal {E : Type u_1} [AddCommMonoid E] [SMul ℝ E] {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) : ConvexOn ℝ {x : E | f x ≠ ⊤} fun (x : E) => (f x).toReal

The real representative of a convex function. If f : E → EReal has convex real epigraph and never takes the value ⊥, then x ↦ (f x).toReal is convex on the effective domain {x | f x ≠ ⊤}, where it agrees with f by EReal.coe_toReal.