Total exceptional targets in a finite family of support windows

def MagnitudeConjecture.GradedInterval.sigmaFinsetFilterEquiv {ι : Type u} (F : ι → Finset ℤ) (P : ι → ℤ → Prop) [(i : ι) → DecidablePred (P i)] : { a : (i : ι) × ↥(F i) // P a.fst ↑a.snd } ≃ (i : ι) × ↥(Finset.filter (P i) (F i))

Filtering a finite family of finite sets is equivalent to filtering each fibre.

theorem MagnitudeConjecture.GradedInterval.sigmaFinset_filter_card_le {ι : Type u} [Fintype ι] (F : ι → Finset ℤ) (P : ι → ℤ → Prop) [(i : ι) → DecidablePred (P i)] (B : ℕ) (hB : ∀ (i : ι), (Finset.filter (P i) (F i)).card ≤ B) : Nat.card { a : (i : ι) × ↥(F i) // P a.fst ↑a.snd } ≤ Fintype.card ι * B

Summing uniform fibre bounds bounds the whole exceptional label set.

theorem MagnitudeConjecture.GradedInterval.total_exceptional_allowedShifts_card_le {ι : Type u} [Fintype ι] (m h : ℕ) (l r : ι → ℕ) (hl : ∀ (i : ι), l i ≤ h) : Nat.card { a : (i : ι) × ↥(allowedShifts m (l i) (r i)) // ¬(0 ≤ ↑a.snd ∧ ↑a.snd ≤ ↑m - 2 * ↑h) } ≤ Fintype.card ι * (3 * h)

At most 3h boundary targets occur for each original label, uniformly in m.