Translating the affine box by a vector bounded by the degree costs only a dimension constant in the coefficient-sensitive minimum bound.
theorem
CCDN.affineMinimumAuxiliaryBound_translation
{n d : ℕ}
(hd : 0 < d)
{A B L b : ℝ}
(hA : 0 ≤ A)
(hB : 1 ≤ B)
(hL : 1 ≤ L)
(hb : 0 ≤ b)
:
affineMinimumAuxiliaryBound n d A (B + ↑d) L b ≤ 2 * Real.exp (↑n + 2) * affineMinimumAuxiliaryBound n d A B L b
Specialization to the common minimum bound used by both affine branches.