OAI/Combinatorics/Progressions/Estimates/PreparedModularGeneralDetectorLateFloor.lean

GitHub source file

5 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/PreparedLateToleranceCertifiedSource.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/PreparedLateToleranceCertifiedSource.lean:21 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedModularGeneralProductivityEarlyGain.lean:635 (same declaration text).

3. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularGeneralCanonicalLateFloorSource line 26
4. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularGeneralCanonicalLateFloorPhysicalSource line 181
5. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularGeneralDetectorLateFloor line 353