Main.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Paper 009-01: the three original main results, unconditionally.

theorem OAI.TwoPointCorrelations.liouvilleLogSaving line 10
Source documentation
Theorem 1.1: ordinary Liouville correlations with an absolute logarithmic saving.
```
theorem liouvilleLogSaving : LiouvilleLogSaving :=
…
```
Mentions: OAI.TwoPointCorrelations.LiouvilleLogSaving
theorem OAI.TwoPointCorrelations.binaryCorrectedElliott line 14
Source documentation
Theorem 1.2: the binary corrected Elliott theorem.
```
theorem binaryCorrectedElliott : BinaryCorrectedElliott :=
…
```
Mentions: OAI.TwoPointCorrelations.BinaryCorrectedElliott
theorem OAI.TwoPointCorrelations.affineCorrectedElliott line 18
Source documentation
Corollary 1.3: the corrected Elliott theorem for nonproportional affine forms.
```
theorem affineCorrectedElliott : AffineCorrectedElliott :=
…
```
Mentions: OAI.TwoPointCorrelations.AffineCorrectedElliott