OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpandingArray.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.ExpandingArray.K₀ line 17
  2. def OAI.VelocityDetection.ExpandingArray.D line 19
  3. theorem OAI.VelocityDetection.ExpandingArray.K₀_nonneg line 21
  4. theorem OAI.VelocityDetection.ExpandingArray.D_ge_one line 23
  5. theorem OAI.VelocityDetection.ExpandingArray.count_eq line 28
  6. def OAI.VelocityDetection.ExpandingArray.sign line 46
  7. theorem OAI.VelocityDetection.ExpandingArray.abs_sign line 48
  8. def OAI.VelocityDetection.ExpandingArray.path line 67
  9. def OAI.VelocityDetection.ExpandingArray.stage line 73
  10. theorem OAI.VelocityDetection.ExpandingArray.contDiff_path line 78
  11. theorem OAI.VelocityDetection.ExpandingArray.contDiff_stage line 81
  12. theorem OAI.VelocityDetection.ExpandingArray.divergence_stage line 89
  13. theorem OAI.VelocityDetection.ExpandingArray.stage_zero_before line 102
  14. theorem OAI.VelocityDetection.ExpandingArray.stage_zero_after line 112
  15. theorem OAI.VelocityDetection.ExpandingArray.compactSupport_stage line 122
  16. def OAI.VelocityDetection.ExpandingArray.field line 134
  17. theorem OAI.VelocityDetection.ExpandingArray.field_eq_finite line 136
  18. theorem OAI.VelocityDetection.ExpandingArray.contDiff_field line 145
  19. theorem OAI.VelocityDetection.ExpandingArray.field_at_rest line 158
  20. theorem OAI.VelocityDetection.ExpandingArray.field_eq_stage line 169
  21. theorem OAI.VelocityDetection.ExpandingArray.divergence_field line 179
  22. theorem OAI.VelocityDetection.ExpandingArray.finiteCylinderSupport line 191
  23. theorem OAI.VelocityDetection.ExpandingArray.paths_separated line 208
  24. theorem OAI.VelocityDetection.ExpandingArray.stage_plateau line 222
  25. theorem OAI.VelocityDetection.ExpandingArray.field_plateau line 234
  26. theorem OAI.VelocityDetection.ExpandingArray.path_negative line 244
  27. theorem OAI.VelocityDetection.ExpandingArray.path_end line 253
  28. theorem OAI.VelocityDetection.ExpandingArray.path_coordinate_bounds line 261
  29. theorem OAI.VelocityDetection.ExpandingArray.path_derivative_bounds line 277