OAI/NumberTheory/TwoPoint/PartiallyDischargedMain.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

All three main statements with the two proved prime-distribution inputs discharged. Only the circuit and MRT inputs remain parameters.

  1. theorem OAI.TwoPointCorrelations.liouvilleLogSaving_of_circuit_mrt line 12
  2. theorem OAI.TwoPointCorrelations.binaryCorrectedElliott_of_circuit_mrt line 16
  3. theorem OAI.TwoPointCorrelations.affineCorrectedElliott_of_circuit_mrt line 20