如何解决比较总和 ssreflect
我的目标是说,如果我们有
sum(a) = sum(b)
然后
a = b.
如果目标是这样的,那么合适的策略是什么:
\big[Radd_comoid/0]_(i <- fin_img (A:=U) (B:=R_eqType) X)
Radd_comoid
(Pr P F * (i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: F) / Pr P F))
(Pr P (~: F) *
(i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: ~: F) / Pr P (~: F))) =
\sum_(u in U) X u * `p_ X u
已编辑。 上下文包含:
X: {RV (P) -> (R)}
F: {set U}
H: 0 < Pr P F
H0: Pr P F < 1
rewrite /=.
之后的目标如下所示:
\big[Rplus/0]_(i <- fin_img (A:=U) (B:=R_eqType) X)
(Pr P F * (i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: F) / Pr P F) +
Pr P (~: F) *
(i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: ~: F) / Pr P (~: F))) =
\sum_(u in U) X u * `p_ X u
解决方法
如果是这样,您可能需要在右侧使用 sum_parti_finType
并尝试使用 eq_bigr
确定求和的一般项。可以在 mulrC mulfVK
的两侧使用 +
(或类似的东西)来简化左侧的通用术语。然后用不相交联合的概率确定概率之和。
无论如何,这不仅仅是“一种战术”......