OAI/Combinatorics/Progressions/Polynomial/EmbeddedMatrixDeterminantPolynomial.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.polynomial_det_totalDegree_le line 20
  2. theorem OAI.Erdos3.coordinateMatrixPolynomial_totalDegree line 38
  3. def OAI.Erdos3.unitMvPolynomialSublevel line 55
  4. theorem OAI.Erdos3.unitMvPolynomialSublevel_measurable line 58
  5. theorem OAI.Erdos3.unitMvPolynomialSublevel_volume_ne_top line 63
  6. def OAI.Erdos3.multivariateSublevelConstant line 70
  7. theorem OAI.Erdos3.multivariateSublevelConstant_pos line 73
  8. theorem OAI.Erdos3.multivariate_polynomial_sublevel_bound line 78
  9. theorem OAI.Erdos3.weighted_multivariate_polynomial_sublevel_bound line 91
  10. def OAI.Erdos3.boxMvPolynomialSublevel line 121
  11. theorem OAI.Erdos3.boxMvPolynomialSublevel_eq_smul line 124
  12. theorem OAI.Erdos3.boxMvPolynomialSublevel_volume line 153
  13. theorem OAI.Erdos3.boxMvPolynomialSublevel_volume_ne_top line 161
  14. theorem OAI.Erdos3.polynomial_sublevel_box_bound line 166
  15. theorem OAI.Erdos3.polynomial_sublevel_bounded_set_bound line 178
  16. theorem OAI.Erdos3.weighted_polynomial_sublevel_bounded_set_bound line 200
  17. theorem OAI.Erdos3.polynomial_sublevel_bound_of_value line 222
  18. theorem OAI.Erdos3.weighted_polynomial_sublevel_bound_of_value line 235
  19. theorem OAI.Erdos3.polynomial_det_exists_large_coefficient line 261
  20. theorem OAI.Erdos3.polynomial_det_sublevel_bound line 274
  21. theorem OAI.Erdos3.weighted_polynomial_det_sublevel_bound line 291
  22. theorem OAI.Erdos3.polynomial_grid_sublevel_transfer line 322
  23. theorem OAI.Erdos3.polynomial_grid_sublevel_bound_of_value line 363
  24. def OAI.Erdos3.normalizedMatrixEntryIndex line 394
  25. def OAI.Erdos3.normalizedMatrixDeterminantPolynomial line 397
  26. def OAI.Erdos3.normalizedMatrixIdentityPoint line 401
  27. theorem OAI.Erdos3.normalizedMatrixDeterminantPolynomial_eval line 404
  28. theorem OAI.Erdos3.normalizedMatrixDeterminantPolynomial_degree line 409
  29. theorem OAI.Erdos3.normalizedMatrixDeterminantPolynomial_totalDegree line 414
  30. theorem OAI.Erdos3.normalizedMatrixIdentityPoint_bound line 419
  31. theorem OAI.Erdos3.normalizedMatrixDeterminantPolynomial_identity line 424
  32. def OAI.Erdos3.normalizedMatrixDeterminantLip line 434
  33. theorem OAI.Erdos3.normalizedMatrixDeterminantLip_nonneg line 437
  34. theorem OAI.Erdos3.normalizedMatrixDeterminantPolynomial_derivative line 442
  35. theorem OAI.Erdos3.normalizedMatrixDeterminantPolynomial_lipschitz line 459
  36. theorem OAI.Erdos3.normalizedMatrixDeterminantPolynomial_sublevel line 474
  37. theorem OAI.Erdos3.normalizedMatrixDeterminantPolynomial_zero_eval line 487
  38. def OAI.Erdos3.reindexPolynomialMatrix line 502
  39. theorem OAI.Erdos3.reindexPolynomialMatrix_degreeOf line 506
  40. theorem OAI.Erdos3.reindexPolynomialMatrix_eval line 513
  41. theorem OAI.Erdos3.reindexed_polynomial_det_sublevel_bound line 520
  42. theorem OAI.Erdos3.weighted_reindexed_polynomial_det_sublevel_bound line 545
  43. theorem OAI.Erdos3.shiftedPolynomial_grid_sublevel_transfer line 583
  44. theorem OAI.Erdos3.shiftedPolynomial_grid_sublevel_bound_of_value line 621
  45. def OAI.Erdos3.embeddedMatrixDeterminantPolynomial line 657
  46. def OAI.Erdos3.embeddedMatrixIdentityPoint line 661
  47. theorem OAI.Erdos3.embeddedMatrixIdentityPoint_entry line 665
  48. theorem OAI.Erdos3.embeddedMatrixIdentityPoint_bound line 677
  49. theorem OAI.Erdos3.embeddedMatrixDeterminantPolynomial_eval line 682
  50. theorem OAI.Erdos3.embeddedMatrixDeterminantPolynomial_degree line 688
  51. theorem OAI.Erdos3.embeddedMatrixDeterminantPolynomial_totalDegree line 694
  52. theorem OAI.Erdos3.embeddedMatrixDeterminantPolynomial_identity line 700
  53. def OAI.Erdos3.embeddedMatrixDeterminantLip line 710
  54. theorem OAI.Erdos3.embeddedMatrixDeterminantLip_nonneg line 713
  55. theorem OAI.Erdos3.embeddedMatrixDeterminantPolynomial_derivative line 718
  56. theorem OAI.Erdos3.embeddedMatrixDeterminantPolynomial_lipschitz line 734
  57. theorem OAI.Erdos3.embeddedMatrixDeterminantPolynomial_sublevel line 750
  58. theorem OAI.Erdos3.embeddedMatrixDeterminantPolynomial_zero_eval line 765