MathCompの `analysis` リポジトリを見る：

* 参考： [GitHub - math-comp/analysis: Mathematical Components compliant Analysis Library](https://github.com/math-comp/analysis)

## `cardinality.v`

以下の素朴集合論に基づく集合の濃度に関する定式化．

## `classical_sets.v`

素朴集合論の定式化．

## `constructive_ereal.v`

“Extended real numbers” の理論．具体的には $\mathbf{R}$ に $+\infty$ と $-\infty$ を加えて拡張したもの．

**測度論の水準の確率論ではこの種の集合は頻出するので関係しそうではある．**

## `exp.v`

指数・対数に関する定義や定理など．600行程度．

## `forms.v`

冒頭にコメントがないため何をやっているファイルかすぐにはわからない．数百行程度のコードで，コメントアウトが多い．

## `fsbigop.v`

“Finitely-supported big operators” についての定式化らしい．おそらく添字が有限集合を動く $∑$ や $⋃$ などのこと．

**標本空間が有限集合の場合は移植に利用できそう（というかAffeldt先生の実装が使っていたかも？ 要確認）．**

## `functions.v`

プログラムの意味の函数を数学の意味の函数として扱った定理集？（始域と終域は，その型に対応するsetが定式化に用いられているらしい）

単射・全射といった基礎的な命題が定義されていたりする．

## `landau.v`

漸近記法，いわゆる big-O など．

## `lebesgue_integral.v`

Lebesgue積分に関する定式化．かなり長い（5000行ほどある）．冒頭のコメントによるとFatouの補題やFubiniの定理などまで示しているらしい．

## `lebesgue_measure.v`

Lebesgue測度の定式化．1800行程度．そのまま `lebesgue_measure` という名前でLebesgue測度が定義されている．

冒頭のコメントによると `measure.v` で示されているCaratheodoryの定理を使っているらしい．

## `mathcomp_extra.v`

ユーティリティ的なもの．800行くらい．

## `measure.v`

測度論に関する基礎的な理論の定式化．3500行程度ある．Caratheodoryの定理を示している．

**確率論の定式化の話としては結構近いのではないかと思う．**

## `reals.v`

実数の公理化．