OAI/MathematicalPhysics/NavierStokes/VelocityDetection/BurstBlock.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.BurstBlock.initial line 16
  2. def OAI.VelocityDetection.BurstBlock.rawField line 18
  3. def OAI.VelocityDetection.BurstBlock.field line 21
  4. def OAI.VelocityDetection.BurstBlock.rawSource line 24
  5. def OAI.VelocityDetection.BurstBlock.source line 27
  6. theorem OAI.VelocityDetection.BurstBlock.contDiff_time_smul line 29
  7. theorem OAI.VelocityDetection.BurstBlock.contDiff_rawField line 38
  8. theorem OAI.VelocityDetection.BurstBlock.contDiff_field line 41
  9. theorem OAI.VelocityDetection.BurstBlock.contDiff_rawSource line 44
  10. theorem OAI.VelocityDetection.BurstBlock.field_periodic line 48
  11. theorem OAI.VelocityDetection.BurstBlock.divergence_field line 55
  12. theorem OAI.VelocityDetection.BurstBlock.rawField_support line 59
  13. theorem OAI.VelocityDetection.BurstBlock.rawSource_support line 65
  14. theorem OAI.VelocityDetection.BurstBlock.bounded_rawSource line 78
  15. theorem OAI.VelocityDetection.BurstBlock.contDiff_source line 89
  16. theorem OAI.VelocityDetection.BurstBlock.field_zero line 93
  17. theorem OAI.VelocityDetection.BurstBlock.source_zero line 104
  18. def OAI.VelocityDetection.BurstBlock.center line 127
  19. def OAI.VelocityDetection.BurstBlock.rawPacket line 129
  20. def OAI.VelocityDetection.BurstBlock.rawReference line 132
  21. def OAI.VelocityDetection.BurstBlock.reference line 134
  22. theorem OAI.VelocityDetection.BurstBlock.contDiff_center line 136
  23. theorem OAI.VelocityDetection.BurstBlock.contDiff_rawPacket line 139
  24. theorem OAI.VelocityDetection.BurstBlock.contDiff_rawReference line 142
  25. theorem OAI.VelocityDetection.BurstBlock.deriv_center line 145
  26. theorem OAI.VelocityDetection.BurstBlock.plateau line 150
  27. theorem OAI.VelocityDetection.BurstBlock.packet_transport line 158
  28. theorem OAI.VelocityDetection.BurstBlock.source_match line 163
  29. theorem OAI.VelocityDetection.BurstBlock.rawReference_transport line 172
  30. theorem OAI.VelocityDetection.BurstBlock.rawReference_support line 186
  31. theorem OAI.VelocityDetection.BurstBlock.rawReference_interior line 190
  32. theorem OAI.VelocityDetection.BurstBlock.rawReference_boundedSupport line 194
  33. theorem OAI.VelocityDetection.BurstBlock.contDiff_reference line 201
  34. theorem OAI.VelocityDetection.BurstBlock.reference_periodic line 205
  35. theorem OAI.VelocityDetection.BurstBlock.reference_transport line 208