什么是重写的最佳方式\sum_(i...) (F i - G i)
是(\sum_(i...) F i - \sum_(i...) G i)
与序数bigop
,假设下溢得到妥善管理?
更准确地说,关于这些下溢,我对以下引理感兴趣:
Lemma big_split_subn (n : nat) (P : 'I_n -> bool) (F G : 'I_n -> nat) :
(forall i : 'I_n, P i -> G i <= F i) ->
\sum_(i < n | P i) (F i - G i) = \sum_(i < n | P i) F i - \sum_(i < n | P i) G i.
似乎big_split …