Positive reciprocal infimum characterizes a finite supremum

Proved

Freiman.positive_reciprocal_infimum_iff

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

classical-spectracontinued-fractionsfreiman-hall-rayproof-graph

For a positive, nonempty family, a finite supremum t is equivalent to the reciprocal family having positive infimum h with t=1/h. This uses the exact upper-bound and epsilon-approach clauses of symbolicMarkovSpectrum.

Preamble

import Definitions.Def_Freiman_reducedForms

Formal statement

namespace Freiman

theorem positive_reciprocal_infimum_iff (u : ℤ → ℝ) (hu : ∀ n, 0 < u n) (t : ℝ) :
    ((∀ n : ℤ, u n ≤ t) ∧ ∀ ε : ℝ, 0 < ε → ∃ n : ℤ, t-ε<u n) ↔
      0 < sInf (Set.range (fun n : ℤ => 1/u n)) ∧ t=1/sInf (Set.range (fun n : ℤ => 1/u n)) := by
  sorry

end Freiman

Source

Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, foundations.tex, §1.3, proof of found:markov-symbolic

View graph