Surplus in terms of vertex, arrow and projective counts #
theorem
MagnitudeConjecture.ARCount.surplus_eq_counts
{ι : Type u}
[Fintype ι]
(a : ι → ι → ℕ)
(P : ι → Prop)
[DecidablePred P]
:
surplus a P = 2 * vertexCount - arrowCount a - 2 * projectiveCount P
The surplus is twice the vertex count, less arrows and twice the projective count.
theorem
MagnitudeConjecture.GradedInterval.surplus_error_of_exact_counts
(N Nm p pm m : ℕ)
(a am W C : ℤ)
(hN : ↑Nm = ↑N * (↑m + 1) - W)
(ha : |am - (↑m + 1) * a| ≤ C)
(hp : pm = p * (m + 1))
:
|2 * ↑Nm - am - 2 * ↑pm - (↑m + 1) * (2 * ↑N - a - 2 * ↑p)| ≤ 2 * |W| + C
Exact object and simple counts together with the arrow error give the surplus error, with a fixed support-width correction.