OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.Effective.residualCode line 12

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

  2. theorem OAI.VelocityDetection.Effective.valid_residualCode line 18
  3. theorem OAI.VelocityDetection.Effective.eval_residualCode line 24
  4. def OAI.VelocityDetection.Effective.ArrayRecipe.initialCode line 63

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

  5. def OAI.VelocityDetection.Effective.ArrayRecipe.source line 66

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

  6. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_initialCode line 70
  7. theorem OAI.VelocityDetection.Effective.ArrayRecipe.eval_source line 76
  8. theorem OAI.VelocityDetection.Effective.ArrayRecipe.valid_source line 84
  9. def OAI.VelocityDetection.Effective.forceFunction line 99

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

  10. inductive OAI.VelocityDetection.Effective.MachineRecipe.Domain line 113

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

  11. def OAI.VelocityDetection.Effective.MachineRecipe.field line 116

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

  12. def OAI.VelocityDetection.Effective.MachineRecipe.source line 121

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

  13. def OAI.VelocityDetection.Effective.MachineRecipe.force line 125

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

  14. def OAI.VelocityDetection.Effective.MachineRecipe.analyticField line 131
  15. def OAI.VelocityDetection.Effective.MachineRecipe.analyticForce line 136
  16. def OAI.VelocityDetection.Effective.MachineRecipe.Good line 141
  17. theorem OAI.VelocityDetection.Effective.MachineRecipe.good_open line 144
  18. theorem OAI.VelocityDetection.Effective.MachineRecipe.valid_field line 157
  19. theorem OAI.VelocityDetection.Effective.MachineRecipe.valid_source line 164
  20. theorem OAI.VelocityDetection.Effective.MachineRecipe.valid_force line 171
  21. theorem OAI.VelocityDetection.Effective.MachineRecipe.eval_field line 179
  22. theorem OAI.VelocityDetection.Effective.MachineRecipe.field_germ line 187
  23. theorem OAI.VelocityDetection.Effective.MachineRecipe.eval_source line 193
  24. theorem OAI.VelocityDetection.Effective.MachineRecipe.eval_force line 204
  25. theorem OAI.VelocityDetection.Effective.MachineRecipe.force_germ line 228
  26. def OAI.VelocityDetection.Effective.MachineRecipe.timeCutoff line 243

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

  27. def OAI.VelocityDetection.Effective.MachineRecipe.spaceCutoff line 247

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

  28. theorem OAI.VelocityDetection.Effective.MachineRecipe.cutoffs_good line 251
  29. def OAI.VelocityDetection.Effective.MachineRecipe.runTrial line 270

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

  30. theorem OAI.VelocityDetection.Effective.MachineRecipe.runTrial_correct line 275
  31. theorem OAI.VelocityDetection.Effective.MachineRecipe.runTrial_terminates line 284
  32. theorem OAI.VelocityDetection.Effective.flatRound_radius_tendsto_precision line 298
  33. theorem OAI.VelocityDetection.Effective.Ball.converges_flat_precision line 362
  34. theorem OAI.VelocityDetection.Effective.Expr.round_converges_precision line 385
  35. structure OAI.VelocityDetection.Effective.RationalBox line 420

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

  36. def OAI.VelocityDetection.Effective.RationalBox.carrier line 434

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

  37. theorem OAI.VelocityDetection.Effective.RationalBox.compact_carrier line 436
  38. def OAI.VelocityDetection.Effective.RationalBox.cell line 438

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

  39. theorem OAI.VelocityDetection.Effective.RationalBox.cell_nonneg line 442
  40. theorem OAI.VelocityDetection.Effective.RationalBox.center_mem line 445
  41. theorem OAI.VelocityDetection.Effective.RationalBox.covers line 457
  42. theorem OAI.VelocityDetection.Effective.RationalBox.radius_tendsto line 500