OAI/Analysis/PeriodicLattice/Trigonometry.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Effective trigonometric values and derivative stencils.

  1. def OAI.PeriodicLattice.CertifiedReal.phaseCoeff line 18
  2. theorem OAI.PeriodicLattice.CertifiedReal.phaseCoeff_recursive line 22
  3. def OAI.PeriodicLattice.CertifiedReal.complexPart line 30
  4. def OAI.PeriodicLattice.CertifiedReal.trig line 32
  5. theorem OAI.PeriodicLattice.CertifiedReal.phaseCoeff_spec line 34
  6. theorem OAI.PeriodicLattice.CertifiedReal.complexPart_linear line 41
  7. theorem OAI.PeriodicLattice.CertifiedReal.trig_taylor line 47
  8. theorem OAI.PeriodicLattice.CertifiedReal.Effective.trig line 80
  9. theorem OAI.PeriodicLattice.CertifiedReal.Effective.sin line 123
  10. theorem OAI.PeriodicLattice.CertifiedReal.Effective.cos line 125
  11. theorem OAI.PeriodicLattice.CertifiedReal.Effective.cond line 135
  12. theorem OAI.PeriodicLattice.CertifiedReal.Effective.ite line 146
  13. def OAI.PeriodicLattice.CertifiedReal.refinePrecision line 153
  14. theorem OAI.PeriodicLattice.CertifiedReal.refinePrecision_recursive line 155
  15. theorem OAI.PeriodicLattice.CertifiedReal.error_refine line 158
  16. abbrev OAI.PeriodicLattice.CertifiedReal.Task line 166
  17. def OAI.PeriodicLattice.CertifiedReal.spawn line 168
  18. def OAI.PeriodicLattice.CertifiedReal.stencil line 172
  19. theorem OAI.PeriodicLattice.CertifiedReal.stencil_nil line 176
  20. theorem OAI.PeriodicLattice.CertifiedReal.stencil_cons line 178
  21. theorem OAI.PeriodicLattice.CertifiedReal.spawn_recursive line 181
  22. theorem OAI.PeriodicLattice.CertifiedReal.stencil_recursive line 192
  23. def OAI.PeriodicLattice.CertifiedReal.difference line 200
  24. theorem OAI.PeriodicLattice.CertifiedReal.stencil_correct line 206
  25. theorem OAI.PeriodicLattice.CertifiedReal.computable_list_sum line 223
  26. theorem OAI.PeriodicLattice.CertifiedReal.computable_list_map line 226
  27. theorem OAI.PeriodicLattice.CertifiedReal.difference_computable line 248