OAI/MathematicalPhysics/SheetFlows/Profiles.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows profiles.

  1. def OAI.Solenoidal.plateau line 17
  2. theorem OAI.Solenoidal.plateau_contDiff line 21
  3. theorem OAI.Solenoidal.plateau_nonneg line 25
  4. theorem OAI.Solenoidal.plateau_le_one line 28
  5. theorem OAI.Solenoidal.plateau_even line 32
  6. theorem OAI.Solenoidal.plateau_one line 38
  7. theorem OAI.Solenoidal.plateau_zero line 46
  8. theorem OAI.Solenoidal.plateau_compactSupport line 54
  9. def OAI.Solenoidal.linearProfile line 63
  10. theorem OAI.Solenoidal.linearProfile_contDiff line 65
  11. theorem OAI.Solenoidal.linearProfile_odd line 69
  12. theorem OAI.Solenoidal.linearProfile_eq line 75
  13. theorem OAI.Solenoidal.linearProfile_zero line 78
  14. theorem OAI.Solenoidal.linearProfile_integral_zero line 81
  15. def OAI.Solenoidal.periodize line 89
  16. theorem OAI.Solenoidal.periodize_periodic line 92
  17. theorem OAI.Solenoidal.periodize_locally_finite line 107
  18. theorem OAI.Solenoidal.periodize_contDiff line 136
  19. theorem OAI.Solenoidal.periodize_on_chart line 147
  20. theorem OAI.Solenoidal.periodize_integral_eq line 166
  21. theorem OAI.Solenoidal.shifted_profile_zero_outside line 182
  22. def OAI.Solenoidal.Cprofile line 191
  23. def OAI.Solenoidal.Dprofile line 194
  24. theorem OAI.Solenoidal.Cprofile_periodic line 197
  25. theorem OAI.Solenoidal.Dprofile_periodic line 200
  26. theorem OAI.Solenoidal.Cprofile_contDiff line 203
  27. theorem OAI.Solenoidal.Dprofile_contDiff line 213
  28. theorem OAI.Solenoidal.Cprofile_on_chart line 223
  29. theorem OAI.Solenoidal.Dprofile_on_chart line 229
  30. theorem OAI.Solenoidal.Cprofile_one line 235
  31. theorem OAI.Solenoidal.Dprofile_linear line 241
  32. theorem OAI.Solenoidal.Cprofile_zero_on_chart line 247
  33. theorem OAI.Solenoidal.Dprofile_zero_on_chart line 253
  34. theorem OAI.Solenoidal.Cprofile_integral_eq line 259
  35. theorem OAI.Solenoidal.Dprofile_integral_zero line 266
  36. theorem OAI.Solenoidal.Cprofile_corrected_integral_zero line 274