OAI/Geometry/SmoothYau/Smoothness/GlobalPrepDualNorm.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.smooth_translate line 17
  2. lemma OAI.YauCounterexamples.fderiv_translate line 20
  3. theorem OAI.YauCounterexamples.preparation_remainder_uniform_phase line 26
  4. def OAI.YauCounterexamples.preparationCorrugation line 70
  5. lemma OAI.YauCounterexamples.preparationCorrugation_smooth line 74
  6. theorem OAI.YauCounterexamples.preparation_C1_uniform_phase line 80
  7. def OAI.YauCounterexamples.preparationWave line 173
  8. def OAI.YauCounterexamples.preparationWaveFirst line 175
  9. def OAI.YauCounterexamples.preparationWaveSecond line 177
  10. lemma OAI.YauCounterexamples.preparationWave_smooth line 179
  11. lemma OAI.YauCounterexamples.preparationWave_hasDeriv line 182
  12. lemma OAI.YauCounterexamples.preparationWaveFirst_hasDeriv line 192
  13. lemma OAI.YauCounterexamples.preparationWave_deriv line 203
  14. lemma OAI.YauCounterexamples.preparationWave_second line 207
  15. lemma OAI.YauCounterexamples.preparationWave_abs_bound line 212
  16. lemma OAI.YauCounterexamples.preparationWave_deriv_bound line 217
  17. lemma OAI.YauCounterexamples.preparationWave_second_bound line 223
  18. lemma OAI.YauCounterexamples.preparationWaveSecond_smooth line 228
  19. lemma OAI.YauCounterexamples.preparationWave_periodic line 231
  20. lemma OAI.YauCounterexamples.preparationWaveSecond_periodic line 236
  21. lemma OAI.YauCounterexamples.scalar_second_fderiv line 241
  22. def OAI.YauCounterexamples.actualCoordinateNorm line 277
  23. def OAI.YauCounterexamples.actualProfileSpeed line 280
  24. lemma OAI.YauCounterexamples.actualCoordinateNorm_eq line 284
  25. lemma OAI.YauCounterexamples.actualProfileSpeed_eq line 292
  26. lemma OAI.YauCounterexamples.actualCoordinateNorm_nonneg line 300
  27. lemma OAI.YauCounterexamples.actualCoordinateNorm_pos line 304
  28. lemma OAI.YauCounterexamples.continuous_actualCoordinateNorm line 308
  29. lemma OAI.YauCounterexamples.continuous_actualProfileSpeed line 312
  30. lemma OAI.YauCounterexamples.actualCoordinateNorm_abs_sub line 317
  31. theorem OAI.YauCounterexamples.compact_actual_gradient_error line 323
  32. lemma OAI.YauCounterexamples.compact_actual_speed_pos line 365
  33. lemma OAI.YauCounterexamples.actualJet_eventuallyEq line 374
  34. lemma OAI.YauCounterexamples.preparationCorrugation_eventuallyEq line 390
  35. lemma OAI.YauCounterexamples.preparationCorrugation_tsupport line 397
  36. lemma OAI.YauCounterexamples.disjoint_sum_eventuallyEq line 407
  37. theorem OAI.YauCounterexamples.compact_relative_gradient_tolerance line 432