OAI/Combinatorics/Progressions/Estimates/PreparedModularGeneralProductivityEarlyGain.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_early_dimensions line 15
  2. theorem OAI.Erdos3.VectorPolynomial.preparedModularCanonicalDetector_early_cap line 40
  3. structure OAI.Erdos3.VectorPolynomial.AllocatedEarlyNativeSourceGeometryGeneral line 159
  4. def OAI.Erdos3.VectorPolynomial.AllocatedPreparedNativeInterfaceGeneral line 201
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedPreparedNativeInterfaceGeneral_of_geometry line 435
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedPreparedNativeInterfaceGeneral_of_nonempty_geometry line 496
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCoveredComparison_instances line 524
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedEarlyNativeSourceGeometryGeneral_of_fields line 545
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLengthLog_prepared_density_fin line 626

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

  10. theorem OAI.Erdos3.VectorPolynomial.preparedComparison_eta_bound line 635

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

  11. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularGeneralCanonicalSource line 640
  12. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularGeneralCanonicalEarlyParameters line 785
  13. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularGeneralCanonicalPhysicalSource line 828
  14. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralProductivity_early_gain line 997