OAI/Combinatorics/Progressions/Estimates/PreparedDetectedCanonicalNativeSource.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.prepared_jointAffineSourceEnvelope_ge_accuracy line 12
  2. theorem OAI.Erdos3.prepared_affineProfileToleranceEnvelope_ge_accuracy line 32
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLengthLog_mono_density line 50
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLengthLog_prepared_density line 57
  5. theorem OAI.Erdos3.VectorPolynomial.prepared_affineProfileToleranceEnvelope_kernel_bound line 63
  6. theorem OAI.Erdos3.VectorPolynomial.preparedCommonSamplerBlock_positive_spectrum line 96
  7. theorem OAI.Erdos3.VectorPolynomial.preparedCommonSamplerBlock_uniform_spectrum line 117
  8. structure OAI.Erdos3.VectorPolynomial.AllocatedEarlyNativeSourceGeometry line 197
  9. def OAI.Erdos3.VectorPolynomial.AllocatedPreparedNativeInterface line 239
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedPreparedNativeInterface_of_geometry line 473
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedPreparedNativeInterface_of_nonempty_geometry line 532
  12. theorem OAI.Erdos3.VectorPolynomial.exists_detected_canonical_native_source line 558
  13. def OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetectorConstants line 699
  14. theorem OAI.Erdos3.VectorPolynomial.preparedModularDetector_period_prefactor line 734
  15. theorem OAI.Erdos3.VectorPolynomial.exists_prepared_detected_canonical_native_source line 783