[3/3] 话说去年底回国前夕我的形式化证明（中心极限定理的一部分）卡在一个可以交换偏导数和积分号的 “小” 定理上，但是我在《Measures, Integrals and Martingales》那本书里找到的版本带有苛刻的前置条件，在应用的时候根本无法满足。1月中旬的时候无意中在同一本书的某章习题部分找到了另一个版本，前置条件更复杂但可以满足。但是这个定理的证明太繁琐了，同时用到 Gauge 积分那边的微积分基本定理、勒贝格积分这边的富比尼定理、以及两个积分系统的等价性定理（后两个也都是我形式化的）。我歇了两个月，现在不得不重操旧业继续证下去了。举步维艰。