OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Expanding.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.Expanding.lambda line 10

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:94 (same declaration text).

  2. def OAI.VelocityDetection.Expanding.initialRadius line 12

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:96 (same declaration text).

  3. def OAI.VelocityDetection.Expanding.radius line 15

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:99 (same declaration text).

  4. def OAI.VelocityDetection.Expanding.count line 17
  5. def OAI.VelocityDetection.Expanding.spacing line 19
  6. def OAI.VelocityDetection.Expanding.duration line 21
  7. def OAI.VelocityDetection.Expanding.startTime line 24
  8. theorem OAI.VelocityDetection.Expanding.lambda_pos line 28
  9. theorem OAI.VelocityDetection.Expanding.lambda_ge_four line 32
  10. theorem OAI.VelocityDetection.Expanding.initialRadius_lower line 36
  11. theorem OAI.VelocityDetection.Expanding.initialRadius_pos line 45
  12. theorem OAI.VelocityDetection.Expanding.duration_div_radius_sq line 49
  13. theorem OAI.VelocityDetection.Expanding.coefficient_eq line 61
  14. theorem OAI.VelocityDetection.Expanding.loss_term_bound line 73
  15. theorem OAI.VelocityDetection.Expanding.summable_loss line 101
  16. theorem OAI.VelocityDetection.Expanding.stages_loss_lt line 108
  17. theorem OAI.VelocityDetection.Expanding.loading_loss_lt line 130
  18. theorem OAI.VelocityDetection.Expanding.total_loss_lt line 142
  19. theorem OAI.VelocityDetection.Expanding.radius_ge_one line 153
  20. theorem OAI.VelocityDetection.Expanding.radius_next_ge line 161
  21. theorem OAI.VelocityDetection.Expanding.duration_ge_one line 169
  22. theorem OAI.VelocityDetection.Expanding.startTime_ge line 176
  23. theorem OAI.VelocityDetection.Expanding.active_level_lt line 184
  24. theorem OAI.VelocityDetection.Expanding.finitely_many_active_levels line 189