def sublevelSet {n : ℕ} (f : (Fin n → ℝ) → WithTop ℝ) (α : ℝ) : Set (Fin n → ℝ)

Definition 6.27.1 (Sublevel set): for an extended-real-valued function f : ℝ^n → (-∞, +∞] and α ∈ ℝ, the α-sublevel set lev_α f is {x ∈ ℝ^n | f x ≤ α}.

noncomputable def functionInfimum {n : ℕ} (f : (Fin n → ℝ) → WithTop ℝ) : WithBot (WithTop ℝ)

Definition 6.27.2 (Infimum of a function): for an extended-real-valued function f : ℝ^n → (-∞, +∞], the infimum inf f is the infimum in [-∞, +∞] of the set of values {f x | x ∈ ℝ^n}, viewed in [-∞, +∞], equivalently the greatest lower bound of those values.

def minimumSet {n : ℕ} (f : (Fin n → ℝ) → WithTop ℝ) : Set (Fin n → ℝ)

Definition 6.27.3 (Minimum set): for an extended-real-valued function f : ℝ^n → (-∞, +∞], the minimum set is the set of minimizers, namely {x ∈ ℝ^n | f x = inf f}, with f x viewed in [-∞, +∞].

def IsConvexFunction {n : ℕ} (f : (Fin n → ℝ) → WithTop ℝ) : Prop

An extended-real-valued function on ℝ^n is convex when its epigraph is a convex subset of ℝ^n × ℝ.

def withTopFunctionToEReal {n : ℕ} (f : (Fin n → ℝ) → WithTop ℝ) : (Fin n → ℝ) → EReal

Lift a WithTop ℝ-valued function to an EReal-valued function by viewing each value in (-∞, +∞] as an extended real with no additional -∞ values introduced.

def epigraphWithTop {n : ℕ} (h : (Fin n → ℝ) → WithTop ℝ) : Set ((Fin n → ℝ) × ℝ)

Definition 6.27.9 (Epigraph): for an extended-real-valued function h : ℝ^n → (-∞, +∞], the epigraph epi h is the subset of ℝ^(n+1) consisting of the pairs (x, μ) with h x ≤ μ. In Lean, ℝ^(n+1) is modeled as (Fin n → ℝ) × ℝ.

theorem helperForProposition_6_27_1_mem_epigraphWithTop_iff {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} {x : Fin n → ℝ} {α : ℝ} : x ∈ sublevelSet f α ↔ (x, α) ∈ epigraphWithTop f

Helper for Proposition 6.27.1: membership in the α-sublevel set is the same as membership in the epigraph at height α.

theorem helperForProposition_6_27_1_affineCombo_same_height {n : ℕ} {x y : Fin n → ℝ} {a b α : ℝ} (hab : a + b = 1) : a • (x, α) + b • (y, α) = (a • x + b • y, α)

Helper for Proposition 6.27.1: an affine combination of two points with common height α still has height α when the coefficients sum to 1.

theorem helperForProposition_6_27_1_convex_epigraphWithTop_of_IsConvexFunction {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hf : IsConvexFunction f) : Convex ℝ (epigraphWithTop f)

Helper for Proposition 6.27.1: convexity of the function is exactly convexity of its epigraph written with the dedicated definition epigraphWithTop.

