OAI/Analysis/MatrixSigning/Complexity/StoredBits.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.ScheduleBits.Args line 14
  2. def OAI.CurrentKS.ScheduleBits.eps line 15
  3. def OAI.CurrentKS.ScheduleBits.strip line 16
  4. def OAI.CurrentKS.ScheduleBits.movement line 17
  5. def OAI.CurrentKS.ScheduleBits.coarse line 22
  6. def OAI.CurrentKS.ScheduleBits.jacobian line 25
  7. def OAI.CurrentKS.ScheduleBits.derivative line 26
  8. def OAI.CurrentKS.ScheduleBits.second line 27
  9. def OAI.CurrentKS.ScheduleBits.third line 29
  10. def OAI.CurrentKS.ScheduleBits.curvature line 33
  11. def OAI.CurrentKS.ScheduleBits.threshold line 35
  12. def OAI.CurrentKS.ScheduleBits.step line 36
  13. def OAI.CurrentKS.ScheduleBits.mesh line 37
  14. lemma OAI.CurrentKS.ScheduleBits.eps_bits line 55
  15. lemma OAI.CurrentKS.ScheduleBits.strip_bits line 56
  16. lemma OAI.CurrentKS.ScheduleBits.movement_bits line 57
  17. lemma OAI.CurrentKS.ScheduleBits.coarse_bits line 62
  18. lemma OAI.CurrentKS.ScheduleBits.jacobian_bits line 67
  19. lemma OAI.CurrentKS.ScheduleBits.derivative_bits line 71
  20. lemma OAI.CurrentKS.ScheduleBits.second_bits line 75
  21. lemma OAI.CurrentKS.ScheduleBits.third_bits line 81
  22. lemma OAI.CurrentKS.ScheduleBits.curvature_bits line 87
  23. lemma OAI.CurrentKS.ScheduleBits.threshold_bits line 93
  24. lemma OAI.CurrentKS.ScheduleBits.step_bits line 97
  25. lemma OAI.CurrentKS.ScheduleBits.mesh_bits line 103
  26. def OAI.CurrentKS.ScheduleBits.args line 110
  27. lemma OAI.CurrentKS.ScheduleBits.step_eq line 111
  28. lemma OAI.CurrentKS.ScheduleBits.mesh_eq line 113
  29. theorem OAI.CurrentKS.ScheduleBits.schedule_parts_linear line 116
  30. lemma OAI.CurrentKS.RationalBits.Parts.natCast line 136
  31. lemma OAI.CurrentKS.RationalBits.natCast_parts line 141
  32. lemma OAI.CurrentKS.RationalGridSize.Grid.mono line 147
  33. lemma OAI.CurrentKS.RationalGridSize.Grid.half line 149
  34. lemma OAI.CurrentKS.RationalRoot.squareInterval_grid line 160
  35. lemma OAI.CurrentKS.RationalRoot.squareInterval_cube line 173
  36. lemma OAI.CurrentKS.RationalRoot.upperSqrt_parts line 186
  37. lemma OAI.CurrentKS.RationalGrid.upper_parts line 199
  38. def OAI.CurrentKS.RationalFace.baseBits line 212
  39. lemma OAI.CurrentKS.RationalFace.variance_parts line 214
  40. lemma OAI.CurrentKS.RationalFace.penalty_parts line 218
  41. lemma OAI.CurrentKS.RationalFace.base_parts line 226
  42. lemma OAI.CurrentKS.RationalRoot.roundMesh_grid line 245
  43. lemma OAI.CurrentKS.RationalRoot.computedCurvature_grid line 249
  44. lemma OAI.CurrentKS.Difference.gradientStep_grid line 267
  45. lemma OAI.CurrentKS.Difference.interiorCandidates_grid line 274
  46. lemma OAI.CurrentKS.Difference.endpointCandidates_grid line 291
  47. lemma OAI.CurrentKS.Difference.allCandidates_grid line 303
  48. def OAI.CurrentKS.RationalFace.meshDenominator line 322
  49. lemma OAI.CurrentKS.RationalFace.meshDenominator_pos line 325
  50. lemma OAI.CurrentKS.RationalFace.schedule_grid line 330
  51. lemma OAI.CurrentKS.RationalFace.extend_grid line 338
  52. lemma OAI.CurrentKS.RationalFace.freezeOne_grid line 346
  53. lemma OAI.CurrentKS.RationalFace.freezeList_grid line 360
  54. lemma OAI.CurrentKS.RationalFace.faceChoice_grid line 366
  55. lemma OAI.CurrentKS.RationalFace.transition_grid line 378
  56. theorem OAI.CurrentKS.RationalFace.rationalRun_grid line 390
  57. def OAI.CurrentKS.RationalFace.baseBitsP line 404
  58. def OAI.CurrentKS.RationalFace.meshBitsP line 407
  59. def OAI.CurrentKS.RationalFace.storedBitsP line 410
  60. lemma OAI.CurrentKS.RationalFace.baseBits_le line 412
  61. lemma OAI.CurrentKS.RationalFace.mesh_bits_bound line 425
  62. theorem OAI.CurrentKS.RationalFace.normalized_mesh_polynomial line 445
  63. lemma OAI.CurrentKS.RationalFace.run_grid line 463
  64. lemma OAI.CurrentKS.RationalFace.run_cube line 475
  65. theorem OAI.CurrentKS.RationalFace.normalized_stored_bits_polynomial line 488