OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VelocityDetection.Effective.ChartRecipe.cast_scale line 15
  2. def OAI.VelocityDetection.Effective.ChartRecipe.radius line 19

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

  3. theorem OAI.VelocityDetection.Effective.ChartRecipe.cast_radius line 21
  4. def OAI.VelocityDetection.Effective.ChartRecipe.targetHeight line 25

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

  5. theorem OAI.VelocityDetection.Effective.ChartRecipe.cast_targetHeight line 28
  6. def OAI.VelocityDetection.Effective.ChartRecipe.path line 45

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

  7. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_path line 52
  8. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_path line 59
  9. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_velocity line 64
  10. def OAI.VelocityDetection.Effective.ChartRecipe.gate line 74

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

  11. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_gate line 79
  12. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_gate line 89
  13. def OAI.VelocityDetection.Effective.ChartRecipe.stage line 98

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

  14. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_stage line 101
  15. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_stage line 108
  16. def OAI.VelocityDetection.Effective.ChartRecipe.prefixCode line 111

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

  17. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_prefix line 113
  18. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_prefix line 120
  19. def OAI.VelocityDetection.Effective.ChartRecipe.duration line 123

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

  20. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_duration line 128
  21. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_duration line 134
  22. def OAI.VelocityDetection.Effective.ChartRecipe.localTime line 143

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

  23. def OAI.VelocityDetection.Effective.ChartRecipe.weight line 147

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

  24. def OAI.VelocityDetection.Effective.ChartRecipe.clock line 150

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

  25. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_localTime line 153
  26. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_weight line 157
  27. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_clock line 161
  28. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_localTime line 167
  29. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_weight line 174
  30. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_clock line 181
  31. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_weightD line 186
  32. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_clockD line 192
  33. def OAI.VelocityDetection.Effective.ChartRecipe.rawField line 198

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

  34. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_rawField line 203
  35. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_rawField line 211
  36. def OAI.VelocityDetection.Effective.ChartRecipe.initial line 219

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

  37. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_initial line 222
  38. def OAI.VelocityDetection.Effective.ChartRecipe.rawSource line 226

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

  39. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_rawSource line 232
  40. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_rawSource line 241
  41. def OAI.VelocityDetection.Effective.latticeIndex line 258
  42. theorem OAI.VelocityDetection.Effective.latticeIndex_mem line 261
  43. theorem OAI.VelocityDetection.Effective.latticeIndex_injective line 268
  44. theorem OAI.VelocityDetection.Effective.latticeIndex_surjective line 275
  45. theorem OAI.VelocityDetection.Effective.sum_lattice line 285
  46. def OAI.VelocityDetection.Effective.periodize line 299

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

  47. def OAI.VelocityDetection.Effective.shifted line 304
  48. theorem OAI.VelocityDetection.Effective.eval_periodize line 307
  49. theorem OAI.VelocityDetection.Effective.valid_periodize line 318
  50. def OAI.VelocityDetection.Effective.ChartRecipe.fieldBlock line 340

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

  51. def OAI.VelocityDetection.Effective.ChartRecipe.sourceBlock line 342

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

  52. theorem OAI.VelocityDetection.Effective.ChartRecipe.chartBound line 344
  53. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_fieldBlock line 348
  54. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_sourceBlock line 363
  55. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_fieldBlock line 379
  56. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_sourceBlock line 387
  57. def OAI.VelocityDetection.Effective.ChartRecipe.field line 393

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

  58. def OAI.VelocityDetection.Effective.ChartRecipe.source line 395

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

  59. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_field line 397
  60. theorem OAI.VelocityDetection.Effective.ChartRecipe.eval_source line 410
  61. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_field line 426
  62. theorem OAI.VelocityDetection.Effective.ChartRecipe.valid_source line 432
  63. def OAI.VelocityDetection.Effective.axis line 445
  64. def OAI.VelocityDetection.Effective.direction line 447
  65. def OAI.VelocityDetection.Effective.point line 450
  66. def OAI.VelocityDetection.Effective.pull line 452
  67. theorem OAI.VelocityDetection.Effective.axis_ne_zero line 454
  68. theorem OAI.VelocityDetection.Effective.update_axis_zero line 456
  69. theorem OAI.VelocityDetection.Effective.point_hasDerivAt line 459
  70. theorem OAI.VelocityDetection.Effective.coordinateD_pull line 479
  71. theorem OAI.VelocityDetection.Effective.coordinateDD_pull line 486