OAI/Combinatorics/Progressions/Estimates/AllocatedCommonCover.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedCommonScale line 19
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonScale_lower line 24
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonScale_period_window line 33
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonScale_upper line 54
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonScale_refined_period_window line 89
  6. def OAI.Erdos3.VectorPolynomial.allocatedRefinedPeriodLog line 135
  7. def OAI.Erdos3.VectorPolynomial.allocatedRefinedPeriodCutoff line 138
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedPeriodCutoff_bounds line 141
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedPeriodCutoff_contains line 149
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedPeriodCutoff_contains_power line 167
  11. abbrev OAI.Erdos3.VectorPolynomial.AllocatedRefinedPeriodCandidate line 178
  12. def OAI.Erdos3.VectorPolynomial.allocatedRefinedPeriodCandidate line 181
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedPeriodCandidate_value line 190
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonScale_cutoff_window line 215
  15. abbrev OAI.Erdos3.VectorPolynomial.AllocatedRefinedPeriodIndex line 243
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedPeriodIndex_power line 246
  17. def OAI.Erdos3.VectorPolynomial.allocatedRefinedPeriodIndex line 254
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedPeriodIndex_value line 263
  19. abbrev OAI.Erdos3.VectorPolynomial.AllocatedFittingPeriod line 280
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedFittingPeriod_power line 283
  21. def OAI.Erdos3.VectorPolynomial.allocatedCommonFittingPeriod line 298
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonFittingPeriod_value line 313
  23. theorem OAI.Erdos3.VectorPolynomial.common_scale_good_kernel_ideal_cover_at_sampling line 387