OAI/Combinatorics/Progressions/Estimates/PreparedShortLateFloorCertifiedBadProduct.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.PreparedCertifiedSameScaleBadProductInterface line 22
  2. theorem OAI.Erdos3.VectorPolynomial.preparedCertifiedSameScaleBadProductInterface_of_bounds line 107
  3. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredJoint_badProduct_of_read line 172
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedWitnessScaleLog_lateFloor_le line 309
  5. theorem OAI.Erdos3.VectorPolynomial.preparedCertifiedSameScaleBadProductInterface_of_lateFloor line 334
  6. theorem OAI.Erdos3.VectorPolynomial.preparedCertifiedSameScaleBadProductInterface_of_late_parameters line 358
  7. theorem OAI.Erdos3.VectorPolynomial.lateTolerance_base_bounds line 403

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedShortLateToleranceCertifiedAttachment.lean:11 (same declaration text).

  8. theorem OAI.Erdos3.VectorPolynomial.lateTolerance_larger_bounds line 415

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedShortLateToleranceCertifiedAttachment.lean:23 (same declaration text).

  9. theorem OAI.Erdos3.VectorPolynomial.preparedCertifiedSameScaleBadProductInterface_of_lateTolerance line 448
  10. theorem OAI.Erdos3.VectorPolynomial.preparedCertifiedSameScaleBadProductInterface_of_lateTolerance_larger line 478
  11. theorem OAI.Erdos3.VectorPolynomial.preparedShortCertifiedSameScaleBadProductInterface_of_lateFloor line 533
  12. theorem OAI.Erdos3.VectorPolynomial.preparedShortCertifiedSameScaleBadProductInterface_of_late_parameters line 557