OAI/Combinatorics/Progressions/Estimates/AllocatedReferenceWindowTest.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.BooleanCubeKernel.smoothPhysicalResidue_window_expectation line 14
  2. theorem OAI.Erdos3.BooleanCubeKernel.physicalCenteredResidueMixture_window_error line 34
  3. theorem OAI.Erdos3.BooleanCubeKernel.physicalSelectedResidue_window_site_error line 77
  4. theorem OAI.Erdos3.canonicalVectorSpatialSiteApprox_shift_error line 118
  5. theorem OAI.Erdos3.BooleanCubeKernel.smoothPhysicalResidue_reference_window_error line 192
  6. theorem OAI.Erdos3.BooleanCubeKernel.physicalCenteredResidueMixture_reference_error line 220
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedTrimmedSpatial_reference_window line 289
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalColumns_difference_sum_bound line 371
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedTrimmedSpatial_shifted_vector_site_error line 390
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedTrimmedSpatial_reference_site_test line 503