Exact support endpoints and allowed shifts

structure MagnitudeConjecture.GradedInterval.SupportWindow (D : Finset ℤ) : Type

Natural endpoints of a finite nonnegative support, attained in that support.

• lower : ℕ
• upper : ℕ
• lower_mem : ↑self.lower ∈ D
• upper_mem : ↑self.upper ∈ D
• bounds (d : ℤ) : d ∈ D → ↑self.lower ≤ d ∧ d ≤ ↑self.upper

def MagnitudeConjecture.GradedInterval.SupportWindow.ofNonnegative (D : Finset ℤ) (hne : D.Nonempty) (hpos : ∀ d ∈ D, 0 ≤ d) : SupportWindow D

A finite nonempty nonnegative support has exact natural endpoints.

theorem MagnitudeConjecture.GradedInterval.SupportWindow.lower_le_upper {D : Finset ℤ} (W : SupportWindow D) : W.lower ≤ W.upper

theorem MagnitudeConjecture.GradedInterval.SupportWindow.shift_supported_iff {D : Finset ℤ} (W : SupportWindow D) (m : ℕ) (t : ℤ) : (∀ d ∈ D, 0 ≤ d + t ∧ d + t ≤ ↑m) ↔ t ∈ allowedShifts m W.lower W.upper

Support containment after a shift is exactly the allowed-shift condition.