OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.VelocityDetection.Effective.Expr.(instance at line 13) line 13
  2. instance OAI.VelocityDetection.Effective.Expr.(instance at line 15) line 15
  3. instance OAI.VelocityDetection.Effective.Expr.(instance at line 17) line 17
  4. instance OAI.VelocityDetection.Effective.Expr.(instance at line 19) line 19
  5. instance OAI.VelocityDetection.Effective.Expr.(instance at line 21) line 21
  6. instance OAI.VelocityDetection.Effective.Expr.(instance at line 23) line 23
  7. instance OAI.VelocityDetection.Effective.Expr.(instance at line 25) line 25
  8. theorem OAI.VelocityDetection.Effective.Expr.eval_add line 27
  9. theorem OAI.VelocityDetection.Effective.Expr.eval_neg line 29
  10. theorem OAI.VelocityDetection.Effective.Expr.eval_sub line 31
  11. theorem OAI.VelocityDetection.Effective.Expr.eval_mul line 33
  12. theorem OAI.VelocityDetection.Effective.Expr.eval_inv line 35
  13. theorem OAI.VelocityDetection.Effective.Expr.eval_div line 37
  14. theorem OAI.VelocityDetection.Effective.Expr.eval_rat line 39
  15. theorem OAI.VelocityDetection.Effective.Expr.eval_var line 41
  16. theorem OAI.VelocityDetection.Effective.Expr.eval_nat line 43
  17. theorem OAI.VelocityDetection.Effective.Expr.valid_add line 47
  18. theorem OAI.VelocityDetection.Effective.Expr.valid_neg line 49
  19. theorem OAI.VelocityDetection.Effective.Expr.valid_sub line 51
  20. theorem OAI.VelocityDetection.Effective.Expr.valid_mul line 53
  21. theorem OAI.VelocityDetection.Effective.Expr.valid_inv line 55
  22. theorem OAI.VelocityDetection.Effective.Expr.valid_div line 57
  23. theorem OAI.VelocityDetection.Effective.Expr.valid_rat line 59
  24. theorem OAI.VelocityDetection.Effective.Expr.valid_var line 61
  25. theorem OAI.VelocityDetection.Effective.Expr.valid_nat line 63
  26. theorem OAI.VelocityDetection.Effective.Expr.eval_lit0 line 65
  27. theorem OAI.VelocityDetection.Effective.Expr.valid_lit0 line 67
  28. theorem OAI.VelocityDetection.Effective.Expr.eval_lit1 line 69
  29. theorem OAI.VelocityDetection.Effective.Expr.valid_lit1 line 71
  30. theorem OAI.VelocityDetection.Effective.Expr.eval_lit2 line 73
  31. theorem OAI.VelocityDetection.Effective.Expr.valid_lit2 line 75
  32. theorem OAI.VelocityDetection.Effective.Expr.eval_lit3 line 77
  33. theorem OAI.VelocityDetection.Effective.Expr.valid_lit3 line 79
  34. theorem OAI.VelocityDetection.Effective.Expr.eval_lit8 line 81
  35. theorem OAI.VelocityDetection.Effective.Expr.valid_lit8 line 83
  36. theorem OAI.VelocityDetection.Effective.Expr.eval_lit16 line 85
  37. theorem OAI.VelocityDetection.Effective.Expr.valid_lit16 line 87
  38. theorem OAI.VelocityDetection.Effective.Expr.eval_lit1024 line 89
  39. theorem OAI.VelocityDetection.Effective.Expr.valid_lit1024 line 91
  40. theorem OAI.VelocityDetection.Effective.Expr.eval_lit3000 line 93
  41. theorem OAI.VelocityDetection.Effective.Expr.valid_lit3000 line 95
  42. def OAI.VelocityDetection.Effective.Expr.subst line 97

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

  43. theorem OAI.VelocityDetection.Effective.Expr.eval_subst line 106
  44. theorem OAI.VelocityDetection.Effective.Expr.valid_subst line 110
  45. def OAI.VelocityDetection.Effective.Expr.sumList line 123

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

  46. theorem OAI.VelocityDetection.Effective.Expr.eval_sumList line 127
  47. theorem OAI.VelocityDetection.Effective.Expr.valid_sumList line 133
  48. def OAI.VelocityDetection.Effective.Expr.sumFin line 139

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

  49. theorem OAI.VelocityDetection.Effective.Expr.eval_sumFin line 141
  50. theorem OAI.VelocityDetection.Effective.Expr.valid_sumFin line 145
  51. def OAI.VelocityDetection.Effective.Expr.unaryD line 152

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

  52. theorem OAI.VelocityDetection.Effective.Expr.eval_unaryD line 154
  53. theorem OAI.VelocityDetection.Effective.Expr.valid_unaryD line 167
  54. theorem OAI.VelocityDetection.Effective.Expr.eval_diff_curve line 171
  55. def OAI.VelocityDetection.Effective.Recipe.glue line 189

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

  56. theorem OAI.VelocityDetection.Effective.Recipe.eval_glue line 191
  57. theorem OAI.VelocityDetection.Effective.Recipe.valid_glue line 194
  58. def OAI.VelocityDetection.Effective.Recipe.step line 196

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

  59. theorem OAI.VelocityDetection.Effective.Recipe.eval_step line 198
  60. theorem OAI.VelocityDetection.Effective.Recipe.valid_step line 202
  61. def OAI.VelocityDetection.Effective.Recipe.pulse line 207

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

  62. theorem OAI.VelocityDetection.Effective.Recipe.eval_pulse line 209
  63. theorem OAI.VelocityDetection.Effective.Recipe.valid_pulse line 214
  64. def OAI.VelocityDetection.Effective.Recipe.window line 217

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

  65. def OAI.VelocityDetection.Effective.Recipe.windowD line 219

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

  66. theorem OAI.VelocityDetection.Effective.Recipe.eval_window line 221
  67. theorem OAI.VelocityDetection.Effective.Recipe.eval_windowD line 225
  68. theorem OAI.VelocityDetection.Effective.Recipe.valid_window line 229
  69. theorem OAI.VelocityDetection.Effective.Recipe.valid_windowD line 232
  70. def OAI.VelocityDetection.Effective.Recipe.theta line 236

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

  71. theorem OAI.VelocityDetection.Effective.Recipe.eval_theta line 239
  72. theorem OAI.VelocityDetection.Effective.Recipe.valid_theta line 243
  73. def OAI.VelocityDetection.Effective.Recipe.center line 249

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

  74. theorem OAI.VelocityDetection.Effective.Recipe.eval_center line 254
  75. theorem OAI.VelocityDetection.Effective.Recipe.valid_center line 259
  76. def OAI.VelocityDetection.Effective.Recipe.gate line 266

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

  77. theorem OAI.VelocityDetection.Effective.Recipe.eval_gate line 275
  78. theorem OAI.VelocityDetection.Effective.Recipe.valid_gate line 280
  79. def OAI.VelocityDetection.Effective.Recipe.impulse line 289

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

  80. theorem OAI.VelocityDetection.Effective.Recipe.eval_impulse line 293
  81. theorem OAI.VelocityDetection.Effective.Recipe.valid_impulse line 298
  82. def OAI.VelocityDetection.Effective.Recipe.packet line 304

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

  83. theorem OAI.VelocityDetection.Effective.Recipe.eval_packet line 308
  84. theorem OAI.VelocityDetection.Effective.Recipe.valid_packet line 312
  85. def OAI.VelocityDetection.Effective.Expr.activeSum line 325

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

  86. theorem OAI.VelocityDetection.Effective.Expr.eval_activeSum line 332
  87. theorem OAI.VelocityDetection.Effective.Expr.valid_activeSum line 350
  88. abbrev OAI.VelocityDetection.Effective.ArrayRecipe.Code line 373

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

  89. def OAI.VelocityDetection.Effective.ArrayRecipe.K line 375

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

  90. def OAI.VelocityDetection.Effective.ArrayRecipe.D line 377

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

  91. def OAI.VelocityDetection.Effective.ArrayRecipe.radius line 379

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

  92. def OAI.VelocityDetection.Effective.ArrayRecipe.spacing line 382

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

  93. def OAI.VelocityDetection.Effective.ArrayRecipe.duration line 384

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

  94. def OAI.VelocityDetection.Effective.ArrayRecipe.start line 387

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

  95. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_radius line 391
  96. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_spacing line 396
  97. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_duration line 400
  98. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_start line 404
  99. theorem OAI.VelocityDetection.Effective.ArrayRecipe.valid_radius line 410
  100. theorem OAI.VelocityDetection.Effective.ArrayRecipe.valid_spacing line 412
  101. theorem OAI.VelocityDetection.Effective.ArrayRecipe.valid_duration line 414
  102. theorem OAI.VelocityDetection.Effective.ArrayRecipe.valid_start line 416
  103. def OAI.VelocityDetection.Effective.ArrayRecipe.sign line 421

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

  104. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_sign line 424
  105. abbrev OAI.VelocityDetection.Effective.ArrayRecipe.Instruction line 429

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

  106. def OAI.VelocityDetection.Effective.ArrayRecipe.path line 431

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

  107. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_path line 436
  108. theorem OAI.VelocityDetection.Effective.ArrayRecipe.valid_path line 442
  109. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_velocity line 448
  110. def OAI.VelocityDetection.Effective.ArrayRecipe.gate line 458

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

  111. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_gate line 462
  112. theorem OAI.VelocityDetection.Effective.ArrayRecipe.valid_gate line 474
  113. def OAI.VelocityDetection.Effective.ArrayRecipe.stage line 485

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

  114. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_stage line 488
  115. theorem OAI.VelocityDetection.Effective.ArrayRecipe.valid_stage line 495
  116. def OAI.VelocityDetection.Effective.ArrayRecipe.field line 498

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

  117. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_field line 500
  118. theorem OAI.VelocityDetection.Effective.ArrayRecipe.valid_field line 509
  119. def OAI.VelocityDetection.Effective.ChartRecipe.scale line 523

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