theorem ERealFunction.strict_convex_combination_eq_bot_of_isConvex {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] {f : H → EReal} (hf : IsConvex f) {x y : H} (hx : f x = ⊥) {a : ℝ} (ha : 0 < a) (ha_lt_one : a < 1) : f (a • x + (1 - a) • y) = ⊥

Helper for Proposition 9.6: Jensen convexity sends every strict convex combination with a -∞ endpoint to -∞.

theorem ERealFunction.tendsto_reciprocal_convex_combination_to_right {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (x y : H) : Filter.Tendsto (fun (n : ℕ) => (1 / (↑n + 2)) • x + (1 - 1 / (↑n + 2)) • y) Filter.atTop (nhds y)

Helper for Proposition 9.6: the reciprocal convex combinations converge to the right endpoint.

theorem ERealFunction.eq_bot_of_mem_gamma_of_eq_bot {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] {f : H → EReal} (hf : f ∈ Γ(H)) {x y : H} (hx : f x = ⊥) : f y = ⊥

Helper for Proposition 9.6: lower semicontinuity turns the constant -∞ values on the approaching segment into the endpoint value -∞.

theorem ERealFunction.eq_bot_or_eq_top_of_mem_gamma_of_eq_bot {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] {f : H → EReal} (hf : f ∈ Γ(H)) {x : H} (hx : f x = ⊥) (y : H) : f y = ⊥ ∨ f y = ⊤

Proposition 9.6: if a function in Γ(ℋ) takes the value -∞ at some point, then it is nowhere real-valued: every value is either -∞ or +∞.