Exact finite-product expansion of the spatial drift correction.

theorem AVenhance.Infra.Section4.DriftCommutatorExpansion.amnrDriftTerms_derivative_sum {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) (T : List AmnrDriftTerm) : amnrOp b (some i) (List.map (amnrDriftTermValue b f) T).sum = (List.map (amnrDriftTermValue b f) (List.flatMap (amnrDriftDerivativeTerms i) T)).sum