OAI/Probability/SATComputability/EffectiveLog.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PeriodicLattice.CertifiedReal.logLower line 16
2. def OAI.PeriodicLattice.CertifiedReal.logUpper line 17
3. def OAI.PeriodicLattice.CertifiedReal.logAccuracy line 18
4. theorem OAI.PeriodicLattice.CertifiedReal.logLower_computable line 20
5. theorem OAI.PeriodicLattice.CertifiedReal.logUpper_computable line 23
6. theorem OAI.PeriodicLattice.CertifiedReal.logAccuracy_computable line 26
7. abbrev OAI.PeriodicLattice.CertifiedReal.logTest line 30
8. instance OAI.PeriodicLattice.CertifiedReal.logTest_decidable line 35
9. theorem OAI.PeriodicLattice.CertifiedReal.logTest_computable line 38
10. theorem OAI.PeriodicLattice.CertifiedReal.logTest_exists line 50
11. theorem OAI.PeriodicLattice.CertifiedReal.logTest_sound line 84
12. theorem OAI.PeriodicLattice.CertifiedReal.Effective.log line 120