OAI/Combinatorics/EditApproximation/Queries/QueryRawWidthPolynomial.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EditApproximation.GP line 9

    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/QueryGatherPolynomial.lean:13 (same statement text; different proof or body), OAI/Combinatorics/EditApproximation/Queries/QueryInitialWarmupPolynomial.lean:12 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.GP@path.

  2. def OAI.EditApproximation.gp_bandMassTotalStorageBudget line 11

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

  3. def OAI.EditApproximation.gp_connectionWordBudget line 14
  4. def OAI.EditApproximation.gp_endpointDistanceWordBudget line 17
  5. def OAI.EditApproximation.gp_physicalContinuationInputBudget line 20
  6. def OAI.EditApproximation.gp_bellmanActionWordBudget line 23
  7. def OAI.EditApproximation.gp_localWarmupWordBudget line 26
  8. def OAI.EditApproximation.gp_refinementUpdateWordBudget line 30
  9. def OAI.EditApproximation.gp_localContinuationInputBudget line 33
  10. def OAI.EditApproximation.gp_localContinuationWordBudget line 36
  11. def OAI.EditApproximation.gp_preparedKernelWordBudget line 39
  12. def OAI.EditApproximation.rawWordPolynomial line 42
  13. def OAI.EditApproximation.queryRawWordDegree line 45
  14. theorem OAI.EditApproximation.queryRawWord_fixedPower line 47