def LowerSemicontinuousAtSeq {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) (f : ↑S → EReal) (x : ↑S) : Prop

Text 7.0.1: Let f : S → [-∞, +∞] with S ⊆ R^n and x ∈ S. Then f is lower semicontinuous at x if for every sequence x_i ⊂ S with x_i → x, f x ≤ liminf (fun i => f (x_i)). Equivalently, f x ≤ liminf_{y → x} f y.

Equations

• LowerSemicontinuousAtSeq S f x = ∀ (u : ℕ → ↑S), Filter.Tendsto (fun (i : ℕ) => ↑(u i)) Filter.atTop (nhds ↑x) → f x ≤ Filter.liminf (fun (i : ℕ) => f (u i)) Filter.atTop

theorem exists_seq_tendsto_of_frequently {n : ℕ} {S : Set (EuclideanSpace ℝ (Fin n))} {x : ↑S} {s : Set ↑S} (h : ∃ᶠ (z : ↑S) in nhds x, z ∈ s) : ∃ (u : ℕ → ↑S), (∀ (n_1 : ℕ), u n_1 ∈ s) ∧ Filter.Tendsto (fun (i : ℕ) => ↑(u i)) Filter.atTop (nhds ↑x)

A frequently occurring subset near x yields a sequence in that subset converging to x.

theorem lowerSemicontinuousAtSeq_of_lowerSemicontinuousAt {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) (f : ↑S → EReal) (x : ↑S) : LowerSemicontinuousAt f x → LowerSemicontinuousAtSeq S f x

Lower semicontinuity implies the sequential liminf inequality.

theorem lowerSemicontinuousAt_of_lowerSemicontinuousAtSeq {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) (f : ↑S → EReal) (x : ↑S) : LowerSemicontinuousAtSeq S f x → LowerSemicontinuousAt f x

Sequential lower semicontinuity implies filter lower semicontinuity.

theorem lowerSemicontinuousAtSeq_iff_lowerSemicontinuousAt {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) (f : ↑S → EReal) (x : ↑S) : LowerSemicontinuousAtSeq S f x ↔ LowerSemicontinuousAt f x

The sequential definition agrees with mathlib's LowerSemicontinuousAt on the subtype.

def UpperSemicontinuousAtSeq {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) (f : ↑S → EReal) (x : ↑S) : Prop

Text 7.0.2: With f, S, x as above, f is upper semicontinuous at x if for every sequence x_i ⊂ S with x_i → x, f x ≥ limsup (fun i => f (x_i)). Equivalently, f x ≥ limsup_{y → x} f y.

Equations

• UpperSemicontinuousAtSeq S f x = ∀ (u : ℕ → ↑S), Filter.Tendsto (fun (i : ℕ) => ↑(u i)) Filter.atTop (nhds ↑x) → f x ≥ Filter.limsup (fun (i : ℕ) => f (u i)) Filter.atTop

theorem upperSemicontinuousAtSeq_of_upperSemicontinuousAt {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) (f : ↑S → EReal) (x : ↑S) : UpperSemicontinuousAt f x → UpperSemicontinuousAtSeq S f x

Upper semicontinuity implies the sequential limsup inequality.

theorem upperSemicontinuousAt_of_upperSemicontinuousAtSeq {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) (f : ↑S → EReal) (x : ↑S) : UpperSemicontinuousAtSeq S f x → UpperSemicontinuousAt f x

Sequential upper semicontinuity implies filter upper semicontinuity.

theorem upperSemicontinuousAtSeq_iff_upperSemicontinuousAt {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) (f : ↑S → EReal) (x : ↑S) : UpperSemicontinuousAtSeq S f x ↔ UpperSemicontinuousAt f x

The sequential definition agrees with mathlib's UpperSemicontinuousAt on the subtype.

theorem upperSemicontinuousAtSeq_iff_limsup_nhds {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) (f : ↑S → EReal) (x : ↑S) : UpperSemicontinuousAtSeq S f x ↔ f x ≥ Filter.limsup (fun (y : ↑S) => f y) (nhds x)

