Exact weighted count of interior shifts

theorem MagnitudeConjecture.GradedInterval.interior_subset_allowedShifts (m h l r : ℕ) (hr : r ≤ h) : Finset.Icc 0 (↑m - 2 * ↑h) ⊆ allowedShifts m l r

The common interior interval is contained in every bounded support window.

theorem MagnitudeConjecture.GradedInterval.interior_weighted_sum {ι : Type u_1} [Fintype ι] (m h : ℕ) (l r : ι → ℕ) (hr : ∀ (i : ι), r i ≤ h) (hm : 2 * h ≤ m) (w : ι → ℕ) : ∑ a : { a : (i : ι) × ↥(allowedShifts m (l i) (r i)) // 0 ≤ ↑a.snd ∧ ↑a.snd ≤ ↑m - 2 * ↑h }, w (↑a).fst = (m - 2 * h + 1) * ∑ i : ι, w i

Each ordinary label contributes once for each of the m-2h+1 interior shifts.