OAI/Combinatorics/Progressions/Estimates/AllocatedDetectedCanonicalPeriod.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.canonicalSlicedModulus line 16
  2. theorem OAI.Erdos3.canonicalSlicedModulus_good line 22
  3. theorem OAI.Erdos3.canonicalSlicedModulus_pos line 29
  4. theorem OAI.Erdos3.canonicalSlicedModulus_le_exp line 37
  5. theorem OAI.Erdos3.canonicalSlicedModulus_candidate_dvd line 49
  6. theorem OAI.Erdos3.canonicalSlicedModulus_stride_period_dvd line 59
  7. theorem OAI.Erdos3.canonicalSlicedModulus_jet_period line 80
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_niltest_good_sliced_source line 142
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_canonical_sliced_source line 263
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_canonical_period_source line 402