Statements.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TwoPointCorrelations.LiouvilleLogSaving line 13
Source documentation
Theorem 1.1 (thm:q-affine) of the manuscript, through all real cutoffs, with a single exponent independent of the four affine coefficients.
```
def LiouvilleLogSaving : Prop :=
…
```
def OAI.TwoPointCorrelations.BinaryCorrectedElliott line 22
Source documentation
Theorem 1.2 (thm:elliott): the factors are ordinary multiplicative functions; either original factor satisfies the growing-height condition.
```
def BinaryCorrectedElliott : Prop :=
…
```
def OAI.TwoPointCorrelations.AffineCorrectedElliott line 30
Source documentation
Corollary 1.3 (cor:affine), including coefficients sharing prime factors.
```
def AffineCorrectedElliott : Prop :=
…
```