MRTInputsTheorem.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The corrected short exponential-sum estimates of Matomäki, Radziwiłł, and Tao in the specializations used for ordinary two-point correlations.

theorem OAI.TwoPointCorrelations.mrtShortExponentialInput line 12
Source documentation
Corrected MRT (2015), Theorem 1.7, in the application specialization.
```
theorem mrtShortExponentialInput : MRTShortExponentialInput :=
…
```
Mentions: OAI.TwoPointCorrelations.MRTShortExponentialInput
theorem OAI.TwoPointCorrelations.mrtLiouvilleShortInput line 16
Source documentation
Corrected MRT (2015), Theorem 1.3, in the application specialization.
```
theorem mrtLiouvilleShortInput : MRTLiouvilleShortInput :=
…
```
Mentions: OAI.TwoPointCorrelations.MRTLiouvilleShortInput