OAI/Combinatorics/Progressions/Estimates/PreparedDetectedCanonicalNativeSourceGeometry.lean

GitHub source file

4 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/DetectedCanonicalEarlyRadiusLateFloorSource.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/DetectedCanonicalEarlyRadiusLateFloorSource.lean:32 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedDetectedCanonicalGeometry.lean:385 (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/DetectedCanonicalEarlyRadiusLateFloorSource.lean:40 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedDetectedCanonicalGeometry.lean:393 (same declaration text), OAI/Combinatorics/Progressions/Estimates/PreparedModularWitnessCanonicalGeometry.lean:41 (same declaration text).

  4. theorem OAI.Erdos3.VectorPolynomial.exists_prepared_detected_canonical_native_source_geometry line 64