OAI/Combinatorics/Progressions/Estimates/SharedWidthPreparedPerturbativeCertifiedSource.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.SharedWidthPreparedCenteredModelMarginalDataInterface line 71
  2. theorem OAI.Erdos3.VectorPolynomial.sharedWidthPreparedCenteredModelMarginalData_of_direct line 197
  3. def OAI.Erdos3.VectorPolynomial.SharedWidthPreparedCenteredModelMarginalProjectionInterface line 264
  4. theorem OAI.Erdos3.VectorPolynomial.sharedWidthPreparedCenteredModelMarginalProjectionData_of_direct line 376
  5. def OAI.Erdos3.VectorPolynomial.SharedWidthPreparedCenteredModelMarginalRadiusInterface line 415
  6. theorem OAI.Erdos3.VectorPolynomial.sharedWidthPreparedCenteredModelMarginalRadiusInterface_of_projection line 528
  7. theorem OAI.Erdos3.VectorPolynomial.centeredSource_physical_bounds line 561

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedLateToleranceCertifiedSource.lean:787 (same declaration text).

  8. theorem OAI.Erdos3.VectorPolynomial.centeredSource_master_bounds line 572

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedLateToleranceCertifiedSource.lean:798 (same declaration text).

  9. theorem OAI.Erdos3.VectorPolynomial.centeredSource_late_bounds line 579

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedLateToleranceCertifiedSource.lean:805 (same declaration text).

  10. def OAI.Erdos3.VectorPolynomial.SharedWidthPreparedLateToleranceCenteredSourceStatement line 598
  11. theorem OAI.Erdos3.VectorPolynomial.exists_sharedWidth_prepared_late_tolerance_centered_source line 738
  12. def OAI.Erdos3.VectorPolynomial.SharedWidthPreparedLateToleranceCertifiedSourceStatement line 825
  13. theorem OAI.Erdos3.VectorPolynomial.exists_sharedWidth_prepared_late_tolerance_certified_source line 971
  14. def OAI.Erdos3.VectorPolynomial.SharedWidthPreparedPerturbativeCertifiedSourceStatement line 1035
  15. theorem OAI.Erdos3.VectorPolynomial.exists_sharedWidth_prepared_perturbative_certified_source line 1190