OAI/Combinatorics/Progressions/Polynomial/CRTPolynomialInputAffineLaw.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.crtPrimePowerIntegerPolynomialOutput line 16
  2. theorem OAI.Erdos3.crtPrimePowerIntegerPolynomialOutput_reduce line 26
  3. def OAI.Erdos3.taggedPolynomialOutputCurry line 40
  4. theorem OAI.Erdos3.crt_integer_polynomial_rational_characteristic_decay line 59
  5. theorem OAI.Erdos3.crt_integer_polynomial_rational_order_bounds line 76
  6. theorem OAI.Erdos3.crt_integer_polynomial_rational_inactive_bounds line 103
  7. theorem OAI.Erdos3.finiteImageMass_outputEquiv line 156
  8. def OAI.Erdos3.localPrimePowerIntegerPolynomialOutput line 163
  9. theorem OAI.Erdos3.localPrimePowerIntegerPolynomialOutput_reduce line 169
  10. theorem OAI.Erdos3.crt_integer_polynomial_rational_density_product line 183
  11. theorem OAI.Erdos3.crt_integer_polynomial_rational_inactive_density_product line 239
  12. def OAI.Erdos3.prescribedCRTPolynomialInput line 278
  13. def OAI.Erdos3.crtPolynomialInputLaw line 290
  14. theorem OAI.Erdos3.crtPolynomialInputLaw_complexMean line 298
  15. theorem OAI.Erdos3.crtPolynomialInputLaw_integerLong_characteristic line 308
  16. theorem OAI.Erdos3.crtPolynomialInputLaw_integerLong_characteristic_of_output line 324
  17. theorem OAI.Erdos3.exists_uniform_indexed_positive_product_cutoff line 356
  18. theorem OAI.Erdos3.retainedPrimePowerModulus_dvd line 379
  19. theorem OAI.Erdos3.crt_integer_polynomial_retained_inactive_density_product line 386
  20. def OAI.Erdos3.crtInputAddEquiv line 443
  21. theorem OAI.Erdos3.crtPrimePowerPolynomialLaw_eq_uniform line 458
  22. def OAI.Erdos3.prescribedCRTStep line 469
  23. theorem OAI.Erdos3.prescribedCRTPolynomialInput_eq_affine line 476
  24. theorem OAI.Erdos3.crtPolynomialInputLaw_affine_uniform line 488