OAI/Combinatorics/Progressions/Lattices/AllocatedResidueSitePrimitiveAverage.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.selectedResidue_supported_fiber_error line 22
  2. theorem OAI.Erdos3.selectedResidue_supported_fiber_error_uniform line 38
  3. theorem OAI.Erdos3.selectedResidue_supported_fiber_test_error line 48
  4. theorem OAI.Erdos3.selectedResidue_weighted_condition_error line 88
  5. theorem OAI.Erdos3.selectedResidue_supported_fiber_weighted_error line 117
  6. theorem OAI.Erdos3.selectedResidue_supported_fiber_weighted_test_error line 131
  7. abbrev OAI.Erdos3.VectorPolynomial.AllocatedPositiveResidue line 181
  8. structure OAI.Erdos3.VectorPolynomial.AllocatedResidueSiteWitness line 190
  9. def OAI.Erdos3.VectorPolynomial.allocatedResidueWitnessProfile line 209
  10. def OAI.Erdos3.VectorPolynomial.allocatedSupportedResidueSiteProfile line 213
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedResidueSiteProfile_positive line 220
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueWitnessProfile_error line 228
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedResidueSiteProfile_error line 242
  14. def OAI.Erdos3.VectorPolynomial.AllocatedResidueSiteSampling line 288
  15. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_residue_site_sampling line 387
  16. theorem OAI.Erdos3.VectorPolynomial.allocated_residue_site_sampled_error line 464
  17. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_residue_site_sampled_error line 621
  18. theorem OAI.Erdos3.VectorPolynomial.allocated_residue_site_weighted_sampled_error line 766
  19. theorem OAI.Erdos3.VectorPolynomial.allocated_residue_site_primitive_error line 940
  20. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_residue_site_primitive_error line 1077