Explicit coefficient-height bounds for the bounded integral shear.

theorem CCDN.bivariateShear_bounded_coefficient_bound (a d : ℕ) (ha : a ≤ d) (f : Polynomial (Polynomial ℤ)) (hd : bivariateTotalDegree f ≤ d) (H : ℝ) (hH : 0 ≤ H) (hf : BivariateCoefficientBound f H) : BivariateCoefficientBound ((bivariateShear ℤ ↑a) f) ((↑d + 1) ^ (d + 2) * H)

For the selected parameter 0<=a<=d, the sheared height is at most H*(d+1)^(d+2), hence its logarithm costs only O(d log d).