OAI/Combinatorics/Progressions/Estimates/PreparedLateToleranceCertifiedSource.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLengthLog_prepared_density_fin line 12

    Also declared: OAI/Combinatorics/Progressions/Estimates/DetectedCanonicalEarlyRadiusLateFloorSource.lean:253 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedModularGeneralDetectorLateFloor.lean:12 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedModularGeneralProductivityEarlyGain.lean:626 (same declaration text).

  2. theorem OAI.Erdos3.VectorPolynomial.preparedComparison_eta_bound line 21

    Also declared: OAI/Combinatorics/Progressions/Estimates/DetectedCanonicalEarlyRadiusLateFloorSource.lean:262 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedModularGeneralDetectorLateFloor.lean:21 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedModularGeneralProductivityEarlyGain.lean:635 (same declaration text).

  3. theorem OAI.Erdos3.VectorPolynomial.exists_detected_canonical_early_radius_late_tolerance_source line 26
  4. def OAI.Erdos3.VectorPolynomial.DetectedCanonicalLateToleranceFreeTrimPreparedStatement line 239
  5. theorem OAI.Erdos3.VectorPolynomial.exists_detected_canonical_late_tolerance_free_trim_prepared line 381
  6. def OAI.Erdos3.VectorPolynomial.PreparedLateToleranceFreeTrimSourceStatement line 586
  7. theorem OAI.Erdos3.VectorPolynomial.exists_prepared_late_tolerance_free_trim_source line 726
  8. theorem OAI.Erdos3.VectorPolynomial.centeredSource_physical_bounds line 787

    Also declared: OAI/Combinatorics/Progressions/Estimates/SharedWidthPreparedPerturbativeCertifiedSource.lean:561 (same declaration text).

  9. theorem OAI.Erdos3.VectorPolynomial.centeredSource_master_bounds line 798

    Also declared: OAI/Combinatorics/Progressions/Estimates/SharedWidthPreparedPerturbativeCertifiedSource.lean:572 (same declaration text).

  10. theorem OAI.Erdos3.VectorPolynomial.centeredSource_late_bounds line 805

    Also declared: OAI/Combinatorics/Progressions/Estimates/SharedWidthPreparedPerturbativeCertifiedSource.lean:579 (same declaration text).

  11. def OAI.Erdos3.VectorPolynomial.PreparedLateToleranceCenteredSourceStatement line 824
  12. theorem OAI.Erdos3.VectorPolynomial.exists_prepared_late_tolerance_centered_source line 964
  13. def OAI.Erdos3.VectorPolynomial.PreparedLateToleranceCertifiedSourceStatement line 1075
  14. theorem OAI.Erdos3.VectorPolynomial.exists_prepared_late_tolerance_certified_source line 1221