Magnitude conjecture

MagnitudeConjecture.Combinatorics.GradedIntervalCount

Counting shifts supported in a finite interval #

If an indecomposable graded module has least and greatest nonzero degrees l and u, its shift by t belongs to [0,m] exactly when -l ≤ t ≤ m-u. This file counts those shifts and bounds the exceptional target shifts outside the interior used for the arrow count.

source
def MagnitudeConjecture.GradedInterval.allowedShifts (m l u : ℕ) :
Finset ℤ

Shifts whose support endpoints lie in the interval [0,m].

Instances For
    source
    theorem MagnitudeConjecture.GradedInterval.mem_allowedShifts (m l u : ℕ) (t : ℤ) :
    t ∈ allowedShifts m l u ↔ 0 ≤ ↑l + t ∧ ↑u + t ≤ ↑m
    source
    theorem MagnitudeConjecture.GradedInterval.card_allowedShifts (m l u : ℕ) (hum : u ≤ m) :
    ↑(allowedShifts m l u).card = ↑m + 1 - (↑u - ↑l)

    Once the interval contains the unshifted support, its exact shift count is its length minus the support width.

    source
    theorem MagnitudeConjecture.GradedInterval.sum_card_allowedShifts {ι : Type u_1} (s : Finset ι) (l u : ι → ℕ) (m : ℕ) (hum : ∀ x ∈ s, u x ≤ m) :
    ∑ x ∈ s, ↑(allowedShifts m (l x) (u x)).card = ↑s.card * (↑m + 1) - ∑ x ∈ s, (↑(u x) - ↑(l x))

    Summing the individual counts gives a constant total width correction.

    source
    theorem MagnitudeConjecture.GradedInterval.allowedShifts_subset (m l u h : ℕ) (hlh : l ≤ h) :
    allowedShifts m l u ⊆ Finset.Icc (-↑h) ↑m

    All allowed shifts lie in the larger interval [-h,m].

    source
    theorem MagnitudeConjecture.GradedInterval.incoming_shift_allowed (m h l u : ℕ) (huh : u ≤ h) (s t : ℤ) (ht0 : 0 ≤ t) (htm : t ≤ ↑m - 2 * ↑h) (hst : t ≤ s) (hsth : s ≤ t + ↑h) :
    s ∈ allowedShifts m l u

    Interior targets contain all incoming supports with shift difference between zero and h, provided the original supports lie in [0,h].

    source
    theorem MagnitudeConjecture.GradedInterval.exceptional_shift_mem (m h : ℕ) (t : ℤ) (ht : t ∈ Finset.Icc (-↑h) ↑m) (hout : ¬(0 ≤ t ∧ t ≤ ↑m - 2 * ↑h)) :
    t ∈ Finset.Ico (-↑h) 0 ∪ Finset.Ioc (↑m - 2 * ↑h) ↑m

    Exceptional target shifts occur in two strips, whose total length is 3h; no assertion about preservation of irreducibles at these ends is used.

    source
    theorem MagnitudeConjecture.GradedInterval.boundary_strip_card_le (m h : ℕ) :
    (Finset.Ico (-↑h) 0 ∪ Finset.Ioc (↑m - 2 * ↑h) ↑m).card ≤ 3 * h

    The two boundary strips have uniformly bounded total cardinality, even when the interval is too short for the strips to be disjoint.

    source
    theorem MagnitudeConjecture.GradedInterval.exceptional_allowedShifts_card_le (m l u h : ℕ) (hlh : l ≤ h) :
    {t ∈ allowedShifts m l u | ¬(0 ≤ t ∧ t ≤ ↑m - 2 * ↑h)}.card ≤ 3 * h

    Each indecomposable label has at most 3h exceptional target shifts.