OAI/Combinatorics/Progressions/Lattices/AllocatedActiveResidueComparison.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.integerBox_residue_fiberLaw_l1 line 11
  2. theorem OAI.Erdos3.integerBox_affine_residue_complexMean_error line 40
  3. theorem OAI.Erdos3.integerBox_affine_residue_complexMean_error_unconditional line 61
  4. theorem OAI.Erdos3.originalActiveCube_affine_residue_complexMean_error line 93
  5. theorem OAI.Erdos3.originalActiveCube_crt_input_comparison line 127
  6. theorem OAI.Erdos3.crtPolynomialInputLaw_unrestricted_divisor_complexMean line 147
  7. theorem OAI.Erdos3.originalActiveCube_crt_unrestricted_input_comparison line 164
  8. theorem OAI.Erdos3.rationalPolynomialForecast_unrestrictedCRT_marginal line 198
  9. theorem OAI.Erdos3.rationalInactivePolynomialForecast_conditionalUnrestrictedCRT_tsum_marginal line 220
  10. theorem OAI.Erdos3.rationalInactivePolynomialForecast_unrestrictedCRT_tsum_marginal line 248
  11. def OAI.Erdos3.VectorPolynomial.allocatedShortPrincipalResidueLaw line 306
  12. def OAI.Erdos3.VectorPolynomial.allocatedActivePrincipalResidueLaw line 309
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalResidue_partition line 312
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePrincipalResidue_length line 320
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePrincipalResidueLaw_eq line 323
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalResidue_partition_mul line 332
  17. theorem OAI.Erdos3.VectorPolynomial.scalarResidueIntegerMean_congr line 343
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePrincipalResidueLaw_integer_mean line 354
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalResidue_integer_partition line 376
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedActive_affine_residue_comparison line 416