OAI/Combinatorics/Progressions/Estimates/PreparedCanonicalNativeSource.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.selectedResidueCellLaw line 13
  2. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_genuine_source_cell line 39
  3. theorem OAI.Erdos3.VectorPolynomial.exists_prepared_canonical_sources line 77
  4. def OAI.Erdos3.VectorPolynomial.allocatedProductCoarseNNMesh line 124
  5. theorem OAI.Erdos3.VectorPolynomial.cubeCount_rescale_bound_change_decidable line 130
  6. theorem OAI.Erdos3.VectorPolynomial.sum_compare_enumerations line 138
  7. theorem OAI.Erdos3.VectorPolynomial.allocated_coarse_cube_native_partner line 204
  8. theorem OAI.Erdos3.VectorPolynomial.allocated_coarse_mixture_native_partner line 253
  9. theorem OAI.Erdos3.VectorPolynomial.allocated_coarse_mixture_native_model line 381
  10. def OAI.Erdos3.VectorPolynomial.allocatedCoarseCubeSource line 515
  11. def OAI.Erdos3.VectorPolynomial.allocatedCoarseSiteTwists line 532
  12. theorem OAI.Erdos3.VectorPolynomial.allocated_coarse_native_family line 546
  13. structure OAI.Erdos3.VectorPolynomial.AllocatedCoarseSourceData line 612
  14. def OAI.Erdos3.VectorPolynomial.AllocatedCoarseSourceData.source line 648
  15. def OAI.Erdos3.VectorPolynomial.AllocatedCoarseSourceData.twists line 655
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedCoarseSourceData.twists_norm line 659
  17. theorem OAI.Erdos3.VectorPolynomial.AllocatedCoarseSourceData.detect line 665
  18. def OAI.Erdos3.VectorPolynomial.AllocatedCanonicalNativeData line 717
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalGenuineData_native line 883
  20. def OAI.Erdos3.VectorPolynomial.AllocatedUniversalCanonicalNativeSourceAt line 940
  21. theorem OAI.Erdos3.VectorPolynomial.AllocatedUniversalCanonicalSourceAt.to_native line 984
  22. def OAI.Erdos3.VectorPolynomial.allocatedCanonicalSmoothingLog line 1014
  23. def OAI.Erdos3.VectorPolynomial.allocatedCanonicalTailLog line 1020
  24. theorem OAI.Erdos3.VectorPolynomial.AllocatedFlexibleCanonicalSourceAt.at_log_bounds line 1027
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalSources_synchronize line 1045
  26. def OAI.Erdos3.VectorPolynomial.AllocatedInitializedCanonicalNativeSourceAt line 1096
  27. theorem OAI.Erdos3.VectorPolynomial.AllocatedInitializedCanonicalSourceAt.to_native line 1122
  28. theorem OAI.Erdos3.VectorPolynomial.exists_prepared_common_canonical_sources line 1147
  29. theorem OAI.Erdos3.VectorPolynomial.exists_prepared_canonical_native_sources line 1207