OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/VelocityDetectorScales.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The rational widths and burst durations in the compact velocity detector. Index n below denotes manuscript block n + 1.

  1. def OAI.ForcedComputation.VelocityDetector.expansion line 12
  2. def OAI.ForcedComputation.VelocityDetector.geometricRatio line 14
  3. def OAI.ForcedComputation.VelocityDetector.width line 16
  4. def OAI.ForcedComputation.VelocityDetector.laplacianBound line 18
  5. def OAI.ForcedComputation.VelocityDetector.duration line 21
  6. def OAI.ForcedComputation.VelocityDetector.massBound line 23
  7. theorem OAI.ForcedComputation.VelocityDetector.expansion_pos line 26
  8. theorem OAI.ForcedComputation.VelocityDetector.expansion_one_le line 28
  9. theorem OAI.ForcedComputation.VelocityDetector.geometricRatio_pos line 30
  10. theorem OAI.ForcedComputation.VelocityDetector.geometricRatio_le_half line 35
  11. theorem OAI.ForcedComputation.VelocityDetector.width_pos line 41
  12. theorem OAI.ForcedComputation.VelocityDetector.width_le line 44
  13. theorem OAI.ForcedComputation.VelocityDetector.laplacianBound_nonneg line 49
  14. theorem OAI.ForcedComputation.VelocityDetector.duration_pos line 53
  15. theorem OAI.ForcedComputation.VelocityDetector.duration_le line 58
  16. theorem OAI.ForcedComputation.VelocityDetector.diffusion_loss_small line 64
  17. theorem OAI.ForcedComputation.VelocityDetector.heat_wait_long line 74
  18. theorem OAI.ForcedComputation.VelocityDetector.massBound_small line 78
  19. theorem OAI.ForcedComputation.VelocityDetector.total_injected_mass line 93