OAI/Combinatorics/Progressions/Estimates/PreparedDetectedCanonicalGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.exists_uniform_early_canonical_slice_scales line 13
  2. theorem OAI.Erdos3.VectorPolynomial.exists_detected_uniform_early_canonical_slice_scales line 104
  3. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCanonicalSlice_early_radius line 214
  4. theorem OAI.Erdos3.VectorPolynomial.preparedCommonCanonicalKernel_capacity line 277
  5. def OAI.Erdos3.VectorPolynomial.preparedCommonCanonicalSelection line 281
  6. theorem OAI.Erdos3.VectorPolynomial.preparedCommonCanonicalSelection_val line 289
  7. theorem OAI.Erdos3.VectorPolynomial.exists_prepared_detected_canonical_slice_scales line 292
  8. theorem OAI.Erdos3.VectorPolynomial.chart_budget_le_exp line 385

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

  9. theorem OAI.Erdos3.VectorPolynomial.coefficient_count_add_one_le_support line 393

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

  10. theorem OAI.Erdos3.VectorPolynomial.exists_prepared_detected_canonical_geometry line 417