theorem convexOn_neg_sqrt_one_sub : ConvexOn ℝ (Set.Iio 1) fun (t : ℝ) => -√(1 - t)

Convexity of t ↦ -sqrt (1 - t) on (-∞, 1).

theorem monotoneOn_neg_sqrt_one_sub : MonotoneOn (fun (t : ℝ) => -√(1 - t)) (Set.Iio 1)

Monotonicity of t ↦ -sqrt (1 - t) on (-∞, 1).

theorem convexOn_norm_sq_univ {n : ℕ} : ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => ‖x‖ ^ 2

Convexity of the squared norm on the whole space.

theorem convexOn_neg_sqrt_one_sub_norm_sq {n : ℕ} : ConvexOn ℝ {x : Fin n → ℝ | ‖x‖ < 1} fun (x : Fin n → ℝ) => -√(1 - ‖x‖ ^ 2)

Convexity of x ↦ -sqrt(1 - ‖x‖^2) on the open unit ball.

theorem convexFunction_negativeSqrt_unitBall {n : ℕ} : ConvexFunction fun (x : Fin n → ℝ) => if ‖x‖ < 1 then ↑(-√(1 - ‖x‖ ^ 2)) else ⊤

Remark 7.0.25: Theorem 7.5 can be used to show convexity. For example, the function f(x) = -(1 - |x|^2)^{1/2} on ℝ^n (with f(x) = +∞ for |x| ≥ 1) is convex by verifying the limit relation in Theorem 7.5 at boundary points.

theorem exists_lt_on_ri_effectiveDomain_of_iInf_lt {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) {α : ℝ} (hα : ⨅ (x : Fin n → ℝ), f x < ↑α) : ∃ x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f), f x.ofLp < ↑α

If iInf f < α, then some point in ri (dom f) satisfies f x < α.

theorem levelSets_horizontal_section_mem_iff {n : ℕ} {f : (Fin n → ℝ) → EReal} (α : ℝ) (x : EuclideanSpace ℝ (Fin n)) : have C := ⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) => ((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ f); have y := (EuclideanSpace.equiv (Fin n) ℝ).symm x.ofLp; have zα := (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => α; (appendAffineEquiv n 1) (y, zα) ∈ C ↔ f x.ofLp ≤ ↑α

Horizontal section of the embedded epigraph corresponds to the ≤-sublevel set.

theorem exists_riEpigraph_point_at_height {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) {α : ℝ} (hα : ⨅ (x : Fin n → ℝ), f x < ↑α) : ∃ x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f), f x.ofLp < ↑α ∧ (appendAffineEquiv n 1) ((EuclideanSpace.equiv (Fin n) ℝ).symm x.ofLp, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => α) ∈ riEpigraph f

A point in ri (dom f) with f x < α yields a point of ri (epi f) at height α.

theorem levelSets_plane_meets_riEpigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) {α : ℝ} (hα : ⨅ (x : Fin n → ℝ), f x < ↑α) : have C := ⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) => ((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ f); have zα := (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => α; have φ := LinearMap.snd ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin 1)) ∘ₗ ↑(appendAffineEquiv n 1).symm.linear; have M := AffineSubspace.mk' ((appendAffineEquiv n 1) (0, zα)) (LinearMap.ker φ); (↑M ∩ euclideanRelativeInterior (n + 1) C).Nonempty

The horizontal hyperplane at height α meets ri (epi f) when α > inf f.

theorem appendAffineEquiv_mem_horizontal_plane {n : ℕ} {α : ℝ} (y : EuclideanSpace ℝ (Fin n)) : have zα := (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => α; have φ := LinearMap.snd ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin 1)) ∘ₗ ↑(appendAffineEquiv n 1).symm.linear; have M := AffineSubspace.mk' ((appendAffineEquiv n 1) (0, zα)) (LinearMap.ker φ); (appendAffineEquiv n 1) (y, zα) ∈ ↑M

Points of the form appendAffineEquiv n 1 (y, zα) lie in the horizontal plane M.

