theorem bddAbove_sublevel_real_of_mono_convex_strict_nonneg {g : EReal → EReal} (hg_mono : Monotone g) (hg_conv : ConvexFunctionOn {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0)) (hstrict : ∃ (s : ℝ), 0 < s ∧ g 0 < g ↑s) {αr : ℝ} (hα0 : g 0 < ↑αr) : BddAbove {s : ℝ | 0 ≤ s ∧ g ↑s ≤ ↑αr}

theorem exists_pos_mem_sublevel_real_of_convex_finite_at_pos {g : EReal → EReal} (hg_conv : ConvexFunctionOn {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0)) (hζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) {αr : ℝ} (hα0 : g 0 < ↑αr) : ∃ (s : ℝ), 0 < s ∧ g ↑s ≤ ↑αr

There is a positive real in the cutoff sublevel once g is finite at some positive point.

theorem comp_closedGauge_gives_gaugeLikeClosedProperConvex {n : ℕ} {k : (Fin n → ℝ) → EReal} {g : EReal → EReal} (hk : IsClosedGauge k) (hg_mono : Monotone g) (hg_conv : ConvexFunctionOn {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0)) (hg_closed : IsClosed (epigraph {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0))) (hg_top : g ⊤ = ⊤) (hζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) (hstrict : ∃ (s : ℝ), 0 < s ∧ g 0 < g ↑s) : IsGaugeLikeClosedProperConvex fun (x : Fin n → ℝ) => g (k x)

A composition with a closed gauge is gauge-like closed proper convex under the hypotheses.

theorem gaugeLikeClosedProperConvex_iff_exists_closedGauge_comp {n : ℕ} (f : (Fin n → ℝ) → EReal) : IsGaugeLikeClosedProperConvex f ↔ ∃ (k : (Fin n → ℝ) → EReal) (g : EReal → EReal), IsClosedGauge k ∧ (∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) ∧ (∃ (s : ℝ), 0 < s ∧ g 0 < g ↑s) ∧ Monotone g ∧ (ConvexFunctionOn {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0)) ∧ IsClosed (epigraph {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => g ↑(t 0)) ∧ g ⊤ = ⊤ ∧ f = fun (x : Fin n → ℝ) => g (k x)

Theorem 15.3: A function f is a gauge-like closed proper convex function if and only if it can be expressed as f(x) = g (k x), where k is a closed gauge and g : [0, +∞] → (-∞, +∞] is a non-decreasing, lower semicontinuous convex function which strictly increases at some positive point and satisfies g(ζ) finite for some ζ > 0 (with the convention g(+∞) = +∞).

theorem fenchelConjugate_eq_monotoneConjugate_polarGauge_of_comp_formula {n : ℕ} {f k : (Fin n → ℝ) → EReal} {g : EReal → EReal} (hk : IsClosedGauge k) (hfg : f = fun (x : Fin n → ℝ) => g (k x)) (hg_mono : Monotone g) (hg_top : g ⊤ = ⊤) (hζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) (xStar : Fin n → ℝ) : fenchelConjugate n f xStar = monotoneConjugateERealNonneg g (polarGauge k xStar)

Formula part of Theorem 15.3 for the conjugate of g ∘ k.