OAI/Analysis/PeriodicLattice/ProfileJets.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Explicit jets and uniform profile derivative estimates.

  1. def OAI.PeriodicLattice.ProfileJets.rhoTerm line 19
  2. theorem OAI.PeriodicLattice.ProfileJets.rhoTerm_contDiff line 21
  3. theorem OAI.PeriodicLattice.ProfileJets.rhoTerm_hasDerivAt line 26
  4. theorem OAI.PeriodicLattice.ProfileJets.rhoTerm_bound line 39
  5. theorem OAI.PeriodicLattice.ProfileJets.denominator_lower line 50
  6. def OAI.PeriodicLattice.ProfileJets.denomInv line 65
  7. theorem OAI.PeriodicLattice.ProfileJets.denomInv_contDiff line 68
  8. theorem OAI.PeriodicLattice.ProfileJets.denomInv_bound line 72
  9. theorem OAI.PeriodicLattice.ProfileJets.denomInv_hasDerivAt line 77
  10. abbrev OAI.PeriodicLattice.ProfileJets.Factor line 96
  11. abbrev OAI.PeriodicLattice.ProfileJets.Term line 97
  12. abbrev OAI.PeriodicLattice.ProfileJets.Expr line 98
  13. def OAI.PeriodicLattice.ProfileJets.evalFactor line 100
  14. def OAI.PeriodicLattice.ProfileJets.evalProduct line 104
  15. def OAI.PeriodicLattice.ProfileJets.evalTerm line 106
  16. def OAI.PeriodicLattice.ProfileJets.eval line 108
  17. def OAI.PeriodicLattice.ProfileJets.factorBound line 110
  18. def OAI.PeriodicLattice.ProfileJets.productBound line 112
  19. def OAI.PeriodicLattice.ProfileJets.termBound line 114
  20. def OAI.PeriodicLattice.ProfileJets.bound line 116
  21. theorem OAI.PeriodicLattice.ProfileJets.evalFactor_bound line 118
  22. theorem OAI.PeriodicLattice.ProfileJets.evalProduct_bound line 124
  23. theorem OAI.PeriodicLattice.ProfileJets.evalTerm_bound line 131
  24. theorem OAI.PeriodicLattice.ProfileJets.eval_bound line 134
  25. def OAI.PeriodicLattice.ProfileJets.multPrefix line 141
  26. def OAI.PeriodicLattice.ProfileJets.diffFactor line 144
  27. def OAI.PeriodicLattice.ProfileJets.diffProduct line 152
  28. def OAI.PeriodicLattice.ProfileJets.diffTerm line 156
  29. def OAI.PeriodicLattice.ProfileJets.diff line 158
  30. theorem OAI.PeriodicLattice.ProfileJets.eval_nil line 160
  31. theorem OAI.PeriodicLattice.ProfileJets.eval_cons line 162
  32. theorem OAI.PeriodicLattice.ProfileJets.eval_append line 165
  33. theorem OAI.PeriodicLattice.ProfileJets.evalProduct_nil line 168
  34. theorem OAI.PeriodicLattice.ProfileJets.evalProduct_cons line 170
  35. theorem OAI.PeriodicLattice.ProfileJets.evalProduct_append line 173
  36. theorem OAI.PeriodicLattice.ProfileJets.eval_multPrefix line 177
  37. theorem OAI.PeriodicLattice.ProfileJets.diffFactor_correct line 187
  38. theorem OAI.PeriodicLattice.ProfileJets.diffProduct_correct line 207
  39. theorem OAI.PeriodicLattice.ProfileJets.diffTerm_correct line 216
  40. theorem OAI.PeriodicLattice.ProfileJets.diff_correct line 221
  41. def OAI.PeriodicLattice.ProfileJets.jet line 228
  42. theorem OAI.PeriodicLattice.ProfileJets.jet_correct line 230
  43. def OAI.PeriodicLattice.ProfileJets.clockExpr line 239
  44. def OAI.PeriodicLattice.ProfileJets.bumpExpr line 241
  45. theorem OAI.PeriodicLattice.ProfileJets.eval_clockExpr line 244
  46. theorem OAI.PeriodicLattice.ProfileJets.eval_bumpExpr line 249
  47. def OAI.PeriodicLattice.ProfileJets.pulseBound line 255
  48. def OAI.PeriodicLattice.ProfileJets.bumpBound line 257
  49. theorem OAI.PeriodicLattice.ProfileJets.pulseBound_spec line 259
  50. theorem OAI.PeriodicLattice.ProfileJets.bumpBound_spec line 264