The positive infimum of a continuous global-argmin set is zero or remains a minimiser

Proved

AvramDividend.Classical.continuous_argmin_sInf_zero_or_minimal

by WillR · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

real-analysissource-neutral-childtopology

For a continuous real function on the positive half-line, let S be the set of positive global minimisers. If S is nonempty, then inf S is either zero or is itself a positive global minimiser. This is the pure closure-of-argmin step needed to identify c* with a derivative minimiser.

Preamble

import Mathlib

open Filter Set Topology

Formal statement

namespace AvramDividend.Classical

theorem continuous_argmin_sInf_zero_or_minimal (f : ℝ → ℝ)
    (hcont : ContinuousOn f (Ioi 0))
    (hne : {a : ℝ | 0 < a ∧ ∀ x : ℝ, 0 < x → f a ≤ f x}.Nonempty) :
    sInf {a : ℝ | 0 < a ∧ ∀ x : ℝ, 0 < x → f a ≤ f x} = 0 ∨
      (0 < sInf {a : ℝ | 0 < a ∧ ∀ x : ℝ, 0 < x → f a ≤ f x} ∧
        ∀ x : ℝ, 0 < x →
          f (sInf {a : ℝ | 0 < a ∧ ∀ y : ℝ, 0 < y → f a ≤ f y}) ≤ f x) := by sorry

end AvramDividend.Classical

Source

Elementary real analysis: csInf_mem_closure for the positive argmin set, sequential characterization of closure in ℝ, and continuity of f on (0,∞).

View graph