OAI/Combinatorics/Progressions/Estimates/AllocatedRefinedCoverError.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_fiber_reconstruction_error line 11
  2. theorem OAI.Erdos3.BooleanCubeKernel.physicalReconstruction_fiber_error line 50
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedLongProfileDensity_eq_of_periods line 149
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeMaskedGridlessProfile_eq_of_periods line 180
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeMaskedCoveredProfile_eq_of_periods line 195
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeMaskedCoveredProfile_refine line 210
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedResidueSiteProfile_refined_error line 285
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedCover_reconstruction_error line 296