OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.Effective.Poly line 12

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

  2. def OAI.VelocityDetection.Effective.poly line 14

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

  3. def OAI.VelocityDetection.Effective.nextPoly line 18

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

  4. def OAI.VelocityDetection.Effective.flat line 22

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

  5. theorem OAI.VelocityDetection.Effective.poly_next line 25
  6. theorem OAI.VelocityDetection.Effective.hasDerivAt_flat line 36
  7. theorem OAI.VelocityDetection.Effective.contDiff_flat line 43
  8. def OAI.VelocityDetection.Effective.polyBound line 46

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

  9. theorem OAI.VelocityDetection.Effective.polyBound_nonneg line 50
  10. theorem OAI.VelocityDetection.Effective.monomial_exp_bound line 57
  11. theorem OAI.VelocityDetection.Effective.flat_bound line 66
  12. theorem OAI.VelocityDetection.Effective.flat_lipschitz line 89
  13. theorem OAI.VelocityDetection.Effective.flat_zero line 98
  14. inductive OAI.VelocityDetection.Effective.Expr line 100

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

  15. def OAI.VelocityDetection.Effective.Expr.eval line 119

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

  16. def OAI.VelocityDetection.Effective.Expr.Valid line 128
  17. def OAI.VelocityDetection.Effective.Expr.diff line 137

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

  18. theorem OAI.VelocityDetection.Effective.Expr.valid_diff line 146
  19. theorem OAI.VelocityDetection.Effective.Expr.continuousAt_eval line 156
  20. theorem OAI.VelocityDetection.Effective.Expr.valid_eventually line 167
  21. theorem OAI.VelocityDetection.Effective.Expr.hasDerivAt_eval line 175
  22. def OAI.VelocityDetection.Effective.Expr.jet line 202

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

  23. theorem OAI.VelocityDetection.Effective.Expr.valid_jet line 206
  24. structure OAI.VelocityDetection.Effective.Ball line 220

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

  25. def OAI.VelocityDetection.Effective.Ball.Certifies line 225
  26. def OAI.VelocityDetection.Effective.polyEval line 228

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

  27. theorem OAI.VelocityDetection.Effective.cast_polyEval line 232
  28. def OAI.VelocityDetection.Effective.expSum line 240

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

  29. def OAI.VelocityDetection.Effective.expError line 242

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

  30. theorem OAI.VelocityDetection.Effective.expError_nonneg line 244
  31. theorem OAI.VelocityDetection.Effective.exp_error line 246
  32. def OAI.VelocityDetection.Effective.flatRound line 263

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

  33. theorem OAI.VelocityDetection.Effective.flatRound_certifies line 270
  34. theorem OAI.VelocityDetection.Effective.flatRound_radius_nonneg line 289
  35. theorem OAI.VelocityDetection.Effective.flatRound_small_bound line 292
  36. theorem OAI.VelocityDetection.Effective.flatRound_exp_bound line 300
  37. theorem OAI.VelocityDetection.Effective.flatRound_nonpos line 309
  38. theorem OAI.VelocityDetection.Effective.flatRound_radius_tendsto line 312
  39. def OAI.VelocityDetection.Effective.Ball.atom line 375

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

  40. def OAI.VelocityDetection.Effective.Ball.add line 377

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

  41. def OAI.VelocityDetection.Effective.Ball.neg line 379

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

  42. def OAI.VelocityDetection.Effective.Ball.mul line 381

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

  43. def OAI.VelocityDetection.Effective.Ball.inv line 384

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

  44. def OAI.VelocityDetection.Effective.Ball.invSafe line 387

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

  45. def OAI.VelocityDetection.Effective.Ball.flat line 389

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

  46. theorem OAI.VelocityDetection.Effective.Ball.certifies_atom line 393
  47. theorem OAI.VelocityDetection.Effective.Ball.certifies_add line 396
  48. theorem OAI.VelocityDetection.Effective.Ball.certifies_neg line 404
  49. theorem OAI.VelocityDetection.Effective.Ball.certifies_mul line 409
  50. theorem OAI.VelocityDetection.Effective.Ball.certifies_inv line 425
  51. theorem OAI.VelocityDetection.Effective.Ball.certifies_flat line 441
  52. def OAI.VelocityDetection.Effective.Ball.Converges line 452
  53. theorem OAI.VelocityDetection.Effective.Ball.converges_atom line 456