OAI/Analysis/BoxTransport/Flow.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Localized solenoidal moving fields and their unique global flows.

  1. def OAI.BoxTransport.Routing.derivativeEntry line 13
  2. theorem OAI.BoxTransport.Routing.derivativeEntry_apply line 18
  3. def OAI.BoxTransport.Routing.curlLinear line 21
  4. theorem OAI.BoxTransport.Routing.curlLinear_apply line 27
  5. def OAI.BoxTransport.Routing.spatialCurl line 35
  6. theorem OAI.BoxTransport.Routing.spatial_slice_fderiv line 37
  7. theorem OAI.BoxTransport.Routing.spatialDivergence_eq_full line 44
  8. theorem OAI.BoxTransport.Routing.contDiff_spatialCurl line 54
  9. theorem OAI.BoxTransport.Routing.hasCompactSupport_spatialCurl line 58
  10. theorem OAI.BoxTransport.Routing.fderiv_spatialCurl line 62
  11. theorem OAI.BoxTransport.Routing.spatialDivergence_spatialCurl line 70
  12. theorem OAI.BoxTransport.Routing.spatialCurl_congr_of_eventuallyEq line 86
  13. theorem OAI.BoxTransport.Routing.spatialCurl_zero_on_slice line 91
  14. theorem OAI.BoxTransport.Routing.curl_field_properties line 101
  15. def OAI.BoxTransport.Routing.potentialComponent line 114
  16. def OAI.BoxTransport.Routing.affinePotential line 118
  17. theorem OAI.BoxTransport.Routing.affinePotential_eq_cross line 124
  18. theorem OAI.BoxTransport.Routing.contDiff_affinePotential line 132
  19. theorem OAI.BoxTransport.Routing.fderiv_potentialComponent line 138
  20. theorem OAI.BoxTransport.Routing.fderiv_affinePotential line 154
  21. theorem OAI.BoxTransport.Routing.spatialCurl_affinePotential line 171
  22. theorem OAI.BoxTransport.Routing.spatialCurl_cutoff_plateau line 184
  23. theorem OAI.BoxTransport.Routing.spatialCurl_congr_on_slice line 194
  24. def OAI.BoxTransport.Routing.movingAffinePotential line 205
  25. theorem OAI.BoxTransport.Routing.contDiff_movingAffinePotential line 208
  26. theorem OAI.BoxTransport.Routing.spatialCurl_movingAffinePotential line 216
  27. def OAI.BoxTransport.Routing.movingBoxCutoff line 226
  28. theorem OAI.BoxTransport.Routing.contDiff_movingBoxCutoff line 231
  29. theorem OAI.BoxTransport.Routing.movingBoxCutoff_one line 239
  30. theorem OAI.BoxTransport.Routing.movingBoxCutoff_zero line 255
  31. def OAI.BoxTransport.Routing.movingPlateau line 276
  32. theorem OAI.BoxTransport.Routing.isOpen_movingPlateau line 279
  33. theorem OAI.BoxTransport.Routing.movingBoxCutoff_eventually_one line 287
  34. theorem OAI.BoxTransport.Routing.spatialCurl_localized_movingAffinePotential line 296
  35. def OAI.BoxTransport.Routing.localizedPotential line 309
  36. theorem OAI.BoxTransport.Routing.contDiff_localizedPotential line 312
  37. theorem OAI.BoxTransport.Routing.movingAffinePotential_zero line 318
  38. theorem OAI.BoxTransport.Routing.hasCompactSupport_localizedPotential line 324
  39. def OAI.BoxTransport.Routing.familyPotential line 349
  40. theorem OAI.BoxTransport.Routing.contDiff_familyPotential line 353
  41. theorem OAI.BoxTransport.Routing.hasCompactSupport_familyPotential line 359
  42. theorem OAI.BoxTransport.Routing.familyPotential_zero line 375
  43. theorem OAI.BoxTransport.Routing.familyPotential_eq_on_plateau line 383
  44. theorem OAI.BoxTransport.Routing.spatialCurl_familyPotential_on_plateau line 405
  45. theorem OAI.BoxTransport.Routing.localized_separated_motion line 422
  46. theorem OAI.BoxTransport.Routing.smooth_compact_bounds line 452
  47. theorem OAI.BoxTransport.Routing.globalFlow_of_bounded_lipschitz line 463
  48. theorem OAI.BoxTransport.Routing.smooth_compact_globalFlow line 538
  49. theorem OAI.BoxTransport.Routing.trace_zero_of_determinant_one line 545
  50. def OAI.BoxTransport.Routing.affineTrajectory line 563
  51. theorem OAI.BoxTransport.Routing.affineTrajectory_initial line 566
  52. theorem OAI.BoxTransport.Routing.hasDerivAt_affineTrajectory line 571
  53. theorem OAI.BoxTransport.Routing.affineTrajectory_in_plateau line 581
  54. theorem OAI.BoxTransport.Routing.realizes_supplied_separated_motion line 594
  55. theorem OAI.BoxTransport.Routing.contDiff_motion_deriv line 642
  56. def OAI.BoxTransport.Routing.diagonalLogVelocity line 646
  57. theorem OAI.BoxTransport.Routing.contDiff_diagonalLogVelocity line 649
  58. theorem OAI.BoxTransport.Routing.hasDerivAt_diagonalLogVelocity line 657
  59. theorem OAI.BoxTransport.Routing.deriv_zero_outside_interval line 663
  60. theorem OAI.BoxTransport.Routing.realizes_stationary_separated_motion line 679