Positive-axis minimum or right-endpoint liminf dichotomy under continuity and coercivity

Proved

AvramDividend.Classical.positive_minimum_or_right_liminf_of_tendsto_atTop

by WillR · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

avram-dividendcalculuscoercivitycstar-finiteliminfminimumroot-prerequisite

For a real-valued function continuous on (0,∞) and tending to +∞ at +∞, either its global positive-axis minimum is attained or its EReal right liminf at zero is no larger than every positive value. This is precisely the deterministic dichotomy in AvramDividend.Classical.scaleDeriv_inf_attained after setting f = deriv W and identifying derivZeroPlus. Its proof was previously private inside the canonical Proved cstar finiteness bridge, and this theorem exposes that verified compactness argument for direct reuse.

Preamble

import Theorems.Thm_AvramDividend_Classical_cstar_lt_top_of_deriv_continuous_tendsto_atTop

open Filter Set Topology
open scoped ENNReal

Formal statement

theorem AvramDividend.Classical.positive_minimum_or_right_liminf_of_tendsto_atTop
    (f : ℝ → ℝ)
    (hcont : ContinuousOn f (Ioi 0))
    (htop : Tendsto f atTop atTop) :
    (∃ a : ℝ, 0 < a ∧ ∀ x : ℝ, 0 < x → f a ≤ f x) ∨
      ∀ x : ℝ, 0 < x →
        Filter.liminf (fun y => (f y : EReal)) (𝓝[>] (0 : ℝ)) ≤
          (f x : EReal) := by sorry

Source

The canonically Proved cstar_lt_top_of_deriv_continuous_tendsto_atTop, accepted submission ee363315-f06b-4854-a662-9282e3f92a2c, previously contained this private 40-line proof. Republished verbatim as a reusable generic theorem.

View graph