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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The explicit expanding-array scales in the bounded velocity detector. The diffusion loss is summable even though the number of addresses grows.

  1. def OAI.ForcedComputation.ExpandingDetector.expansion line 13
  2. def OAI.ForcedComputation.ExpandingDetector.initialRadius line 15
  3. def OAI.ForcedComputation.ExpandingDetector.radius line 18
  4. def OAI.ForcedComputation.ExpandingDetector.duration line 20
  5. theorem OAI.ForcedComputation.ExpandingDetector.initialRadius_pos line 23
  6. theorem OAI.ForcedComputation.ExpandingDetector.expansion_ge_four line 29
  7. theorem OAI.ForcedComputation.ExpandingDetector.radius_pos line 33
  8. theorem OAI.ForcedComputation.ExpandingDetector.radius_grows line 39
  9. theorem OAI.ForcedComputation.ExpandingDetector.duration_ratio line 49
  10. theorem OAI.ForcedComputation.ExpandingDetector.duration_ratio_le line 64
  11. theorem OAI.ForcedComputation.ExpandingDetector.diffusion_loss_term_bound line 85
  12. theorem OAI.ForcedComputation.ExpandingDetector.diffusion_loss_summable line 102
  13. theorem OAI.ForcedComputation.ExpandingDetector.total_stage_loss_le line 116
  14. theorem OAI.ForcedComputation.ExpandingDetector.initial_loss_lt line 132
  15. theorem OAI.ForcedComputation.ExpandingDetector.total_diffusion_loss_lt line 145