def ERealFunction.erealOpenInterval (α β : EReal) : Set ℝ

The open real interval cut out by the extended-real endpoints α and β.

@[simp]

theorem ERealFunction.mem_erealOpenInterval_iff {α β : EReal} {x : ℝ} : x ∈ erealOpenInterval α β ↔ α < ↑x ∧ ↑x < β

A real number lies in erealOpenInterval α β exactly when its EReal coercion lies strictly between α and β.

noncomputable def ERealFunction.oneSidedLimitExtensionEReal (g : ℝ → ↑(Set.Ioi ⊥)) (α β : EReal) : ℝ → EReal

The one-sided-limit extension of a function with domain ]α,β[: it agrees with g on the open interval, takes the right and left Filter.liminf values at finite endpoints, and is +∞ elsewhere.

@[simp]

theorem ERealFunction.oneSidedLimitExtensionEReal_apply_of_mem_erealOpenInterval (g : ℝ → ↑(Set.Ioi ⊥)) (α β : EReal) {x : ℝ} (hx : x ∈ erealOpenInterval α β) : oneSidedLimitExtensionEReal g α β x = ↑(g x)

On ]α,β[, the one-sided-limit extension agrees with g.

theorem ERealFunction.oneSidedLimitExtensionEReal_ne_bot (g : ℝ → ↑(Set.Ioi ⊥)) (α β : EReal) (hαlim : ∀ ⦃x : ℝ⦄, α = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Ioi x))) (hβlim : ∀ ⦃x : ℝ⦄, β = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Iio x))) (x : ℝ) : ⊥ < oneSidedLimitExtensionEReal g α β x

If the one-sided boundary liminf values stay above -∞, then the one-sided-limit extension is everywhere ]-∞,+∞]-valued.

noncomputable def ERealFunction.oneSidedLimitExtension (g : ℝ → ↑(Set.Ioi ⊥)) (α β : EReal) (hαlim : ∀ ⦃x : ℝ⦄, α = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Ioi x))) (hβlim : ∀ ⦃x : ℝ⦄, β = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Iio x))) : ℝ → ↑(Set.Ioi ⊥)

The subtype-valued one-sided-limit extension associated with oneSidedLimitExtensionEReal.

@[simp]

theorem ERealFunction.oneSidedLimitExtension_coe (g : ℝ → ↑(Set.Ioi ⊥)) (α β : EReal) (hαlim : ∀ ⦃x : ℝ⦄, α = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Ioi x))) (hβlim : ∀ ⦃x : ℝ⦄, β = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Iio x))) (x : ℝ) : ↑(oneSidedLimitExtension g α β hαlim hβlim x) = oneSidedLimitExtensionEReal g α β x

Coercing the subtype-valued one-sided-limit extension to EReal recovers the explicit piecewise extension formula.

theorem ERealFunction.oneSidedLimitExtension_mem_gammaZero (g : ℝ → ↑(Set.Ioi ⊥)) (α β : EReal) (hαβ : α < β) (hdom : effectiveDomain g = erealOpenInterval α β) (hstrict : StrictlyConvex g) (hαlim : ∀ ⦃x : ℝ⦄, α = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Ioi x))) (hβlim : ∀ ⦃x : ℝ⦄, β = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Iio x))) : oneSidedLimitExtension g α β hαlim hβlim ∈ Γ₀(ℝ)

The one-sided-limit extension from Proposition 9.34 belongs to Γ₀(ℝ).

theorem ERealFunction.oneSidedLimitExtensionEReal_eq_lowerSemicontinuousEnvelope (g : ℝ → ↑(Set.Ioi ⊥)) (α β : EReal) (hαβ : α < β) (hdom : effectiveDomain g = erealOpenInterval α β) (hstrict : StrictlyConvex g) (hαlim : ∀ ⦃x : ℝ⦄, α = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Ioi x))) (hβlim : ∀ ⦃x : ℝ⦄, β = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Iio x))) : oneSidedLimitExtensionEReal g α β = lowerSemicontinuousEnvelope fun (x : ℝ) => ↑(g x)

The one-sided-limit extension coincides with the lower semicontinuous hull of g.

theorem ERealFunction.oneSidedLimitExtension_strictlyConvex (g : ℝ → ↑(Set.Ioi ⊥)) (α β : EReal) (hαβ : α < β) (hdom : effectiveDomain g = erealOpenInterval α β) (hstrict : StrictlyConvex g) (hαlim : ∀ ⦃x : ℝ⦄, α = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Ioi x))) (hβlim : ∀ ⦃x : ℝ⦄, β = ↑x → ⊥ < Filter.liminf (fun (y : ℝ) => ↑(g y)) (nhdsWithin x (Set.Iio x))) : StrictlyConvex (oneSidedLimitExtension g α β hαlim hβlim)

Proposition 9.34: the one-sided-limit extension of a proper strictly convex function on ]\alpha,\beta[ is strictly convex.