OAI/NumberTheory/TwoPoint/MainWithMRTInputs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The three manuscript main results after discharging both prime inputs and the fixed-depth Braverman input. Only the published MRT inputs remain.

  1. theorem OAI.TwoPointCorrelations.liouvilleLogSaving_of_mrt line 11
  2. theorem OAI.TwoPointCorrelations.binaryCorrectedElliott_of_mrt line 14
  3. theorem OAI.TwoPointCorrelations.affineCorrectedElliott_of_mrt line 17