OAI/Combinatorics/EditApproximation/Binary/BinarySampledGroupPolynomial.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

A fixed polynomial bounds the actual sampled-member bit counter. The scale is supplied through its bit length, so a large distance scale does not introduce a spurious linear dependence on that scale.

  1. abbrev OAI.EditApproximation.GP line 12

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Queries/QueryCallbackPolynomial.lean:9 (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.gbits line 13
  3. def OAI.EditApproximation.gSumWord line 14
  4. def OAI.EditApproximation.gSumWork line 16
  5. def OAI.EditApproximation.gSumStorage line 17
  6. def OAI.EditApproximation.gConnectionWord line 18
  7. def OAI.EditApproximation.gConnectionWork line 19
  8. def OAI.EditApproximation.gEnvelopeWord line 22
  9. def OAI.EditApproximation.gEnvelopeWork line 23
  10. def OAI.EditApproximation.gRoundWork line 28
  11. def OAI.EditApproximation.gSampleCountWork line 32
  12. def OAI.EditApproximation.gIndexWork line 35
  13. def OAI.EditApproximation.gScaleWord line 37
  14. def OAI.EditApproximation.gScaleWork line 38
  15. def OAI.EditApproximation.gMemberWord line 41
  16. def OAI.EditApproximation.gMemberWork line 42
  17. def OAI.EditApproximation.gCountedWork line 44
  18. def OAI.EditApproximation.gInput line 46
  19. def OAI.EditApproximation.sampledGroupPolynomial line 49
  20. def OAI.EditApproximation.sampledGroupBitDegree line 60
  21. def OAI.EditApproximation.sampledGroupEnvironment line 62
  22. theorem OAI.EditApproximation.sampledGroupPolynomial_eval line 70
  23. theorem OAI.EditApproximation.sampledMemberBitBudget_fixedPower line 75