OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VelocityDetection.Effective.RationalBox.eventually_safe line 11
  2. def OAI.VelocityDetection.Effective.RationalBox.boundTrial line 31

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

  3. theorem OAI.VelocityDetection.Effective.RationalBox.boundTrial_correct line 37
  4. theorem OAI.VelocityDetection.Effective.RationalBox.boundTrial_terminates line 59
  5. def OAI.VelocityDetection.Effective.MachineRecipe.boxTimeCutoff line 74

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

  6. def OAI.VelocityDetection.Effective.MachineRecipe.boxSpaceCutoff line 78

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

  7. theorem OAI.VelocityDetection.Effective.MachineRecipe.box_good line 82
  8. def OAI.VelocityDetection.Effective.MachineRecipe.runBoundTrial line 105

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

  9. theorem OAI.VelocityDetection.Effective.MachineRecipe.runBoundTrial_correct line 109
  10. theorem OAI.VelocityDetection.Effective.MachineRecipe.runBoundTrial_terminates line 120
  11. structure OAI.VelocityDetection.Effective.MachineRecipe.Program line 132

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

  12. def OAI.VelocityDetection.Effective.MachineRecipe.compile line 137

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

  13. def OAI.VelocityDetection.Effective.MachineRecipe.Program.valueTrial line 148

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

  14. def OAI.VelocityDetection.Effective.MachineRecipe.Program.boundTrial line 152

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

  15. def OAI.VelocityDetection.Effective.MachineRecipe.Program.evaluate line 156

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

  16. def OAI.VelocityDetection.Effective.MachineRecipe.Program.derivativeBounds line 159

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

  17. def OAI.VelocityDetection.Effective.MachineRecipe.Program.Represents line 162

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

  18. theorem OAI.VelocityDetection.Effective.MachineRecipe.Program.compile_represents line 174
  19. def OAI.VelocityDetection.Effective.ComputableReal line 202

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