Lemma 7.0.3. Let S be a subset of R^n, f : S → [-infty, +infty], and x in S. The following are equivalent: (i) for every sequence x_i in S with x_i -> x, f x >= limsup (fun i => f (x_i)); (ii) f x >= limsup_{y -> x} f y, where limsup_{y -> x} f y := lim_{epsilon -> 0} sup { f y | y in S, |y - x| < epsilon }.

theorem exists_real_not_le_of_ne_bot {x : EReal} (hx : x ≠ ⊥) : ∃ (α : ℝ), ¬x ≤ ↑α

A non-bottom EReal exceeds some real number.

theorem isClosed_sublevel_bot_of_closed_sublevels {n : ℕ} {f : (Fin n → ℝ) → EReal} (h : ∀ (α : ℝ), IsClosed {x : Fin n → ℝ | f x ≤ ↑α}) : IsClosed {x : Fin n → ℝ | f x ≤ ⊥}

Real sublevel sets control the bottom sublevel set.

theorem lowerSemicontinuous_iff_closed_sublevel {n : ℕ} (f : (Fin n → ℝ) → EReal) : LowerSemicontinuous f ↔ ∀ (α : ℝ), IsClosed {x : Fin n → ℝ | f x ≤ ↑α}

Lower semicontinuity is equivalent to closed real sublevel sets.

theorem closed_sublevel_of_closed_epigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (h : IsClosed (epigraph Set.univ f)) (α : ℝ) : IsClosed {x : Fin n → ℝ | f x ≤ ↑α}

Closedness of the epigraph implies closedness of every real sublevel set.

theorem closed_epigraph_of_closed_sublevel {n : ℕ} {f : (Fin n → ℝ) → EReal} (h : ∀ (α : ℝ), IsClosed {x : Fin n → ℝ | f x ≤ ↑α}) : IsClosed (epigraph Set.univ f)

Closed real sublevel sets imply closedness of the epigraph.

theorem lowerSemicontinuous_iff_closed_sublevel_iff_closed_epigraph {n : ℕ} (f : (Fin n → ℝ) → EReal) : (LowerSemicontinuous f ↔ ∀ (α : ℝ), IsClosed {x : Fin n → ℝ | f x ≤ ↑α}) ∧ ((∀ (α : ℝ), IsClosed {x : Fin n → ℝ | f x ≤ ↑α}) ↔ IsClosed (epigraph Set.univ f))

Theorem 7.1. Let f : ℝ^n → [-∞, +∞]. The following are equivalent: (a) f is lower semicontinuous on ℝ^n; (b) {x | f x ≤ α} is closed for every α ∈ ℝ; (c) the epigraph of f is closed in ℝ^{n+1}.

