theorem effectiveDomain_convex {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn S f) : Convex ℝ (effectiveDomain S f)

Prop 4.4.1: The effective domain of a convex function is a convex set in ℝ^n.

theorem effectiveDomain_subset {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : effectiveDomain S f ⊆ S

The effective domain is contained in the original set.

theorem epigraph_effectiveDomain_eq {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : epigraph (effectiveDomain S f) f = epigraph S f

The epigraph is unchanged by restricting to the effective domain.

theorem convexFunctionOn_iff_convexFunctionOn_effectiveDomain {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : ConvexFunctionOn S f ↔ ConvexFunctionOn (effectiveDomain S f) f

Prop 4.4.2: Trivially, the convexity of f is equivalent to that of the restriction of f to dom f (the effective domain). All the interest really centers on this restriction, and S has little role of its own.

theorem not_top_le_coe (r : ℝ) : ¬⊤ ≤ ↑r

The inequality ⊤ ≤ (r : EReal) never holds for real r.

theorem convexFunctionOn_const_top {n : ℕ} (C : Set (Fin n → ℝ)) : ConvexFunctionOn C fun (x : Fin n → ℝ) => ⊤

The constant ⊤ function is convex on any set.

theorem effectiveDomain_const_top {n : ℕ} (C : Set (Fin n → ℝ)) : (effectiveDomain C fun (x : Fin n → ℝ) => ⊤) = ∅

The effective domain of the constant ⊤ function is empty.

theorem fixedEffectiveDomain_restriction_not_preferred {n : ℕ} (C : Set (Fin n → ℝ)) (hC : C.Nonempty) : ¬∀ (f : (Fin n → ℝ) → EReal), ConvexFunctionOn C f → effectiveDomain C f = C

Remark 4.4.5: There are weighty reasons, soon apparent, why one does not want to consider merely the class of all convex functions having a fixed set C as their common effective domain.

def ERealForbiddenSum (a b : EReal) : Prop

Defintion 4.4.6: The forbidden sums are ⊤ + ⊥ (that is, ⊤ - ⊤) and ⊥ + ⊤ in the extended real line.

Equations

• ERealForbiddenSum a b = (a = ⊤ ∧ b = ⊥ ∨ a = ⊥ ∧ b = ⊤)

def ERealArithmeticConventions : Prop

Defintion 4.4.6: Conventions for arithmetic on EReal include α + ⊤ = ⊤ + α = ⊤ for ⊥ < α, α - ⊤ = ⊥ + α = ⊥ for α < ⊤, rules for multiplication by ⊤ or ⊥ depending on the sign of α, the identities 0 * ⊤ = ⊤ * 0 = 0 = 0 * ⊥ = ⊥ * 0, -⊥ = ⊤, and sInf ∅ = ⊤, sSup ∅ = ⊥.

Equations

• One or more equations did not get rendered due to their size.

theorem ereal_forbiddenSum_neg_iff {a b : EReal} : ERealForbiddenSum (-a) (-b) ↔ ERealForbiddenSum a b

Negating both arguments preserves the forbidden-sum condition.

theorem ereal_no_forbidden_neg_add {a b : EReal} (h : ¬ERealForbiddenSum a b) : (a ≠ ⊥ ∨ b ≠ ⊤) ∧ (a ≠ ⊤ ∨ b ≠ ⊥)

Disjunctions needed to apply EReal.neg_add from a non-forbidden sum.

theorem ereal_top_mul_add_of_no_forbidden {x1 x2 : EReal} (h : ¬ERealForbiddenSum (⊤ * x1) (⊤ * x2)) : ⊤ * (x1 + x2) = ⊤ * x1 + ⊤ * x2

Left distributivity for multiplication by ⊤ under a non-forbidden sum.