OAI/Combinatorics/Progressions/Estimates/AllocatedCorrelatedModeratePlateau.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.correlatedModerateFourierCoefficient line 19
  2. def OAI.Erdos3.correlatedModerateGridApproximation line 25
  3. def OAI.Erdos3.correlatedModeratePlateauApproximation line 31
  4. theorem OAI.Erdos3.correlatedModeratePointMass_zero_off_scaled_support line 37
  5. theorem OAI.Erdos3.correlatedModeratePointMass_eq_residue_buffered line 59
  6. theorem OAI.Erdos3.correlatedModeratePointMass_error_plateau line 83
  7. def OAI.Erdos3.VectorPolynomial.allocatedCorrelatedModeratePlateauApproximation line 164
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedCorrelatedModeratePlateau_error line 172
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedCorrelatedModeratePlateau_error_of_grid line 215
  10. def OAI.Erdos3.VectorPolynomial.allocatedCorrelatedModeratePlateauBudgetApproximation line 246
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedCorrelatedModeratePlateau_budget_error line 252
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedCorrelatedModeratePlateau_cover_card line 281