OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartRouting.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.ChartRouting.scale line 13
  2. theorem OAI.VelocityDetection.ChartRouting.scale_pos line 15
  3. theorem OAI.VelocityDetection.ChartRouting.scale_small line 22
  4. theorem OAI.VelocityDetection.ChartRouting.scaled_address line 32
  5. def OAI.VelocityDetection.ChartRouting.origin line 45
  6. def OAI.VelocityDetection.ChartRouting.targetHeight line 47
  7. def OAI.VelocityDetection.ChartRouting.path line 50
  8. theorem OAI.VelocityDetection.ChartRouting.contDiff_path line 54
  9. theorem OAI.VelocityDetection.ChartRouting.path_source line 57
  10. theorem OAI.VelocityDetection.ChartRouting.path_target line 64
  11. theorem OAI.VelocityDetection.ChartRouting.velocity_source line 72
  12. theorem OAI.VelocityDetection.ChartRouting.velocity_target line 78
  13. theorem OAI.VelocityDetection.ChartRouting.theta_order line 84
  14. theorem OAI.VelocityDetection.ChartRouting.center_in_rectangle line 88
  15. theorem OAI.VelocityDetection.ChartRouting.path_bounds line 121
  16. theorem OAI.VelocityDetection.ChartRouting.nonterminal_bounds line 146
  17. def OAI.VelocityDetection.ChartRouting.radius line 167
  18. theorem OAI.VelocityDetection.ChartRouting.radius_pos line 169
  19. def OAI.VelocityDetection.ChartRouting.stage line 171
  20. theorem OAI.VelocityDetection.ChartRouting.contDiff_stage line 175
  21. theorem OAI.VelocityDetection.ChartRouting.stage_zero_before line 182
  22. theorem OAI.VelocityDetection.ChartRouting.stage_zero_after line 189
  23. theorem OAI.VelocityDetection.ChartRouting.stage_divergence line 196
  24. theorem OAI.VelocityDetection.ChartRouting.paths_separated line 208
  25. theorem OAI.VelocityDetection.ChartRouting.stage_plateau line 216
  26. def OAI.VelocityDetection.ChartRouting.chartSet line 233
  27. theorem OAI.VelocityDetection.ChartRouting.compact_chartSet line 235
  28. theorem OAI.VelocityDetection.ChartRouting.chartSet_interior line 237
  29. theorem OAI.VelocityDetection.ChartRouting.path_neighborhood line 252
  30. theorem OAI.VelocityDetection.ChartRouting.stage_support line 271
  31. def OAI.VelocityDetection.ChartRouting.finiteField line 281
  32. theorem OAI.VelocityDetection.ChartRouting.contDiff_prefix line 283
  33. theorem OAI.VelocityDetection.ChartRouting.prefix_divergence line 287
  34. theorem OAI.VelocityDetection.ChartRouting.prefix_support line 297
  35. theorem OAI.VelocityDetection.ChartRouting.prefix_zero_before line 303
  36. theorem OAI.VelocityDetection.ChartRouting.prefix_zero_after line 310
  37. theorem OAI.VelocityDetection.ChartRouting.prefix_eq_stage line 319
  38. theorem OAI.VelocityDetection.ChartRouting.compactSupport_prefix line 333
  39. def OAI.VelocityDetection.ChartRouting.periodicPrefix line 340
  40. theorem OAI.VelocityDetection.ChartRouting.contDiff_periodicPrefix line 342
  41. theorem OAI.VelocityDetection.ChartRouting.periodic_periodicPrefix line 350
  42. theorem OAI.VelocityDetection.ChartRouting.periodicPrefix_chart line 353
  43. theorem OAI.VelocityDetection.ChartRouting.periodicPrefix_plateau line 359