OAI/Analysis/PeriodicLattice/EffectiveReals.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Well-formed input encodings and effective real enclosures.

  1. theorem OAI.PeriodicLattice.RecursiveArithmetic.rat_abs line 18
  2. theorem OAI.PeriodicLattice.RecursiveArithmetic.ratLE line 23
  3. theorem OAI.PeriodicLattice.RecursiveArithmetic.ratLT line 27
  4. theorem OAI.PeriodicLattice.RecursiveArithmetic.rat_floor line 30
  5. theorem OAI.PeriodicLattice.RecursiveArithmetic.listSumRat line 33
  6. theorem OAI.PeriodicLattice.RecursiveArithmetic.sumRangeRat line 38
  7. theorem OAI.PeriodicLattice.RecursiveArithmetic.allList line 43
  8. theorem OAI.PeriodicLattice.RecursiveArithmetic.machineTable line 49
  9. theorem OAI.PeriodicLattice.RecursiveArithmetic.instructionState line 51
  10. theorem OAI.PeriodicLattice.RecursiveArithmetic.instructionSymbol line 53
  11. theorem OAI.PeriodicLattice.RecursiveArithmetic.instructionMove line 55
  12. theorem OAI.PeriodicLattice.RecursiveArithmetic.entryValid line 58
  13. theorem OAI.PeriodicLattice.RecursiveArithmetic.machineWellFormed line 73
  14. theorem OAI.PeriodicLattice.RecursiveArithmetic.inputWellFormed line 85
  15. abbrev OAI.PeriodicLattice.ValidInput line 91
  16. def OAI.PeriodicLattice.CertifiedReal.error line 99
  17. def OAI.PeriodicLattice.CertifiedReal.qerror line 100
  18. theorem OAI.PeriodicLattice.CertifiedReal.cast_qerror line 102
  19. theorem OAI.PeriodicLattice.CertifiedReal.error_pos line 103
  20. theorem OAI.PeriodicLattice.CertifiedReal.error_le_one line 104
  21. theorem OAI.PeriodicLattice.CertifiedReal.error_tendsto line 105
  22. theorem OAI.PeriodicLattice.CertifiedReal.qerror_primrec line 108
  23. def OAI.PeriodicLattice.CertifiedReal.Effective line 110
  24. theorem OAI.PeriodicLattice.CertifiedReal.computable_find line 116
  25. theorem OAI.PeriodicLattice.CertifiedReal.of_enclosures line 129
  26. theorem OAI.PeriodicLattice.CertifiedReal.Effective.comp line 151
  27. theorem OAI.PeriodicLattice.CertifiedReal.Effective.congr line 157
  28. theorem OAI.PeriodicLattice.CertifiedReal.rational line 160
  29. theorem OAI.PeriodicLattice.CertifiedReal.Effective.approximants_tendsto line 164
  30. theorem OAI.PeriodicLattice.CertifiedReal.constant line 184
  31. theorem OAI.PeriodicLattice.CertifiedReal.Effective.add line 186
  32. theorem OAI.PeriodicLattice.CertifiedReal.Effective.neg line 198
  33. theorem OAI.PeriodicLattice.CertifiedReal.Effective.sub line 204
  34. theorem OAI.PeriodicLattice.CertifiedReal.Effective.mul line 207