OAI/Computability/MinUncut/Search/RationalInner.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MinUncut.Inner.InnerData line 11
  2. def OAI.MinUncut.Inner.InnerData.epsilon line 25
  3. def OAI.MinUncut.Inner.InnerData.atomConstant line 26
  4. def OAI.MinUncut.Inner.InnerData.Check line 28
  5. instance OAI.MinUncut.Inner.InnerData.(instance at line 42) line 42
  6. lemma OAI.MinUncut.Inner.InnerData.epsilon_pos line 44
  7. lemma OAI.MinUncut.Inner.InnerData.epsilon_le line 52
  8. lemma OAI.MinUncut.Inner.InnerData.atomConstant_cast line 66
  9. def OAI.MinUncut.Inner.InnerData.realize line 70
  10. lemma OAI.MinUncut.Inner.InnerData.check_exists line 156
  11. def OAI.MinUncut.Inner.InnerData.search line 230
  12. lemma OAI.MinUncut.Inner.InnerData.search_check line 232
  13. lemma OAI.MinUncut.Outer.listTerm_mono line 242
  14. lemma OAI.MinUncut.Outer.remainderTerm_mono line 251
  15. structure OAI.MinUncut.Outer.OuterData line 260
  16. def OAI.MinUncut.Outer.OuterData.amplitude line 270
  17. def OAI.MinUncut.Outer.OuterData.hints line 271
  18. def OAI.MinUncut.Outer.OuterData.rate line 272
  19. def OAI.MinUncut.Outer.OuterData.listBound line 273
  20. def OAI.MinUncut.Outer.OuterData.radicand line 275
  21. def OAI.MinUncut.Outer.OuterData.Check line 278
  22. instance OAI.MinUncut.Outer.OuterData.(instance at line 285) line 285
  23. lemma OAI.MinUncut.Outer.OuterData.rate_cast line 288
  24. lemma OAI.MinUncut.Outer.OuterData.hints_eq line 289
  25. lemma OAI.MinUncut.Outer.OuterData.amplitude_nonneg line 291
  26. lemma OAI.MinUncut.Outer.OuterData.amplitude_ge line 298
  27. lemma OAI.MinUncut.Outer.OuterData.listBound_cast line 313
  28. def OAI.MinUncut.Outer.OuterData.realize line 322
  29. lemma OAI.MinUncut.Outer.OuterData.check_exists line 380
  30. def OAI.MinUncut.Outer.OuterData.search line 433
  31. lemma OAI.MinUncut.Outer.OuterData.search_check line 436
  32. def OAI.MinUncut.Outer.rationalBudgets line 448
  33. lemma OAI.MinUncut.Outer.rationalBudgets_cast line 454
  34. lemma OAI.MinUncut.Outer.rationalBudgets_pos line 460
  35. def OAI.MinUncut.Outer.rationalWeight line 466
  36. def OAI.MinUncut.Outer.tableAccuracy line 469
  37. lemma OAI.MinUncut.Outer.rationalWeight_nonneg line 472
  38. lemma OAI.MinUncut.Outer.rationalWeight_cast line 476
  39. lemma OAI.MinUncut.Outer.tableAccuracy_pos line 482
  40. lemma OAI.MinUncut.Outer.tableAccuracy_error line 488
  41. lemma OAI.MinUncut.Outer.ProofFamily.finiteCost_close line 498
  42. lemma OAI.MinUncut.Outer.finite_honest_cost line 511
  43. lemma OAI.MinUncut.Outer.finite_unsound_cost line 523