[2/3] 我还有最后三个（相似的）小引理就完成了随机变量依分布收敛的一个重要等价定理，进而相当于完成首个超越 I.I.D. (独立同分布) 情形的更复杂的中心极限定理（CLT）的形式化证明了，HOL4 重夺兵器谱排名第一位（之前 Isabelle/HOL 下有人完成了中心极限定理的 I.I.D. 版本，那个基于特征函数的证明在教科书上只有一行。）这三个引理不好证，但我无论怎么看都是可证明的真命题（这就已经谢天谢地了！），总算是找到了一条可行的路径。