OAI/Geometry/SmoothYau/Smoothness/WaveDeriv.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.waveDeriv line 31
  2. theorem OAI.YauCounterexamples.waveDeriv_mul line 33
  3. theorem OAI.YauCounterexamples.waveDeriv_add line 40
  4. theorem OAI.YauCounterexamples.waveDeriv_const_mul line 45
  5. theorem OAI.YauCounterexamples.contDiff_waveDeriv line 52
  6. theorem OAI.YauCounterexamples.waveDeriv_exp line 56
  7. def OAI.YauCounterexamples.waveCoordinateOperator line 66
  8. def OAI.YauCounterexamples.waveGradientPair line 71
  9. theorem OAI.YauCounterexamples.waveSecondDeriv_exp_mul line 75
  10. theorem OAI.YauCounterexamples.waveCoordinateOperator_exp_mul line 104
  11. theorem OAI.YauCounterexamples.gaussianEnvelope_moment line 128
  12. theorem OAI.YauCounterexamples.gaussianEnvelope_scaled_moment line 149