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

The α-sublevel of the liminf is the intersection of closed μ-sublevel sets above α.

theorem sublevel_convexFunctionClosure_eq_iInter_closure_sublevel {n : ℕ} (f : (Fin n → ℝ) → EReal) (α : ℝ) (hbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : {x : Fin n → ℝ | convexFunctionClosure f x ≤ ↑α} = ⋂ (μ : { μ : ℝ // μ > α }), closure {x : Fin n → ℝ | f x ≤ ↑↑μ}

Text 7.0.11: For each α ∈ ℝ, {x | (convexFunctionClosure f) x ≤ α} = ⋂ (μ > α), closure {x | f x ≤ μ}.

theorem convexFunctionClosure_le_self {n : ℕ} (f : (Fin n → ℝ) → EReal) : convexFunctionClosure f ≤ f

The closure of a function is pointwise below the function itself.

theorem convexFunctionClosure_mono {n : ℕ} {f1 f2 : (Fin n → ℝ) → EReal} (h12 : f1 ≤ f2) : convexFunctionClosure f1 ≤ convexFunctionClosure f2

The closure operator is monotone with respect to the pointwise order.

theorem iInf_convexFunctionClosure_eq {n : ℕ} (f : (Fin n → ℝ) → EReal) : ⨅ (x : Fin n → ℝ), f x = ⨅ (x : Fin n → ℝ), convexFunctionClosure f x

The infimum of a function equals the infimum of its closure.

theorem convexFunctionClosure_properties {n : ℕ} : (∀ (f : (Fin n → ℝ) → EReal), convexFunctionClosure f ≤ f) ∧ (∀ (f1 f2 : (Fin n → ℝ) → EReal), f1 ≤ f2 → convexFunctionClosure f1 ≤ convexFunctionClosure f2) ∧ ∀ (f : (Fin n → ℝ) → EReal), ⨅ (x : Fin n → ℝ), f x = ⨅ (x : Fin n → ℝ), convexFunctionClosure f x

Text 7.0.12: For any extended-real-valued function f : ℝ^n → [-∞, +∞], one has cl f ≤ f. Moreover, if f₁ ≤ f₂, then cl f₁ ≤ cl f₂. In addition, inf_{x ∈ ℝ^n} f x = inf_{x ∈ ℝ^n} (cl f) x. Here cl f is convexFunctionClosure f.

theorem frequently_pos_coord_nhds_zero : ∃ᶠ (y : Fin 1 → ℝ) in nhds 0, 0 < y 0

Points with positive coordinate appear frequently near the origin.

theorem liminf_example_origin_pos {x : Fin 1 → ℝ} (hx : 0 < x 0) : Filter.liminf (fun (y : Fin 1 → ℝ) => if 0 < y 0 then 0 else ⊤) (nhds x) = 0

At a point with positive coordinate, the liminf of the step function is 0.

theorem liminf_example_origin_neg {x : Fin 1 → ℝ} (hx : x 0 < 0) : Filter.liminf (fun (y : Fin 1 → ℝ) => if 0 < y 0 then 0 else ⊤) (nhds x) = ⊤

At a point with negative coordinate, the liminf of the step function is ⊤.

theorem liminf_example_origin_zero : Filter.liminf (fun (y : Fin 1 → ℝ) => if 0 < y 0 then 0 else ⊤) (nhds 0) = 0

At the origin, the liminf of the step function is 0.

theorem convexFunctionClosure_example_origin : (convexFunctionClosure fun (x : Fin 1 → ℝ) => if 0 < x 0 then 0 else ⊤) = fun (x : Fin 1 → ℝ) => if x 0 < 0 then ⊤ else 0

Text 7.0.13: If f : ℝ → [-∞, +∞] is defined by f(x) = 0 for x > 0 and f(x) = +∞ for x ≤ 0, then cl f agrees with f except at the origin, where (cl f)(0) = 0 rather than +∞.

theorem frequently_mem_ball_of_mem_closure {x : Fin 2 → ℝ} (hx : x ∈ closure (Metric.ball 0 1)) : ∃ᶠ (y : Fin 2 → ℝ) in nhds x, y ∈ Metric.ball 0 1

Points in the closure of the unit ball are frequently in the unit ball.

theorem eventually_not_mem_closure_of_not_mem {x : Fin 2 → ℝ} (hx : x ∉ closure (Metric.ball 0 1)) : ∀ᶠ (y : Fin 2 → ℝ) in nhds x, y ∉ closure (Metric.ball 0 1)

Points outside the closure of the unit ball have a neighborhood outside it.

theorem liminf_unitDisk_closure_eq_zero (f : (Fin 2 → ℝ) → EReal) (h0 : ∀ x ∈ Metric.ball 0 1, f x = 0) (hnonneg : ∀ (x : Fin 2 → ℝ), 0 ≤ f x) {x : Fin 2 → ℝ} (hx : x ∈ closure (Metric.ball 0 1)) : Filter.liminf (fun (y : Fin 2 → ℝ) => f y) (nhds x) = 0

On the closure of the unit ball, the liminf of f is 0.

theorem liminf_unitDisk_outside_eq_top (f : (Fin 2 → ℝ) → EReal) (hInf : ∀ x ∉ closure (Metric.ball 0 1), f x = ⊤) {x : Fin 2 → ℝ} (hx : x ∉ closure (Metric.ball 0 1)) : Filter.liminf (fun (y : Fin 2 → ℝ) => f y) (nhds x) = ⊤

Outside the closure of the unit ball, the liminf of f is ⊤.

theorem convexFunctionClosure_example_unitDisk (f : (Fin 2 → ℝ) → EReal) (h0 : ∀ x ∈ Metric.ball 0 1, f x = 0) (hInf : ∀ x ∉ closure (Metric.ball 0 1), f x = ⊤) (hnonneg : ∀ (x : Fin 2 → ℝ), 0 ≤ f x) : (∀ x ∈ closure (Metric.ball 0 1), convexFunctionClosure f x = 0) ∧ ∀ x ∉ closure (Metric.ball 0 1), convexFunctionClosure f x = ⊤

Text 7.0.14: If C is the unit disk in ℝ^2 and f(x) = 0 for x ∈ C while f(x) = +∞ for x ∉ C (with arbitrary boundary values), then cl f(x) = 0 for all x ∈ cl C and +∞ elsewhere.