OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

A finite polynomial certificate for the complete adaptive gather cost. The four kernel bounds and the two Cartesian counts are explicit inputs. Every remaining operation is addition, multiplication, fixed natural power, or bit length.

  1. abbrev OAI.EditApproximation.GP line 13

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Binary/BinarySampledGroupPolynomial.lean:12 (same statement text; different proof or body), OAI/Combinatorics/EditApproximation/Queries/QueryCallbackPolynomial.lean:9 (same statement text; different proof or body), OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:12 (same statement text; different proof or body), OAI/Combinatorics/EditApproximation/Queries/QueryRawWidthPolynomial.lean:9 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.GP@path.

  2. def OAI.EditApproximation.gp_localEligibilityBitBudget line 15

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:50 (same declaration text).

  3. def OAI.EditApproximation.gp_queryExponentsBitBudget line 19

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:54 (same declaration text).

  4. def OAI.EditApproximation.gp_queryScalesBitBudget line 22

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:57 (same declaration text).

  5. def OAI.EditApproximation.gp_gridPointsBitBudget line 25

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:18 (same declaration text).

  6. def OAI.EditApproximation.gp_gridStateBoxBitBudget line 28

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:21 (same declaration text).

  7. def OAI.EditApproximation.gp_queryGridPointsBitBudget line 32

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:25 (same declaration text).

  8. def OAI.EditApproximation.gp_queryRawCentersBitBudget line 35

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:60 (same declaration text).

  9. def OAI.EditApproximation.gp_cellCoordinateSetupBitBudget line 42
  10. def OAI.EditApproximation.gp_targetCellsBitBudget line 45
  11. def OAI.EditApproximation.gp_queryCellScanBitBudget line 48
  12. def OAI.EditApproximation.gp_queryGroupKeysBitBudget line 52
  13. def OAI.EditApproximation.gp_cellGridSetupBitBudget line 57
  14. def OAI.EditApproximation.gp_cellGridPointBitBudget line 60
  15. def OAI.EditApproximation.gp_cellGridPointsBitBudget line 63
  16. def OAI.EditApproximation.gp_cellStatesBitBudget line 66
  17. def OAI.EditApproximation.gp_queryCellStatesBitBudget line 70
  18. def OAI.EditApproximation.gp_queryOnlineKeysBitBudget line 74
  19. def OAI.EditApproximation.gp_queryInitialSupportBitBudget line 77
  20. def OAI.EditApproximation.gp_queryInitialSupportLength line 84
  21. def OAI.EditApproximation.gp_queryInitialGatherBitBudget line 89
  22. def OAI.EditApproximation.gp_localRepresentativeScaleBitBudget line 92

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:70 (same declaration text).

  23. def OAI.EditApproximation.gp_localRepresentativesBitBudget line 98

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:76 (same declaration text).

  24. def OAI.EditApproximation.gp_cellCentersBitBudget line 102
  25. def OAI.EditApproximation.gp_queryEarlierRepresentativesBitBudget line 107
  26. def OAI.EditApproximation.gp_wideChildGridBitBudget line 114

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:80 (same declaration text).

  27. def OAI.EditApproximation.gp_queryWideInputsBitBudget line 117

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:83 (same declaration text).

  28. def OAI.EditApproximation.gp_queryEarlierRepresentativesLength line 123
  29. def OAI.EditApproximation.gp_queryBandInputsBitBudget line 127
  30. def OAI.EditApproximation.gp_queryBandGatherBitBudget line 131
  31. def OAI.EditApproximation.gp_groupScalesBitBudget line 135
  32. def OAI.EditApproximation.gp_groupSampleCountBitBudget line 139
  33. def OAI.EditApproximation.gp_queryGroupSamplesBitBudget line 144
  34. def OAI.EditApproximation.gp_queryGroupSourceKeysBitBudget line 149
  35. def OAI.EditApproximation.gp_queryGroupSourceKeysLength line 158
  36. def OAI.EditApproximation.gp_queryGroupGatherBitBudget line 161
  37. def OAI.EditApproximation.gp_wideMaterializationBitBudget line 165
  38. def OAI.EditApproximation.gp_tableReadFactor line 169
  39. def OAI.EditApproximation.gp_bandCoordinatesBitBudget line 172
  40. def OAI.EditApproximation.gp_bitPowerBitBudget line 175

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryCallbackPolynomial.lean:31 (same declaration text).

  41. def OAI.EditApproximation.gp_onlineIndexBitBudget line 178
  42. def OAI.EditApproximation.gp_queryOnlineRangeBitBudget line 182
  43. def OAI.EditApproximation.gp_queryOnlineGatherBitBudget line 189
  44. def OAI.EditApproximation.gp_queryHistoryInputsLength line 193
  45. def OAI.EditApproximation.gp_queryGroupInputsLength line 196
  46. def OAI.EditApproximation.gp_querySharedCellInputsLength line 199
  47. def OAI.EditApproximation.gp_querySharedInputsLength line 202
  48. def OAI.EditApproximation.gp_queryRefinementReadBudget line 205
  49. def OAI.EditApproximation.gp_queryNeededInputsBitBudget line 208
  50. def OAI.EditApproximation.gp_queryRefinementStagesBudget line 212
  51. def OAI.EditApproximation.gp_queryRawHistoryInputsBitBudget line 218
  52. def OAI.EditApproximation.gp_queryEarlierInputsBitBudget line 224
  53. def OAI.EditApproximation.gp_groupSampleCountWordBudget line 230
  54. def OAI.EditApproximation.gp_queryGroupLabelsBitBudget line 233
  55. def OAI.EditApproximation.gp_queryGapStatesBitBudget line 237
  56. def OAI.EditApproximation.gp_queryRoundedStatesBitBudget line 242
  57. def OAI.EditApproximation.gp_queryGroupInputsBitBudget line 245
  58. def OAI.EditApproximation.gp_querySharedCellInputsBitBudget line 251
  59. def OAI.EditApproximation.gp_querySharedInputsBitBudget line 256
  60. def OAI.EditApproximation.gp_queryRefinementFinishBitBudget line 265
  61. def OAI.EditApproximation.gp_queryFinishReadBudget line 269
  62. def OAI.EditApproximation.gp_queryLocalRefinementBitBudget line 272
  63. def OAI.EditApproximation.gp_queryGroupBufferReadBudget line 283
  64. def OAI.EditApproximation.gp_queryBufferedGroupReadBudget line 287
  65. def OAI.EditApproximation.gp_queryOnlineBufferReadBudget line 290
  66. def OAI.EditApproximation.gp_queryLocalSourcesBitBudget line 293
  67. def OAI.EditApproximation.gp_queryBandReadBudget line 300
  68. def OAI.EditApproximation.gp_queryLocalBandBitBudget line 303
  69. def OAI.EditApproximation.gp_queryParentBufferReadBudget line 308
  70. def OAI.EditApproximation.gp_queryLocalProgramBitBudget line 311
  71. def OAI.EditApproximation.queryGatherPolynomial line 316
  72. def OAI.EditApproximation.queryGatherBitDegree line 321
  73. def OAI.EditApproximation.queryGatherEnvironment line 323
  74. theorem OAI.EditApproximation.queryGatherPolynomial_eval line 332
  75. theorem OAI.EditApproximation.queryLocalProgramBitBudget_fixedPower line 337