theorem ereal_mul_ne_bot_of_pos {a : EReal} {r : ℝ} (hr : 0 < r) (ha : a ≠ ⊥) : ↑r * a ≠ ⊥

Multiplying a non-⊥ value by a positive real does not yield ⊥ in EReal.

theorem segment_inequality_f_univ {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) (hnotbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (x y : Fin n → ℝ) (t : ℝ) : 0 < t → t < 1 → f ((1 - t) • x + t • y) ≤ ↑(1 - t) * f x + ↑t * f y

Segment inequality for a convex function on Set.univ with no ⊥ values.

theorem segment_inequality_phi_real {phi : EReal → EReal} (hphi : ConvexFunctionOn Set.univ fun (x : Fin 1 → ℝ) => phi ↑(x 0)) (hphi_notbot : ∀ (r : ℝ), phi ↑r ≠ ⊥) (a b t : ℝ) : 0 < t → t < 1 → phi ↑((1 - t) * a + t * b) ≤ ↑(1 - t) * phi ↑a + ↑t * phi ↑b

Segment inequality for phi on real arguments from convexity on Fin 1.

theorem convexFunctionOn_comp_nondecreasing {n : ℕ} {f : (Fin n → ℝ) → EReal} {phi : EReal → EReal} (hf : ConvexFunctionOn Set.univ f) (hf_notbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (hphi : ConvexFunctionOn Set.univ fun (x : Fin 1 → ℝ) => phi ↑(x 0)) (hphi_notbot : ∀ (r : ℝ), phi ↑r ≠ ⊥) (hphi_top : phi ⊤ = ⊤) (hmono : Monotone phi) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => phi (f x)

Theorem 5.1: Let f be a convex function from R^n to (-infty, +infty], and let phi be a convex function from R to (-infty, +infty] which is non-decreasing (with phi (+infty) = +infty). Then h x = phi (f x) is convex on R^n.

noncomputable def expEReal (z : EReal) : EReal

Extended-real exponential with expEReal ⊤ = ⊤ and expEReal ⊥ = 0.

Equations

• expEReal z = if z = ⊥ then ↑0 else if z = ⊤ then ⊤ else ↑(Real.exp z.toReal)

@[simp]

theorem expEReal_coe (r : ℝ) : expEReal ↑r = ↑(Real.exp r)

On real inputs, expEReal agrees with Real.exp.

theorem expEReal_monotone : Monotone expEReal

expEReal is monotone on EReal.

theorem convexFunctionOn_expEReal_univ : ConvexFunctionOn Set.univ fun (x : Fin 1 → ℝ) => expEReal ↑(x 0)

Convexity of expEReal on Fin 1 over Set.univ.

theorem properConvexFunctionOn_exp {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(Real.exp (f x))

Text 5.1.1: The function h x = exp (f x) is a proper convex function on R^n if f is a proper convex function.

theorem convexOn_max_zero : ConvexOn ℝ Set.univ fun (r : ℝ) => max r 0

The function r ↦ max r 0 is convex on ℝ.

theorem convexOn_rpow_max_zero {p : ℝ} (hp1 : 1 ≤ p) : ConvexOn ℝ Set.univ fun (r : ℝ) => (max r 0).rpow p

Convexity of r ↦ (max r 0) ^ p on ℝ for p ≥ 1.

theorem monotone_rpow_max_zero {p : ℝ} (hp0 : 0 ≤ p) : Monotone fun (r : ℝ) => (max r 0).rpow p

The map r ↦ (max r 0) ^ p is monotone for p ≥ 0.

theorem convexFunctionOn_rpow_of_convex_nonneg {n : ℕ} {f : (Fin n → ℝ) → ℝ} {p : ℝ} (hp : 1 < p) (hf : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) (h_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑((f x).rpow p)

Text 5.1.2: The function h x = f x ^ p is convex for p > 1 when f is convex and non-negative.

theorem convexOn_univ_euclidean_norm_rpow {n : ℕ} {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ Set.univ fun (x : EuclideanSpace ℝ (Fin n)) => ‖x‖.rpow p

Text 5.1.3: In particular, h(x) = |x|^p is convex on R^n for p ≥ 1 (|x| being the Euclidean norm).

Helper lemmas for Text 5.1.4.

theorem convex_pos_set_of_concave {n : ℕ} {g : (Fin n → ℝ) → ℝ} (hg : ConcaveOn ℝ Set.univ g) : Convex ℝ {x : Fin n → ℝ | 0 < g x}

Positivity domain of a concave function on Set.univ is convex.

theorem convexOn_inv_Ioi : ConvexOn ℝ (Set.Ioi 0) fun (r : ℝ) => r⁻¹

The reciprocal function is convex on (0, +∞).

theorem convexOn_inv_of_concave_pos {n : ℕ} {g : (Fin n → ℝ) → ℝ} (hg : ConcaveOn ℝ Set.univ g) : ConvexOn ℝ {x : Fin n → ℝ | 0 < g x} fun (x : Fin n → ℝ) => (g x)⁻¹

Text 5.1.4: If g is a concave function, then h x = 1 / g x is convex on C = {x | g x > 0}.

theorem segment_inequality_real_of_ereal {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) (x y : Fin n → ℝ) (t : ℝ) : 0 < t → t < 1 → f ((1 - t) • x + t • y) ≤ (1 - t) * f x + t * f y

Segment inequality on ℝ obtained from convexity of the EReal coercion.

theorem affine_le_affine_combo {a b c t lam alpha : ℝ} (hlam : 0 ≤ lam) (h : a ≤ (1 - t) * b + t * c) : lam * a + alpha ≤ (1 - t) * (lam * b + alpha) + t * (lam * c + alpha)

A nonnegative affine map preserves convex-combination inequalities on ℝ.

theorem properConvexFunctionOn_mul_add_const {n : ℕ} {f : (Fin n → ℝ) → ℝ} {lam alpha : ℝ} (hlam : 0 ≤ lam) (hf : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(lam * f x + alpha)

Text 5.1.5: (lambda f + alpha) is a proper convex function when f is a proper convex function and lambda and alpha are real numbers with lambda ≥ 0.

Helper lemmas for Theorem 5.2.

theorem add_ne_bot_of_notbot {a b : EReal} (ha : a ≠ ⊥) (hb : b ≠ ⊥) : a + b ≠ ⊥

The sum of two non-⊥ values in EReal is non-⊥.

theorem segment_inequality_add_univ {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ConvexFunctionOn Set.univ f1) (hf2 : ConvexFunctionOn Set.univ f2) (hnotbot1 : ∀ (x : Fin n → ℝ), f1 x ≠ ⊥) (hnotbot2 : ∀ (x : Fin n → ℝ), f2 x ≠ ⊥) (x y : Fin n → ℝ) (t : ℝ) : 0 < t → t < 1 → f1 ((1 - t) • x + t • y) + f2 ((1 - t) • x + t • y) ≤ ↑(1 - t) * (f1 x + f2 x) + ↑t * (f1 y + f2 y)

Segment inequality for the sum of convex functions on Set.univ.

theorem convexFunctionOn_add_of_proper {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (hf1 : ProperConvexFunctionOn Set.univ f1) (hf2 : ProperConvexFunctionOn Set.univ f2) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => f1 x + f2 x

Theorem 5.2: If f1 and f2 are proper convex functions on R^n, then f1 + f2 is convex.

theorem convexFunctionOn_linearCombination_of_proper {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} {lam : Fin m → ℝ} (hlam : ∀ (i : Fin m), 0 ≤ lam i) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ∑ i : Fin m, ↑(lam i) * f i x

Text 5.2.1: A linear combination lambda_1 f_1 + ... + lambda_m f_m of proper convex functions with non-negative coefficients is convex.

theorem add_indicatorFunction_eq {n : ℕ} {f : (Fin n → ℝ) → ℝ} {C : Set (Fin n → ℝ)} (x : Fin n → ℝ) : ↑(f x) + indicatorFunction C x = if x ∈ C then ↑(f x) else ⊤

Text 5.2.2: If f is a finite convex function and C is a nonempty convex set, then f x + δ(x | C) = f x for x ∈ C and f x + δ(x | C) = +∞ for x ∉ C, where δ(· | C) is the indicator function of C.