theorem lscHull_candidate_lsc {n : ℕ} (f : (Fin n → ℝ) → EReal) : LowerSemicontinuous fun (x : Fin n → ℝ) => ⨆ (h : { h : (Fin n → ℝ) → EReal // LowerSemicontinuous h ∧ h ≤ f }), ↑h x

Text 7.0.4: Given any function f on ℝ^n, there exists a greatest lower semicontinuous function majorized by f; this function is called the lower semicontinuous hull of f. The pointwise supremum of lower semicontinuous minorants of f is lower semicontinuous.

theorem lscHull_candidate_le {n : ℕ} (f : (Fin n → ℝ) → EReal) : (fun (x : Fin n → ℝ) => ⨆ (h : { h : (Fin n → ℝ) → EReal // LowerSemicontinuous h ∧ h ≤ f }), ↑h x) ≤ f

The pointwise supremum of lower semicontinuous minorants of f lies below f.

theorem lscHull_candidate_max {n : ℕ} {f h : (Fin n → ℝ) → EReal} (hh : LowerSemicontinuous h) (hle : h ≤ f) : h ≤ fun (x : Fin n → ℝ) => ⨆ (h' : { h : (Fin n → ℝ) → EReal // LowerSemicontinuous h ∧ h ≤ f }), ↑h' x

Any lower semicontinuous h ≤ f is bounded above by the candidate hull.

theorem exists_lowerSemicontinuousHull {n : ℕ} (f : (Fin n → ℝ) → EReal) : ∃ (g : (Fin n → ℝ) → EReal), LowerSemicontinuous g ∧ g ≤ f ∧ ∀ (h : (Fin n → ℝ) → EReal), LowerSemicontinuous h → h ≤ f → h ≤ g

noncomputable def lowerSemicontinuousHull {n : ℕ} (f : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

Text 7.0.4: The lower semicontinuous hull of f.

Equations

• lowerSemicontinuousHull f = Classical.choose ⋯

noncomputable def convexFunctionClosure {n : ℕ} (f : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

Text 7.0.5: The closure of a convex function f is the lower semicontinuous hull when f is never -∞, whereas it is the constant function -∞ when f is an improper convex function with f x = -∞ for some x.

Equations

• convexFunctionClosure f = if h : ∀ (x : Fin n → ℝ), f x ≠ ⊥ then lowerSemicontinuousHull f else fun (x : Fin n → ℝ) => ⊥

def ClosedConvexFunction {n : ℕ} (f : (Fin n → ℝ) → EReal) : Prop

Text 7.0.6: A convex function is called closed if it is lower semicontinuous on ℝ^n.

Equations

• ClosedConvexFunction f = (ConvexFunction f ∧ LowerSemicontinuous f)

theorem properConvexFunction_closed_iff_lowerSemicontinuous {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : ClosedConvexFunction f ↔ LowerSemicontinuous f

Text 7.0.6: A proper convex function is closed iff it is lower semicontinuous.

theorem closed_improper_const_top {n : ℕ} : (ClosedConvexFunction fun (x : Fin n → ℝ) => ⊤) ∧ ImproperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ⊤

The constant ⊤ function is closed and improper.

theorem closed_improper_const_bot {n : ℕ} : (ClosedConvexFunction fun (x : Fin n → ℝ) => ⊥) ∧ ImproperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ⊥

The constant ⊥ function is closed and improper.

theorem improperConvexFunctionOn_cases_epigraph_empty_or_bot {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} (h : ImproperConvexFunctionOn S f) : ¬(epigraph S f).Nonempty ∨ ∃ x ∈ S, f x = ⊥

An improper convex function has empty epigraph or attains ⊥ on the set.

theorem epigraph_empty_imp_forall_top {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} (h : ¬(epigraph S f).Nonempty) (x : Fin n → ℝ) : x ∈ S → f x = ⊤

If the epigraph is empty, then the function is identically ⊤ on S.

theorem convexFunctionClosure_eq_bot_of_exists_bot {n : ℕ} {f : (Fin n → ℝ) → EReal} (h : ∃ (x : Fin n → ℝ), f x = ⊥) : convexFunctionClosure f = fun (x : Fin n → ℝ) => ⊥

If f attains ⊥, then its closure is the constant ⊥ function.

theorem convexFunctionClosure_const_top {n : ℕ} : (convexFunctionClosure fun (x : Fin n → ℝ) => ⊤) = fun (x : Fin n → ℝ) => ⊤

The closure of the constant ⊤ function is itself.

theorem closed_improperConvexFunction_eq_top_or_bot {n : ℕ} {f : (Fin n → ℝ) → EReal} : convexFunctionClosure f = f ∧ ImproperConvexFunctionOn Set.univ f ↔ (f = fun (x : Fin n → ℝ) => ⊤) ∨ f = fun (x : Fin n → ℝ) => ⊥

theorem convexFunctionOn_inv_pos_aux : ConvexFunctionOn Set.univ fun (x : Fin 1 → ℝ) => if 0 < x 0 then ↑(1 / x 0) else ⊤

Convexity of the reciprocal on (0, ∞) extended by ⊤ outside.

theorem lowerSemicontinuous_inv_pos_aux : LowerSemicontinuous fun (x : Fin 1 → ℝ) => if 0 < x 0 then ↑(1 / x 0) else ⊤

Lower semicontinuity of the reciprocal on (0, ∞) extended by ⊤ outside.

theorem effectiveDomain_inv_pos_eq : (effectiveDomain Set.univ fun (x : Fin 1 → ℝ) => if 0 < x 0 then ↑(1 / x 0) else ⊤) = {x : Fin 1 → ℝ | 0 < x 0}

The effective domain of the reciprocal example is the positive half-line.

theorem not_isClosed_effectiveDomain_inv_pos : ¬IsClosed {x : Fin 1 → ℝ | 0 < x 0}

The positive half-line in Fin 1 → Real is not closed.

theorem exists_closed_proper_convexFunction_domain_not_closed : ∃ (n : ℕ) (f : (Fin n → ℝ) → EReal), ClosedConvexFunction f ∧ ProperConvexFunctionOn Set.univ f ∧ ¬IsClosed (effectiveDomain Set.univ f)

Text 7.0.8: It can happen that a closed proper convex function has a domain that is not closed.

theorem closedConvexFunction_inv_pos : ClosedConvexFunction fun (x : Fin 1 → ℝ) => if 0 < x 0 then ↑(1 / x 0) else ⊤

Text 7.0.9: For example, the function f(x) = 1/x for x > 0 and f(x) = +∞ for x ≤ 0 is closed.

theorem closure_epigraph_subset_epigraph_of_lsc_le {n : ℕ} {f g : (Fin n → ℝ) → EReal} (hg : LowerSemicontinuous g) (hle : g ≤ f) : closure (epigraph Set.univ f) ⊆ epigraph Set.univ g

If g is lower semicontinuous and g ≤ f, then closure (epi f) ⊆ epi g.

theorem lowerSemicontinuous_le_liminf_of_le {n : ℕ} {f g : (Fin n → ℝ) → EReal} (hg : LowerSemicontinuous g) (hle : g ≤ f) (x : Fin n → ℝ) : g x ≤ Filter.liminf (fun (y : Fin n → ℝ) => f y) (nhds x)

A lower semicontinuous minorant lies below the liminf of its majorant.

theorem closure_epigraph_upward {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ ν : ℝ} (hμν : μ ≤ ν) : (x, μ) ∈ closure (epigraph Set.univ f) → (x, ν) ∈ closure (epigraph Set.univ f)

The closure of an epigraph is upward closed in the second coordinate.

noncomputable def epigraphClosureInf {n : ℕ} (f : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

The function obtained by taking the infimum of each vertical slice of the epigraph closure.

Equations

• epigraphClosureInf f x = sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ closure (epigraph Set.univ f)})

theorem closure_epigraph_eq_epigraph_sInf {n : ℕ} (f : (Fin n → ℝ) → EReal) : epigraph Set.univ (epigraphClosureInf f) = closure (epigraph Set.univ f)

The closure of an epigraph is the epigraph of epigraphClosureInf.

theorem liminf_le_of_mem_closure_epigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} (hmem : (x, μ) ∈ closure (epigraph Set.univ f)) : Filter.liminf (fun (y : Fin n → ℝ) => f y) (nhds x) ≤ ↑μ

Points in the closure of the epigraph bound the liminf from above.

theorem epigraph_convexFunctionClosure_eq_closure_epigraph {n : ℕ} (f : (Fin n → ℝ) → EReal) (hbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : epigraph Set.univ (convexFunctionClosure f) = closure (epigraph Set.univ f) ∧ ∀ (x : Fin n → ℝ), convexFunctionClosure f x = Filter.liminf (fun (y : Fin n → ℝ) => f y) (nhds x)

Text 7.0.10: The epigraph of the closure of f is the closure of the epigraph of f. Consequently, (convexFunctionClosure f)(x) = liminf_{y → x} f(y).

theorem liminf_le_mem_iInter_closure_sublevel {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} {x : Fin n → ℝ} : Filter.liminf (fun (y : Fin n → ℝ) => f y) (nhds x) ≤ ↑α → x ∈ ⋂ (μ : { μ : ℝ // μ > α }), closure {y : Fin n → ℝ | f y ≤ ↑↑μ}

A liminf bound yields membership in all closed real sublevel sets above α.

theorem liminf_le_of_mem_iInter_closure_sublevel {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} {x : Fin n → ℝ} : x ∈ ⋂ (μ : { μ : ℝ // μ > α }), closure {y : Fin n → ℝ | f y ≤ ↑↑μ} → Filter.liminf (fun (y : Fin n → ℝ) => f y) (nhds x) ≤ ↑α

Membership in all closed real sublevel sets above α forces the liminf bound.