theorem levelSets_horizontal_slice_image {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} : have sublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp ≤ ↑α}; have C := ⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) => ((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ f); have zα := (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => α; have φ := LinearMap.snd ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin 1)) ∘ₗ ↑(appendAffineEquiv n 1).symm.linear; have M := AffineSubspace.mk' ((appendAffineEquiv n 1) (0, zα)) (LinearMap.ker φ); have g := fun (x : EuclideanSpace ℝ (Fin n)) => (appendAffineEquiv n 1) ((EuclideanSpace.equiv (Fin n) ℝ).symm x.ofLp, zα); g '' sublevel = ↑M ∩ C

The horizontal slice of the embedded epigraph is the image of the ≤-sublevel set.

theorem horizontal_slice_homeomorph {n : ℕ} {α : ℝ} : have zα := (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => α; have φ := LinearMap.snd ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin 1)) ∘ₗ ↑(appendAffineEquiv n 1).symm.linear; have M := AffineSubspace.mk' ((appendAffineEquiv n 1) (0, zα)) (LinearMap.ker φ); have g := fun (x : EuclideanSpace ℝ (Fin n)) => (appendAffineEquiv n 1) ((EuclideanSpace.equiv (Fin n) ℝ).symm x.ofLp, zα); ∃ (gM : EuclideanSpace ℝ (Fin n) ≃ₜ ↥M), ∀ (x : EuclideanSpace ℝ (Fin n)), ↑(gM x) = g x

The horizontal slice map is a homeomorphism onto the plane M.

theorem levelSets_horizontal_slice_preimage_closure_ri {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} : have sublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp ≤ ↑α}; have C := ⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) => ((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ f); have zα := (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => α; have φ := LinearMap.snd ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin 1)) ∘ₗ ↑(appendAffineEquiv n 1).symm.linear; have M := AffineSubspace.mk' ((appendAffineEquiv n 1) (0, zα)) (LinearMap.ker φ); have g := fun (x : EuclideanSpace ℝ (Fin n)) => (appendAffineEquiv n 1) ((EuclideanSpace.equiv (Fin n) ℝ).symm x.ofLp, zα); Convex ℝ C → (↑M ∩ euclideanRelativeInterior (n + 1) C).Nonempty → closure sublevel = g ⁻¹' (↑M ∩ closure C) ∧ euclideanRelativeInterior n sublevel = g ⁻¹' (↑M ∩ euclideanRelativeInterior (n + 1) C)

Pull back closure and relative interior across the horizontal slice homeomorphism.

theorem sublevel_subset_closure_strictSublevel {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) {α : ℝ} (hα : ⨅ (x : Fin n → ℝ), f x < ↑α) : have sublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp ≤ ↑α}; have strictSublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp < ↑α}; sublevel ⊆ closure strictSublevel

The non-strict sublevel lies in the closure of the strict sublevel.

