OAI/Combinatorics/Progressions/Sampling/AllocatedForecastShortRawDependence.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceForecastRankConstant_dimension line 28
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruence_rational_order_bounds line 37
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruence_rational_inactive_bounds line 80
  4. def OAI.Erdos3.VectorPolynomial.allocatedForecastPolynomial line 150
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedForecastPolynomial_crt_decay_of_bad_product line 172
  6. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceDeepBadDepth line 240
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruence_bad_product_le_of_deep line 248
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruence_rational_order_bounds_of_deep_bad_product line 269
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruence_rational_inactive_bounds_of_deep_bad_product line 309
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedForecastPolynomial_rational_density_eq_crt line 374
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedForecastPolynomial_rational_density_product line 422
  12. theorem OAI.Erdos3.samplerSeparated_eval₂_raw_congr line 472
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedForecastPolynomial_eval₂_raw_congr line 503
  14. def OAI.Erdos3.VectorPolynomial.allocatedShortPrincipalRaw line 534
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedShortPrincipalRaw_restrict line 539
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedForecastPolynomial_short_raw line 547