Ssreflect中如何快速推导事件F与非F的概率和为1并证明指定等式

核心思路 #

你当前待证明的等式完全不需要依赖“事件F和补集的概率和为1”的全局概率性质就能完成，核心突破口在两个指示项的局部逻辑关系：

• 等式左右两侧的公共因式为X i * P i，只要所处的代数结构（如实数域）满足消去律，就可以先将目标归约为证明括号内的两个条件表达式之和为1，完全用不上那两个关于Pr P F范围的假设H、H0
• 补集~: F的成员关系天然满足互斥穷尽性：对任意给定的i: U，i \in F和i \in ~: F不可能同真、也不可能同假，覆盖了所有可能的取值情况。

具体证明操作步骤 #

• 第一步调用Ssreflect内置的集合重写规则inE，将i \in ~: F转换为等价布尔表达式~~ (i \in F)，此时两个条件分支的判断条件恰好互为否定
• 第二步对布尔判断i \in F做分情况讨论：
  • 若判断为真：第一个条件表达式取指示值R1（即1），第二个因条件为假取R0（即0），二者求和为1
  • 若判断为假：第一个条件表达式取R0（即0），第二个因条件为真取R1（即1），二者求和仍为1
• 第三步将括号部分等于1的结论代回原式，利用乘法单位元性质a * 1 = a，即可直接推导出目标等式成立。

备注：你最初想推导的Pr P F + Pr P (~: F) = 1是概率测度的全局可加性结论，适用于全空间积分类的证明场景；本次待证等式是单采样点i上的指示函数计算，仅靠集合成员关系的局部性质就能快速完成推导，不需要引入全局概率测度的相关引理。

内容的提问来源于stack exchange，提问作者Fusen