次回予告

　次回からは，fが区間[0,1]で連続のとき
\lim_{n\to\infty}\int_{0}^{1}f(x)|\sin{n \pi x}| dx=\frac{2}{\pi}\int_{0}^{1}f(x)dx
の証明を進めます．
　証明の流れは，区間を等分して，積分の平均値定理，絶対値との順序交換，リーマン和の極限といったものです．
\sum_{k=1}^{n}\int_{(k-1)/n}^{k/n}f(x)|\sin{n \pi x}| dx=\sum_{k=1}^{n}f(x_k)\int_{(k-1)/n}^{k/n}|\sin{n \pi x}| dx=\frac{2}{\pi}\cdot\frac{1}{n}\sum_{k=1}^{n}f(x_k)
　本格的な積分の証明には，"Multivariate/realanalysis.ml"あたりが入用ですが，今回程度なら"Library/transc.ml"＋自作で賄えそうです．なお，HOL Lightは，所謂，ゲージ積分(http://www.math.vanderbilt.edu/~schectex/ccc/gauge/)(http://www.resource-aware.org/twiki/pub/Teaching/617References_Fall09/Theorem-Proving-with-the-Real-Numbers.pdf 3.6)を採用しています．