OAI/Geometry/SmoothYau/Smoothness/ProfilePeriodizeEventuallyZero.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.YauCounterexamples.ProfilePlane line 18
  2. abbrev OAI.YauCounterexamples.ProfileLattice line 19
  3. def OAI.YauCounterexamples.profileLatticePoint line 21
  4. lemma OAI.YauCounterexamples.profileLatticePoint_add line 23
  5. lemma OAI.YauCounterexamples.profileLattice_embedding line 27
  6. theorem OAI.YauCounterexamples.profile_translates_locallyFinite line 30
  7. def OAI.YauCounterexamples.profilePeriodize line 55
  8. theorem OAI.YauCounterexamples.profilePeriodize_smooth line 58
  9. theorem OAI.YauCounterexamples.profilePeriodize_periodic line 64
  10. def OAI.YauCounterexamples.radialPrimitive line 92
  11. lemma OAI.YauCounterexamples.radialPrimitive_hasDeriv line 94
  12. lemma OAI.YauCounterexamples.radialPrimitive_smooth line 98
  13. lemma OAI.YauCounterexamples.radialPrimitive_zero line 106
  14. lemma OAI.YauCounterexamples.radialPrimitive_constant line 116
  15. theorem OAI.YauCounterexamples.exists_radial_derivative line 131
  16. def OAI.YauCounterexamples.radialSquaredBase line 138
  17. lemma OAI.YauCounterexamples.radialSquaredBase_smooth line 141
  18. lemma OAI.YauCounterexamples.radialSquaredBase_zero line 146
  19. lemma OAI.YauCounterexamples.radialSquaredBase_compact line 151
  20. theorem OAI.YauCounterexamples.radial_periodic_smooth line 167
  21. lemma OAI.YauCounterexamples.profileRadiusSquared_hasFDeriv line 192
  22. theorem OAI.YauCounterexamples.radialSquaredBase_first line 200
  23. theorem OAI.YauCounterexamples.radialSquaredBase_second line 212
  24. lemma OAI.YauCounterexamples.profilePeriodize_eventually_zero line 246
  25. lemma OAI.YauCounterexamples.profilePeriodize_jets_zero line 263
  26. def OAI.YauCounterexamples.planeRadialCovector line 273
  27. def OAI.YauCounterexamples.planeAngularCovector line 278
  28. lemma OAI.YauCounterexamples.plane_radius_pos line 283
  29. lemma OAI.YauCounterexamples.plane_radial_angular_sq line 294
  30. lemma OAI.YauCounterexamples.radialSquaredBase_radial_first line 307
  31. lemma OAI.YauCounterexamples.radialSquaredBase_radial_second line 320