OAI/Combinatorics/Progressions/Estimates/DetectedCanonicalEarlyRadiusLateFloorSource.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

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

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedDetectedCanonicalNativeSourceGeometry.lean:12 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedModularWitnessCanonicalGeometry.lean:13 (same declaration text).

  2. theorem OAI.Erdos3.VectorPolynomial.chart_budget_le_exp line 32

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedDetectedCanonicalGeometry.lean:385 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedDetectedCanonicalNativeSourceGeometry.lean:32 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedModularWitnessCanonicalGeometry.lean:33 (same declaration text).

  3. theorem OAI.Erdos3.VectorPolynomial.coefficient_count_add_one_le_support line 40

    Also declared: OAI/Combinatorics/Progressions/Estimates/PreparedDetectedCanonicalGeometry.lean:393 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedDetectedCanonicalNativeSourceGeometry.lean:40 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedModularWitnessCanonicalGeometry.lean:41 (same declaration text).

  4. theorem OAI.Erdos3.VectorPolynomial.exists_detected_canonical_native_source_early_radius line 64
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLengthLog_prepared_density_fin line 253

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

  6. theorem OAI.Erdos3.VectorPolynomial.preparedComparison_eta_bound line 262

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

  7. theorem OAI.Erdos3.VectorPolynomial.exists_detected_canonical_early_radius_late_floor_source line 267