OAI/Combinatorics/EditApproximation/Queries/QueryCallbackPolynomial.lean

GitHub source file

15 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 declaration text), 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), 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_storedSumWordBudget line 11
  3. def OAI.EditApproximation.gp_storedSumBitBudget line 14
  4. def OAI.EditApproximation.gp_bandMassTotalStorageBudget line 17

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryRawWidthPolynomial.lean:11 (same declaration text).

  5. def OAI.EditApproximation.gp_warmupAverageBitBudget line 20
  6. def OAI.EditApproximation.gp_queryPhysicalDataBudget line 24
  7. def OAI.EditApproximation.gp_queryFamilySourceReadBudget line 28
  8. def OAI.EditApproximation.gp_bitPowerBitBudget line 31

    Also declared: OAI/Combinatorics/EditApproximation/Queries/QueryGatherPolynomial.lean:175 (same declaration text).

  9. def OAI.EditApproximation.gp_powerDenominatorBitBudget line 34
  10. def OAI.EditApproximation.callbackPolynomial line 37
  11. def OAI.EditApproximation.queryCallbackShellDegree line 41
  12. theorem OAI.EditApproximation.queryCallbackShell_fixedPower line 43
  13. def OAI.EditApproximation.normalizationPolynomial line 58
  14. def OAI.EditApproximation.queryNormalizationBitDegree line 61
  15. theorem OAI.EditApproximation.queryNormalization_fixedPower line 63