OAI/Combinatorics/Progressions/Estimates/PreparedModularWitnessCanonicalGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

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

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

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

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

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

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

  4. theorem OAI.Erdos3.VectorPolynomial.exists_detected_canonical_native_source_geometry line 65
  5. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularCanonicalDetectorEarlyParameters line 236
  6. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularGeneralCanonicalGeometry line 290
  7. theorem OAI.Erdos3.VectorPolynomial.exists_preparedModularWitnessCanonicalGeometry line 445