OAI/Analysis/MatrixSigning/Potential/MovementBudget.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Schedule.movementBudget line 10
  2. def OAI.CurrentKS.Schedule.threshold line 16
  3. lemma OAI.CurrentKS.Schedule.movementBudget_one_le line 18
  4. lemma OAI.CurrentKS.Schedule.movementBudget_pos line 20
  5. lemma OAI.CurrentKS.Schedule.threshold_pos line 23
  6. lemma OAI.CurrentKS.Schedule.threshold_le_one line 28
  7. lemma OAI.CurrentKS.Schedule.threshold_relation line 35
  8. def OAI.CurrentKS.Schedule.stepSize line 41
  9. def OAI.CurrentKS.Schedule.stencilSize line 42
  10. def OAI.CurrentKS.Schedule.meshSize line 43
  11. lemma OAI.CurrentKS.Schedule.stepSize_spec line 45
  12. lemma OAI.CurrentKS.Schedule.stencilSize_spec line 55
  13. lemma OAI.CurrentKS.Schedule.meshSize_spec line 62
  14. lemma OAI.CurrentKS.Schedule.schedule_radius line 71
  15. def OAI.CurrentKS.Schedule.coarseBudgetQ line 79
  16. def OAI.CurrentKS.Schedule.valueCurve2Q line 83
  17. def OAI.CurrentKS.Schedule.valueCurve3Q line 89
  18. def OAI.CurrentKS.Schedule.curveBudget line 96
  19. lemma OAI.CurrentKS.Schedule.coarseBudgetQ_cast line 99
  20. lemma OAI.CurrentKS.Schedule.curveBudget_cast line 104
  21. lemma OAI.CurrentKS.Schedule.curveBudget_one_le line 110