OAI/Analysis/MatrixSigning/Complexity/GlobalCounts.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Schedule.X line 15
  2. def OAI.CurrentKS.Schedule.coarseP line 17
  3. def OAI.CurrentKS.Schedule.jacobianP line 20
  4. def OAI.CurrentKS.Schedule.derivativeP line 21
  5. def OAI.CurrentKS.Schedule.secondP line 22
  6. def OAI.CurrentKS.Schedule.thirdP line 23
  7. def OAI.CurrentKS.Schedule.curvatureP line 25
  8. def OAI.CurrentKS.Schedule.movementP line 27
  9. def OAI.CurrentKS.Schedule.thresholdInvP line 29
  10. def OAI.CurrentKS.Schedule.stepInvP line 30
  11. def OAI.CurrentKS.Schedule.dropInvP line 31
  12. def OAI.CurrentKS.Schedule.iterationP line 32
  13. lemma OAI.CurrentKS.Schedule.coarseBudget_polynomial line 34
  14. lemma OAI.CurrentKS.Schedule.jacobian_polynomial line 46
  15. lemma OAI.CurrentKS.Schedule.derivative_polynomial line 55
  16. lemma OAI.CurrentKS.Schedule.secondP_eval line 65
  17. lemma OAI.CurrentKS.Schedule.thirdP_eval line 72
  18. lemma OAI.CurrentKS.Schedule.outer_polynomial line 85
  19. lemma OAI.CurrentKS.Schedule.curve2_mono line 92
  20. lemma OAI.CurrentKS.Schedule.curve3_mono line 100
  21. lemma OAI.CurrentKS.Schedule.valueCurve2_polynomial line 109
  22. lemma OAI.CurrentKS.Schedule.valueCurve3_polynomial line 122
  23. lemma OAI.CurrentKS.Schedule.curvatureP_eval line 135
  24. lemma OAI.CurrentKS.Schedule.curveBudget_polynomial line 140
  25. lemma OAI.CurrentKS.Schedule.movementBudget_polynomial line 158
  26. lemma OAI.CurrentKS.Schedule.thresholdInvP_eval line 190
  27. lemma OAI.CurrentKS.Schedule.threshold_inv_polynomial line 195
  28. lemma OAI.CurrentKS.Schedule.inv_min_le_sum line 207
  29. lemma OAI.CurrentKS.Schedule.stepSize_inv_bound line 215
  30. lemma OAI.CurrentKS.Schedule.stepInvP_eval line 226
  31. lemma OAI.CurrentKS.Schedule.dropInvP_eval line 231
  32. lemma OAI.CurrentKS.Schedule.dropInvP_one line 236
  33. lemma OAI.CurrentKS.Schedule.step_inv_polynomial line 240
  34. lemma OAI.CurrentKS.Schedule.drop_inv_polynomial line 257
  35. lemma OAI.CurrentKS.Descent.minList_inv_le line 275
  36. theorem OAI.CurrentKS.Schedule.normalized_parameter_bounds line 295
  37. lemma OAI.CurrentKS.RationalFace.uniformDrop_inv_polynomial line 358
  38. lemma OAI.CurrentKS.RationalFace.fuel_polynomial line 370
  39. theorem OAI.CurrentKS.RationalFace.normalized_fuel_polynomial line 378
  40. lemma OAI.CurrentKS.RationalSDP.searchFuel_le line 418
  41. lemma OAI.CurrentKS.RationalSDP.optimizeFuel_le line 431
  42. def OAI.CurrentKS.RationalSDP.queryDimensionBound line 440
  43. def OAI.CurrentKS.RationalSDP.queryOuterBound line 441
  44. def OAI.CurrentKS.RationalSDP.queryLipschitzBound line 442
  45. def OAI.CurrentKS.RationalSDP.queryInnerInvBound line 443
  46. def OAI.CurrentKS.RationalSDP.queryNearInvBound line 444
  47. def OAI.CurrentKS.RationalSDP.querySearchBound line 446
  48. def OAI.CurrentKS.RationalSDP.queryScanBound line 449
  49. lemma OAI.CurrentKS.RationalSDP.valueDimension_le line 451
  50. lemma OAI.CurrentKS.RationalSDP.valueOuterRadius_le_bound line 456
  51. lemma OAI.CurrentKS.RationalSDP.valueLipschitz_le_bound line 465
  52. lemma OAI.CurrentKS.RationalSDP.valueInnerRadius_inv_le_bound line 476
  53. lemma OAI.CurrentKS.RationalSDP.valueNearRadius_inv_le_bound line 483
  54. theorem OAI.CurrentKS.RationalSDP.valueSearchFuel_le line 503
  55. theorem OAI.CurrentKS.RationalSDP.valueScanIterations_le line 517
  56. def OAI.CurrentKS.Schedule.stencilInvP line 532
  57. def OAI.CurrentKS.Schedule.queryPrecisionP line 536
  58. lemma OAI.CurrentKS.Schedule.stencilSize_inv_bound line 541
  59. lemma OAI.CurrentKS.Schedule.stencilInvP_eval line 554
  60. lemma OAI.CurrentKS.Schedule.stencil_inv_polynomial line 560
  61. lemma OAI.CurrentKS.Schedule.queryPrecisionP_eval line 575
  62. lemma OAI.CurrentKS.Schedule.queryPrecisionP_ge line 583
  63. lemma OAI.CurrentKS.Schedule.query_errors_inv_polynomial line 594
  64. def OAI.CurrentKS.RationalSDP.valueScanP line 649
  65. lemma OAI.CurrentKS.RationalSDP.valueScanP_eval line 657
  66. theorem OAI.CurrentKS.RationalSDP.normalized_query_precisions line 660
  67. theorem OAI.CurrentKS.RationalSDP.normalized_query_search_iterations line 701