OAI/Combinatorics/Progressions/Dynamics/PreparedFiniteNestedCanonicalEarlyPrimitiveBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.exists_commonRadiusPrimitive_bound line 10
  2. theorem OAI.Erdos3.VectorPolynomial.exists_preparedCommonRadiusPrimitive_budget line 21
  3. def OAI.Erdos3.VectorPolynomial.preparedCommonRadiusPrimitiveExponent line 39
  4. theorem OAI.Erdos3.VectorPolynomial.preparedCommonRadiusPrimitiveExponent_two_le line 42
  5. theorem OAI.Erdos3.VectorPolynomial.preparedCommonRadiusPrimitive_bound line 46
  6. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardPairedSourcePrecision_le_direct line 61
  7. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllSlotResource_budget line 77
  8. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceNative_budget line 107
  9. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedEarlyPrimitive_budget line 153
  10. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedCanonicalEarlyPrimitive_budget line 283