OAI/Combinatorics/EditApproximation/Numerics/GradientStorageBits.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for the rational data stored by the gradient and linear-score routines, including the finite logarithm sums.

  1. def OAI.EditApproximation.logarithmEncodingBudget line 13
  2. theorem OAI.EditApproximation.rationalLogApproximation_encoding_le line 16
  3. def OAI.EditApproximation.smoothedPointEncodingBudget line 24
  4. theorem OAI.EditApproximation.smoothedPoint_encoding_le line 26
  5. def OAI.EditApproximation.gradientEncodingBudget line 37
  6. theorem OAI.EditApproximation.rationalSmoothedGradient_encoding_le line 41
  7. theorem OAI.EditApproximation.rational_finite_sum_encoding_le line 61
  8. theorem OAI.EditApproximation.vectorDotWithWork_encoding_le line 82