StabilizationBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.stabilization_reduction line 10
Source documentation
The parameter reduction in the induction on the outer symmetric degree.
```
theorem stabilization_reduction {a b : ℕ} (ha : 2 ≤ a)
    (hab : a * (a - 1) ≤ b) :
    let r := a - 1
…
```
theorem OAI.Problem346.first_shift_weight line 30
Source documentation
The first sequence of shifts has positive source-minus-destination weight.
```
theorem first_shift_weight {b r i : ℕ} (hir : i ≤ b - r)
    (hi : 1 ≤ i) : r < b - i + 1 := by
…
```

theorem OAI.Problem346.second_shift_weight_gap line 35

Source documentation

The shared destination variable remains at least two degrees below the source.

theorem second_shift_weight_gap {b r i j : ℕ}
    (hr : 1 ≤ r) (hb : r * (r + 1) ≤ b)
    (hi : 1 ≤ i) (hir : i ≤ r) (hj : j < r) :
    (i - 1) * r + j + 2 ≤ b - j := by
…

theorem OAI.Problem346.second_shift_weight line 47

Source documentation

The second sequence of shifts satisfies the strict injectivity inequality.

theorem second_shift_weight {b r i j : ℕ}
    (hr : 1 ≤ r) (hb : r * (r + 1) ≤ b)
    (hi : 1 ≤ i) (hir : i ≤ r) (hj : j < r) :
    (i - 1) * r + j < b - j := by
…

theorem OAI.Problem346.grid_shift_weight line 56

Source documentation

Arbitrary progress vectors, rather than only lexicographic schedules, satisfy the positive-weight inequality at every unfinished slot.

theorem grid_shift_weight {b r : ℕ} (hb : r * (r + 1) ≤ b)
    (counts : Fin r → ℕ) (hcounts : ∀ j, counts j ≤ r)
    (i : Fin r) (hi : counts i < r) :
    (∑ j, counts j) < b - counts i := by
…