gap centered membership
ProvedFreiman.gap_centered_membershipfreimangaphall-ray
An attained global height satisfies both clauses of the existing symbolic Markov-spectrum definition.
Preamble
import Definitions.Def_Freiman_gapModel
Formal statement
namespace Freiman theorem gap_centered_membership (a : ℤ → ℕ+) (t : ℝ) (hmax : ∀ i, localValue a i ≤ t) (h0 : localValue a 0 = t) : t ∈ symbolicMarkovSpectrum := by sorry end Freiman
Source
Freiman Hall ray report, m3.tex; thm:m3:gap