OAI/Combinatorics/Progressions/Polynomial/PolynomialDifferencePermanentIndependence.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.polynomialIterDifference_zero line 17
  2. theorem OAI.Erdos3.polynomialIterDifference_sum line 23
  3. theorem OAI.Erdos3.polynomialIterDifference_sub line 32
  4. theorem OAI.Erdos3.polynomialIterDifference_eq_zero_of_totalDegree_lt line 40
  5. theorem OAI.Erdos3.pderiv_polynomialTranslate line 51
  6. theorem OAI.Erdos3.pderiv_polynomialIterDifference line 64
  7. theorem OAI.Erdos3.polynomialIterDifference_linearCoeff line 75
  8. theorem OAI.Erdos3.pderiv_prod_X_of_notMem line 82
  9. theorem OAI.Erdos3.pderiv_prod_X_of_mem line 91
  10. theorem OAI.Erdos3.polynomialIterDifference_prod_X_linearCoeff_zero line 97
  11. theorem OAI.Erdos3.totalDegree_prod_X_le line 104
  12. theorem OAI.Erdos3.polynomialDifference_prod_X line 114
  13. theorem OAI.Erdos3.polynomialIterDifference_prod_X_step line 127
  14. theorem OAI.Erdos3.polynomialIterDifference_prod_X_eq_permanent line 162
  15. theorem OAI.Erdos3.polynomialIterDifference_prod_X_linearCoeff_permanent line 179
  16. theorem OAI.Erdos3.polynomialIterDifference_prod_X_linearCoeff_matrix_permanent line 188
  17. theorem OAI.Erdos3.polynomialIterDifference_designated_linearCoeff line 201
  18. theorem OAI.Erdos3.polynomialIterDifference_disjoint_designated_linearCoeff line 221
  19. theorem OAI.Erdos3.FiniteProbabilityWeights.pi_uniform_mean line 244
  20. theorem OAI.Erdos3.uniform_expect_coordinate_pullback line 258
  21. theorem OAI.Erdos3.productMean_prod_disjoint line 276
  22. theorem OAI.Erdos3.uniform_expect_prod_disjoint_tuples line 309
  23. theorem OAI.Erdos3.uniform_expect_prod_disjoint_tuples_le line 331
  24. theorem OAI.Erdos3.uniform_expect_prod_disjoint_permanents line 348