OAI/Combinatorics/Progressions/Dynamics/AllocatedNormalizedScaleBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedInitialLog line 9
  2. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedScaleInput line 14
  3. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedScaleLog line 18
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientAccuracyLog_nonneg line 23
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedJointLengthEnvelope_nonneg line 32
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedScaleBudget_bounds line 41
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedLengthLog_le_normalizedInitial line 59