theorem continuousOn_toReal_on_ri_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hg : ConvexOn ℝ (effectiveDomain Set.univ f) fun (x : Fin n → ℝ) => (f x).toReal) : ContinuousOn (fun (x : EuclideanSpace ℝ (Fin n)) => (f x.ofLp).toReal) (euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f))

theorem convexFunction_continuousOn_ri_effectiveDomain_of_proper {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : ContinuousOn (fun (x : EuclideanSpace ℝ (Fin n)) => f x.ofLp) (euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f))

theorem convexFunction_continuousOn_ri_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) : ContinuousOn (fun (x : EuclideanSpace ℝ (Fin n)) => f x.ofLp) (euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f))

Remark 7.0.24: A convex function is continuous relative to ri (dom f).

theorem tendsto_segment_to_y {n : ℕ} (x y : EuclideanSpace ℝ (Fin n)) : Filter.Tendsto (fun (t : ℝ) => (1 - t) • x + t • y) (nhds 1) (nhds y)

The segment map tends to its endpoint as t → 1.

theorem liminf_along_segment_ge_closure {n : ℕ} {f : (Fin n → ℝ) → EReal} {x y : EuclideanSpace ℝ (Fin n)} (hf : ProperConvexFunctionOn Set.univ f) : convexFunctionClosure f y.ofLp ≤ Filter.liminf (fun (t : ℝ) => f ((1 - t) • x.ofLp + t • y.ofLp)) (nhdsWithin 1 (Set.Iio 1))

Liminf along the segment bounds the closure from below.

theorem limsup_along_segment_le_beta {n : ℕ} {f : (Fin n → ℝ) → EReal} {x y : EuclideanSpace ℝ (Fin n)} (hx : x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f)) (hf : ProperConvexFunctionOn Set.univ f) {β : ℝ} (hβ : convexFunctionClosure f y.ofLp ≤ ↑β) : Filter.limsup (fun (t : ℝ) => f ((1 - t) • x.ofLp + t • y.ofLp)) (nhdsWithin 1 (Set.Iio 1)) ≤ ↑β

Upper bound for the limsup along a segment via the embedded epigraph.

theorem convexFunctionClosure_eq_limit_along_segment {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f)) : (ProperConvexFunctionOn Set.univ f → ∀ (y : EuclideanSpace ℝ (Fin n)), Filter.Tendsto (fun (t : ℝ) => f ((1 - t) • x.ofLp + t • y.ofLp)) (nhdsWithin 1 (Set.Iio 1)) (nhds (convexFunctionClosure f y.ofLp))) ∧ (ImproperConvexFunctionOn Set.univ f → ∀ y ∈ closure ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f), Filter.Tendsto (fun (t : ℝ) => f ((1 - t) • x.ofLp + t • y.ofLp)) (nhdsWithin 1 (Set.Iio 1)) (nhds (convexFunctionClosure f y.ofLp)))

Theorem 7.5. Let f be a proper convex function, and let x ∈ ri (dom f). Then (cl f)(y) = lim_{λ ↑ 1} f((1 - λ)x + λ y) for every y. (The formula is also valid when f is improper and y ∈ cl (dom f).)

theorem closedProperConvexFunction_eq_limit_along_segment {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfclosed : ClosedConvexFunction f) (hfproper : ProperConvexFunctionOn Set.univ f) {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f) (y : EuclideanSpace ℝ (Fin n)) : Filter.Tendsto (fun (t : ℝ) => f ((1 - t) • x.ofLp + t • y.ofLp)) (nhdsWithin 1 (Set.Iio 1)) (nhds (f y.ofLp))

Corollary 7.5.1. For a closed proper convex function f, one has f y = lim_{λ ↑ 1} f((1 - λ) x + λ y) for every x ∈ dom f and every y.