Documentation

LeanPool.CCDN.AuxiliaryPolynomial.AffineAuxiliaryTranslationBound

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.