theorem helperForProposition_6_27_1_convex_sublevelSet_of_convex_epigraphWithTop {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (h_epigraph : Convex ℝ (epigraphWithTop f)) (α : ℝ) : Convex ℝ (sublevelSet f α)

Helper for Proposition 6.27.1: once the epigraph is convex, each horizontal slice at height α is convex, so the corresponding sublevel set is convex.

theorem convex_sublevelSet {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hf : IsConvexFunction f) (α : ℝ) : Convex ℝ (sublevelSet f α)

Proposition 6.27.1 (Convexity of sublevel sets): if f : ℝ^n → (-∞, +∞] is a convex function, then for every α ∈ ℝ the sublevel set sublevelSet f α = {x | f x ≤ α} is convex.

theorem helperForProposition_6_27_2_sublevelSet_eq_preimage_Iic {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (α : ℝ) : sublevelSet f α = f ⁻¹' Set.Iic ↑α

Helper for Proposition 6.27.2: the real sublevel set is the preimage of the lower interval (-∞, α] in WithTop ℝ.

theorem helperForProposition_6_27_2_isClosed_preimage_Iic {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hf_closed : LowerSemicontinuous f) (α : ℝ) : IsClosed (f ⁻¹' Set.Iic ↑α)

Helper for Proposition 6.27.2: a lower semicontinuous WithTop ℝ-valued function has closed preimages of lower closed rays (-∞, α].

theorem helperForProposition_6_27_2_isClosed_sublevelSet_of_lsc {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hf_closed : LowerSemicontinuous f) (α : ℝ) : IsClosed (sublevelSet f α)

Helper for Proposition 6.27.2: lower semicontinuity alone already forces every real sublevel set of f to be closed.

theorem isClosed_sublevelSet_of_closed_convexFunction {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hf_closed : LowerSemicontinuous f) (hf_convex : IsConvexFunction f) (α : ℝ) : IsClosed (sublevelSet f α)

Proposition 6.27.2 (Closedness of sublevel sets): if f : ℝ^n → (-∞, +∞] is a closed convex function, then for every α ∈ ℝ the sublevel set sublevelSet f α = {x | f x ≤ α} is closed.

def effectiveDomainWithTop {n : ℕ} (f : (Fin n → ℝ) → WithTop ℝ) : Set (Fin n → ℝ)

The effective domain of a (-∞, +∞]-valued function on ℝ^n is the set of points where the function is finite.

def IsDirectionOfRecessionWithTop {n : ℕ} (f : (Fin n → ℝ) → WithTop ℝ) (y : Fin n → ℝ) : Prop

Definition 6.27.4 (Direction of recession): for an extended-real-valued function f : ℝ^n → (-∞, +∞], a nonzero vector y is a direction of recession of f when for every x ∈ dom f and every λ ≥ 0, one has f (x + λ y) ≤ f x; equivalently, the function λ ↦ f (x + λ y) is non-increasing on [0, ∞).

def parabolicConvexSet : Set (ℝ × ℝ)

Definition 6.27.5 (Parabolic convex set): the set P ⊆ ℝ² is {(ξ₁, ξ₂) ∈ ℝ² | ξ₂ ≥ ξ₁²}.

@[reducible, inline]

abbrev EuclideanPlane : Type

A concrete Euclidean model of ℝ².

noncomputable def squaredDistance (P : Set EuclideanPlane) (x : EuclideanPlane) : WithTop ℝ

Definition 6.27.7 (Squared distance function): for a set P ⊆ ℝ² and each x ∈ ℝ², define f₀(x) to be the infimum of the squared Euclidean distances ‖x - y‖² as y ranges over P. Here the infimum is taken in WithTop ℝ, so squaredDistance P x takes values in [0, +∞]; in particular, this convention gives squaredDistance P x = ⊤ when P = ∅.

def parabolicConvexSetEuclidean : Set EuclideanPlane

The parabolic convex set viewed inside the Euclidean-space model of ℝ².

noncomputable def squaredDistanceToParabolicConvexSet : EuclideanPlane → WithTop ℝ

The squared-distance function specialized to the parabolic convex set.

@[reducible, inline]

noncomputable abbrev indicatorFunctionEReal {n : ℕ} (C : Set (Fin n → ℝ)) : (Fin n → ℝ) → EReal

Definition 6.27.6 (Indicator function): for a set C ⊆ ℝ^n, the indicator function δ(· | C) is the extended-real-valued function equal to 0 on C and +∞ outside C. This reuses the existing EReal-valued indicator function already defined in the project.

noncomputable def parabolicNormSquareFunction : EuclideanPlane → WithTop ℝ

The auxiliary function f₁ on the Euclidean plane is the squared norm x ↦ ‖x‖², viewed as a (-∞, +∞]-valued function with no +∞ values.

noncomputable def parabolicIndicatorFunction : EuclideanPlane → WithTop ℝ

The auxiliary function f₂ on the Euclidean plane is the indicator δ(· | P) of the parabolic convex set P, taking the value 0 on P and +∞ outside P.

noncomputable def parabolicAuxiliaryAndObjectiveFunctions : (EuclideanPlane → WithTop ℝ) × (EuclideanPlane → WithTop ℝ) × (EuclideanPlane → WithTop ℝ)

Definition 6.27.8 (Auxiliary functions; The function f): define the three functions (f₁, f₂, f) on ℝ² by f₁(x) = ‖x‖², f₂(x) = δ(x | P), and, for x = (ξ₁, ξ₂) ∈ ℝ², f(x) = f₀(ξ₁, ξ₂) - ξ₁, where f₀ is the squared-distance function to the parabolic set P. In Lean, ξ₁ is the first coordinate x (0 : Fin 2).

noncomputable def parabolicObjectiveFunction : EuclideanPlane → WithTop ℝ

The parabolic objective function f is the third component of the bundled triple (f₁, f₂, f).

theorem helperForProposition_6_27_8_parabolicConvexSetEuclidean_nonempty : parabolicConvexSetEuclidean.Nonempty

Helper for Proposition 6.27.8: the Euclidean parabolic set contains the origin, so the squared-distance infimum is taken over a nonempty set.

theorem helperForProposition_6_27_8_parabolicConvexSetEuclidean_convex : Convex ℝ parabolicConvexSetEuclidean

Helper for Proposition 6.27.8: the Euclidean parabolic set is convex.

theorem helperForProposition_6_27_8_squaredDistanceToParabolicConvexSet_eq_coe_sInf (x : EuclideanPlane) : squaredDistanceToParabolicConvexSet x = ↑(sInf ((fun (y : EuclideanPlane) => ‖x - y‖ ^ 2) '' parabolicConvexSetEuclidean))

Helper for Proposition 6.27.8: the squared-distance function is the coercion of the real infimum of squared norms over the parabolic set.

theorem helperForProposition_6_27_8_parabolicObjectiveFunction_eq_coe_realEnvelope (x : EuclideanPlane) : parabolicObjectiveFunction x = ↑(sInf ((fun (y : EuclideanPlane) => ‖x - y‖ ^ 2) '' parabolicConvexSetEuclidean) - x.ofLp 0)

Helper for Proposition 6.27.8: the parabolic objective is the coercion of the real squared-distance envelope minus the first coordinate.

theorem helperForProposition_6_27_8_realEnvelope_convex : ConvexOn ℝ Set.univ fun (x : EuclideanPlane) => sInf ((fun (y : EuclideanPlane) => ‖x - y‖ ^ 2) '' parabolicConvexSetEuclidean)

Helper for Proposition 6.27.8: the real squared-distance envelope over the parabolic set is convex on the whole Euclidean plane.

theorem helperForProposition_6_27_8_negFirstCoordinate_convex : ConvexOn ℝ Set.univ fun (x : EuclideanPlane) => -x.ofLp 0

Helper for Proposition 6.27.8: the negative first-coordinate map is affine, hence convex on the whole Euclidean plane.

theorem parabolicObjectiveFunction_finite_and_convex : (∀ (x : EuclideanPlane), parabolicObjectiveFunction x < ⊤) ∧ Convex ℝ {p : EuclideanPlane × ℝ | parabolicObjectiveFunction p.1 ≤ ↑p.2}

Proposition 6.27.8: the function f defined by f(x) = f₀(x) - ξ₁ for x = (ξ₁, ξ₂) ∈ ℝ², where f₀ is the squared-distance function to the parabolic convex set, is finite everywhere on ℝ² and is convex.

theorem helperForProposition_6_27_3_mem_effectiveDomain_of_mem_sublevel {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} {x : Fin n → ℝ} {α : ℝ} : x ∈ sublevelSet f α → x ∈ effectiveDomainWithTop f

Helper for Proposition 6.27.3: membership in a real sublevel set already forces the function value to be finite.

theorem helperForProposition_6_27_3_exists_sublevel_of_mem_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} {x : Fin n → ℝ} : x ∈ effectiveDomainWithTop f → ∃ (α : ℝ), x ∈ sublevelSet f α

Helper for Proposition 6.27.3: a finite WithTop ℝ value comes from an actual real level, so the point lies in some real sublevel set.

theorem helperForProposition_6_27_3_mem_iUnion_sublevelSet_iff {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} {x : Fin n → ℝ} : x ∈ ⋃ (α : ℝ), sublevelSet f α ↔ x ∈ effectiveDomainWithTop f

Helper for Proposition 6.27.3: a point belongs to the union of all real sublevel sets exactly when the function is finite there.

theorem iUnion_sublevelSet_eq_effectiveDomainWithTop {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hproper : (effectiveDomainWithTop f).Nonempty) : ⋃ (α : ℝ), sublevelSet f α = effectiveDomainWithTop f

Proposition 6.27.3 (Union of sublevel sets): for a proper function f : ℝ^n → (-∞, +∞], the union of all real sublevel sets is the effective domain dom f = {x ∈ ℝ^n | f x < +∞}.

theorem helperForProposition_6_27_4_minimumSet_eq_empty_of_functionInfimum_eq_bot {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (h : functionInfimum f = ⊥) : minimumSet f = ∅

Helper for Proposition 6.27.4: if the function infimum is -∞, then no point can realize that value because f only takes values in (-∞, +∞].

theorem helperForProposition_6_27_4_minimumSet_eq_univ_of_functionInfimum_eq_top {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (h : functionInfimum f = ⊤) : minimumSet f = Set.univ

Helper for Proposition 6.27.4: if the function infimum is +∞, then every value of f must be +∞, so every point is a minimizer.

theorem helperForProposition_6_27_4_exists_real_of_functionInfimum_ne_bot_ne_top {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hne_bot : functionInfimum f ≠ ⊥) (hne_top : functionInfimum f ≠ ⊤) : ∃ (α : ℝ), functionInfimum f = ↑↑α

Helper for Proposition 6.27.4: if the function infimum is neither -∞ nor +∞, then it is represented by a finite real number.

theorem helperForProposition_6_27_4_minimumSet_eq_sublevelSet_of_functionInfimum_eq_real {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} {α : ℝ} (h : functionInfimum f = ↑↑α) : minimumSet f = sublevelSet f α

Helper for Proposition 6.27.4: once the infimum is a finite real value α, the minimum set coincides with the α-sublevel set.

theorem convex_minimumSet {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hf : IsConvexFunction f) : Convex ℝ (minimumSet f)

Proposition 6.27.4 (Convexity of the minimum set): if f : ℝ^n → (-∞, +∞] is a convex function and M is its minimum set, then M is a convex subset of ℝ^n.

theorem isClosed_minimumSet_of_closed_convexFunction {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hf_closed : LowerSemicontinuous f) (hf_convex : IsConvexFunction f) : IsClosed (minimumSet f)

Proposition 6.27.5 (Closedness of the minimum set): if f : ℝ^n → (-∞, +∞] is a closed convex function and M is its minimum set, then M is a closed subset of ℝ^n.

theorem helperForProposition_6_27_6_functionInfimum_le_pointValue {n : ℕ} (f : (Fin n → ℝ) → WithTop ℝ) (z : Fin n → ℝ) : functionInfimum f ≤ ↑(f z)

Helper for Proposition 6.27.6: the function infimum lies below every point value in the range used to define it.

theorem helperForProposition_6_27_6_mem_minimumSet_iff_pointwiseLowerBound {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} {x : Fin n → ℝ} : x ∈ minimumSet f ↔ ∀ (z : Fin n → ℝ), ↑(f x) ≤ ↑(f z)

Helper for Proposition 6.27.6: belonging to the minimum set means that the value at x is below every point value of f.

theorem helperForProposition_6_27_6_withTopFunctionToEReal_order_iff {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} {x z : Fin n → ℝ} : withTopFunctionToEReal f x ≤ withTopFunctionToEReal f z ↔ ↑(f x) ≤ ↑(f z)

Helper for Proposition 6.27.6: the EReal order for the lifted function is exactly the same as the WithBot (WithTop ℝ) order on the original WithTop ℝ values.

theorem helperForProposition_6_27_6_zero_mem_subdifferentialAt_iff_pointwiseLowerBound {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} {x : Fin n → ℝ} : 0 ∈ subdifferentialAt (withTopFunctionToEReal f) x ↔ ∀ (z : Fin n → ℝ), withTopFunctionToEReal f x ≤ withTopFunctionToEReal f z

Helper for Proposition 6.27.6: the zero dual vector is a subgradient exactly when the lifted function value at x is below every lifted function value.

theorem mem_minimumSet_iff_zero_mem_subdifferentialAt {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hproper : (effectiveDomainWithTop f).Nonempty) (hf : IsConvexFunction f) (x : Fin n → ℝ) : x ∈ minimumSet f ↔ 0 ∈ subdifferentialAt (withTopFunctionToEReal f) x

Proposition 6.27.6 (Characterization of minimizers by the subdifferential): let f : ℝ^n → (-∞, +∞] be a proper convex function, and let M be the minimum set of f. Then for any x ∈ ℝ^n, one has x ∈ M if and only if the zero dual vector belongs to the subdifferential of f at x. Equivalently, x is a minimizer exactly when x^* = 0 is a subgradient of f at x.

theorem helperForProposition_6_27_7_value_le_affineCombinationOfHeights {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hf : IsConvexFunction f) {x y : Fin n → ℝ} {a b t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) (hx : f x ≤ ↑a) (hy : f y ≤ ↑b) : f ((1 - t) • x + t • y) ≤ ↑((1 - t) * a + t * b)

Helper for Proposition 6.27.7: convexity of the epigraph bounds the function value at a segment point by the affine combination of the two finite endpoint heights.

theorem helperForProposition_6_27_7_segmentPoint_mem_ball {n : ℕ} {x y : Fin n → ℝ} {ε : ℝ} (hε : 0 < ε) : have t := ε / (2 * (ε + ‖y - x‖)); have z := (1 - t) • x + t • y; 0 < t ∧ t < 1 ∧ ‖z - x‖ < ε

Helper for Proposition 6.27.7: the standard short segment point from x toward y stays inside the local-minimum ball.

theorem helperForProposition_6_27_7_globalLowerBound_of_localMinimum {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hf : IsConvexFunction f) {x : Fin n → ℝ} (hx : x ∈ effectiveDomainWithTop f) (hlocal : ∃ ε > 0, ∀ (z : Fin n → ℝ), ‖z - x‖ < ε → f z ≥ f x) (y : Fin n → ℝ) : f y ≥ f x

Helper for Proposition 6.27.7: a finite local minimum of a convex function is already a global lower bound.

theorem localMinimumPoint_globalMinimizer_of_proper_convexFunction {n : ℕ} {f : (Fin n → ℝ) → WithTop ℝ} (hproper : (effectiveDomainWithTop f).Nonempty) (hf : IsConvexFunction f) {x : Fin n → ℝ} (hx : x ∈ effectiveDomainWithTop f) (hlocal : ∃ ε > 0, ∀ (z : Fin n → ℝ), ‖z - x‖ < ε → f z ≥ f x) : (∀ (y : Fin n → ℝ), f y ≥ f x) ∧ 0 ∈ subdifferentialAt (withTopFunctionToEReal f) x

Proposition 6.27.7 (A local minimum of a convex function is global): let f : ℝ^n → (-∞, +∞] be a proper convex function, and let x ∈ dom f. If x is a finite local minimum point of f, meaning that there exists ε > 0 such that f z ≥ f x whenever ‖z - x‖ < ε, then x is a global minimum point of f, so f y ≥ f x for every y ∈ ℝ^n. Consequently, 0 ∈ ∂f(x).