theorem ri_domf_lt_open {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) {α : ℝ} : have domf := (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f; have s := {x : EuclideanSpace ℝ (Fin n) | x ∈ euclideanRelativeInterior n domf ∧ f x.ofLp < ↑α}; IsOpen {x : ↥(affineSpan ℝ domf) | ↑x ∈ s}

The strict inequality set is relatively open in affineSpan domf.

theorem affineSpan_eq_of_nonempty_relOpen {n : ℕ} (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) {s : Set (EuclideanSpace ℝ (Fin n))} (hsA : s ⊆ ↑A) (hsne : s.Nonempty) (hsopen : IsOpen {x : ↥A | ↑x ∈ s}) : affineSpan ℝ s = A

A nonempty relatively open subset of an affine subspace has full affine span.

theorem closure_embedded_epigraph_eq_convexFunctionClosure {n : ℕ} {f : (Fin n → ℝ) → EReal} (hbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : have C := ⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) => ((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ f); closure C = ⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) => ((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ (convexFunctionClosure f))

The closure of the embedded epigraph equals the embedded epigraph of the closure.

Theorem 7.6 auxiliary proof

theorem properConvexFunction_levelSets_same_closure_ri_dim_aux {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) {α : ℝ} (hα : ⨅ (x : Fin n → ℝ), f x < ↑α) : have sublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp ≤ ↑α}; have strictSublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp < ↑α}; have domf := (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f; closure sublevel = {x : EuclideanSpace ℝ (Fin n) | convexFunctionClosure f x.ofLp ≤ ↑α} ∧ closure strictSublevel = {x : EuclideanSpace ℝ (Fin n) | convexFunctionClosure f x.ofLp ≤ ↑α} ∧ euclideanRelativeInterior n sublevel = {x : EuclideanSpace ℝ (Fin n) | x ∈ euclideanRelativeInterior n domf ∧ f x.ofLp < ↑α} ∧ euclideanRelativeInterior n strictSublevel = {x : EuclideanSpace ℝ (Fin n) | x ∈ euclideanRelativeInterior n domf ∧ f x.ofLp < ↑α} ∧ Module.finrank ℝ ↥(affineSpan ℝ sublevel).direction = Module.finrank ℝ ↥(affineSpan ℝ domf).direction ∧ Module.finrank ℝ ↥(affineSpan ℝ strictSublevel).direction = Module.finrank ℝ ↥(affineSpan ℝ domf).direction

Auxiliary proof for Theorem 7.6.

theorem properConvexFunction_levelSets_same_closure_ri_dim {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) {α : ℝ} (hα : ⨅ (x : Fin n → ℝ), f x < ↑α) : have sublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp ≤ ↑α}; have strictSublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp < ↑α}; have domf := (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f; closure sublevel = {x : EuclideanSpace ℝ (Fin n) | convexFunctionClosure f x.ofLp ≤ ↑α} ∧ closure strictSublevel = {x : EuclideanSpace ℝ (Fin n) | convexFunctionClosure f x.ofLp ≤ ↑α} ∧ euclideanRelativeInterior n sublevel = {x : EuclideanSpace ℝ (Fin n) | x ∈ euclideanRelativeInterior n domf ∧ f x.ofLp < ↑α} ∧ euclideanRelativeInterior n strictSublevel = {x : EuclideanSpace ℝ (Fin n) | x ∈ euclideanRelativeInterior n domf ∧ f x.ofLp < ↑α} ∧ Module.finrank ℝ ↥(affineSpan ℝ sublevel).direction = Module.finrank ℝ ↥(affineSpan ℝ domf).direction ∧ Module.finrank ℝ ↥(affineSpan ℝ strictSublevel).direction = Module.finrank ℝ ↥(affineSpan ℝ domf).direction

Theorem 7.6: Let f be a proper convex function, and let α ∈ ℝ with α > inf f. The convex level sets {x | f x ≤ α} and {x | f x < α} have the same closure and the same relative interior, namely {x | (cl f) x ≤ α} and {x ∈ ri (dom f) | f x < α}. Furthermore, they have the same dimension as dom f.

theorem iInf_const_zero_ereal {n : ℕ} : ⨅ (x : Fin n → ℝ), 0 = 0

The infimum of the constant zero EReal function is zero.

theorem strictSublevel_const_zero_eq_empty {n : ℕ} : {x : EuclideanSpace ℝ (Fin n) | 0 < 0 ∧ x = x} = ∅

The strict sublevel set for the constant zero function at zero is empty.

theorem rhs_nonempty_via_closure_le_self {n : ℕ} : ∃ (x : EuclideanSpace ℝ (Fin n)), convexFunctionClosure (fun (x : Fin n → ℝ) => 0) x.ofLp ≤ 0

The right-hand side of the strict-sublevel closure formula is nonempty for the zero function.

theorem properConvexFunction_levelSets_formulas_fail_at_inf : ∃ (n : ℕ) (f : (Fin n → ℝ) → EReal) (α : ℝ), ProperConvexFunctionOn Set.univ f ∧ ↑α = ⨅ (x : Fin n → ℝ), f x ∧ have sublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp ≤ ↑α}; have strictSublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp < ↑α}; have domf := (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f; ¬(closure sublevel = {x : EuclideanSpace ℝ (Fin n) | convexFunctionClosure f x.ofLp ≤ ↑α} ∧ closure strictSublevel = {x : EuclideanSpace ℝ (Fin n) | convexFunctionClosure f x.ofLp ≤ ↑α} ∧ euclideanRelativeInterior n sublevel = {x : EuclideanSpace ℝ (Fin n) | x ∈ euclideanRelativeInterior n domf ∧ f x.ofLp < ↑α} ∧ euclideanRelativeInterior n strictSublevel = {x : EuclideanSpace ℝ (Fin n) | x ∈ euclideanRelativeInterior n domf ∧ f x.ofLp < ↑α})

Text 7.0.17: The closure and relative interior formulas in Theorem 7.6 can fail when α = inf f.

theorem lt_f_of_lt_iInf {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} (hα : ↑α < ⨅ (x : Fin n → ℝ), f x) (x : Fin n → ℝ) : ↑α < f x

If α < iInf f, then α < f x for every x.

theorem not_mem_sublevel_of_lt {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} {x : Fin n → ℝ} (h : ↑α < f x) : ¬f x ≤ ↑α

A strict lower bound excludes membership in the ≤-sublevel set.

theorem sublevel_eq_empty_of_forall_not_mem {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} (h : ∀ (x : Fin n → ℝ), ¬f x ≤ ↑α) : {x : Fin n → ℝ | f x ≤ ↑α} = ∅

If no point satisfies the sublevel predicate, the sublevel set is empty.

theorem sublevel_eq_empty_of_lt_inf {n : ℕ} (f : (Fin n → ℝ) → EReal) {α : ℝ} (hα : ↑α < ⨅ (x : Fin n → ℝ), f x) : {x : Fin n → ℝ | f x ≤ ↑α} = ∅

Text 7.0.18: If α < inf f then {x | f x ≤ α} is empty and the formulas are trivial. The case α = inf f is more subtle and can also lead to failure of the formulas; see the example above.

theorem strictSublevel_eq_domf_inter_of_lt_top {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} (hαtop : ↑α < ⊤) : {x : EuclideanSpace ℝ (Fin n) | f x.ofLp < ↑α} = {x : EuclideanSpace ℝ (Fin n) | x ∈ (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f ∧ f x.ofLp < ↑α}

If α < ⊤, the strict sublevel already lies in the effective domain.

theorem ri_domf_eq_of_relOpen {n : ℕ} {domf : Set (EuclideanSpace ℝ (Fin n))} (hopen : euclideanRelativelyOpen n domf) : euclideanRelativeInterior n domf = domf

Relative openness means the relative interior agrees with the set.

theorem sublevel_eq_set_of_convexFunctionClosure_of_closed {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} (hfclosed : ClosedConvexFunction f) (hbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : {x : EuclideanSpace ℝ (Fin n) | convexFunctionClosure f x.ofLp ≤ ↑α} = {x : EuclideanSpace ℝ (Fin n) | f x.ofLp ≤ ↑α}

Closedness lets us replace cl f with f in sublevel sets.

theorem closedProperConvexFunction_ri_sublevel_eq_strictSublevel_and_closure {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfclosed : ClosedConvexFunction f) (hfproper : ProperConvexFunctionOn Set.univ f) (hopen : euclideanRelativelyOpen n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f)) {α : ℝ} (hαinf : ⨅ (x : Fin n → ℝ), f x < ↑α) (hαtop : ↑α < ⊤) : have sublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp ≤ ↑α}; have strictSublevel := {x : EuclideanSpace ℝ (Fin n) | f x.ofLp < ↑α}; euclideanRelativeInterior n sublevel = strictSublevel ∧ closure strictSublevel = sublevel

Corollary 7.6.1: If f is a closed proper convex function whose effective domain is relatively open (in particular if effectiveDomain Set.univ f is an affine set), then for inf f < α < +∞ one has ri {x | f x ≤ α} = {x | f x < α} and cl {x | f x < α} = {x | f x ≤ α}.