OAI/Analysis/PeriodicLattice/ElementaryFunctions.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Certified effective inversion, powers and exponential evaluation.

  1. theorem OAI.PeriodicLattice.CertifiedReal.Effective.abs line 20
  2. theorem OAI.PeriodicLattice.CertifiedReal.Effective.inv line 26
  3. theorem OAI.PeriodicLattice.CertifiedReal.Effective.div line 79
  4. theorem OAI.PeriodicLattice.CertifiedReal.Effective.pow line 82
  5. theorem OAI.PeriodicLattice.CertifiedReal.computable_sum line 113
  6. theorem OAI.PeriodicLattice.CertifiedReal.rat_abs_bound line 126
  7. theorem OAI.PeriodicLattice.CertifiedReal.Effective.exp line 133
  8. theorem OAI.PeriodicLattice.CertifiedReal.piTerm_recursive line 213
  9. theorem OAI.PeriodicLattice.CertifiedReal.piApprox_recursive line 219
  10. theorem OAI.PeriodicLattice.CertifiedReal.pi line 225