OAI/Combinatorics/Progressions/Estimates/PrincipalCoefficientMarginal.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.Homogeneous line 20
  2. theorem OAI.Erdos3.VectorPolynomial.homogeneous_tmul line 23
  3. theorem OAI.Erdos3.VectorPolynomial.homogeneous_support_degree line 28
  4. theorem OAI.Erdos3.VectorPolynomial.eq_of_homogeneous_tmul line 33
  5. def OAI.Erdos3.VectorPolynomial.siteEvaluation line 45
  6. theorem OAI.Erdos3.VectorPolynomial.siteEvaluation_tmul line 48
  7. def OAI.Erdos3.VectorPolynomial.siteFunctional line 51
  8. theorem OAI.Erdos3.VectorPolynomial.siteFunctional_tmul line 55
  9. theorem OAI.Erdos3.VectorPolynomial.curried_nonfactor line 65
  10. def OAI.Erdos3.VectorPolynomial.homogeneousPart line 94
  11. theorem OAI.Erdos3.VectorPolynomial.homogeneousPart_tmul line 98
  12. theorem OAI.Erdos3.VectorPolynomial.coefficients_homogeneousPart line 101
  13. theorem OAI.Erdos3.VectorPolynomial.homogeneousPart_homogeneous line 113
  14. theorem OAI.Erdos3.VectorPolynomial.homogeneousPart_eq_self line 118
  15. theorem OAI.Erdos3.VectorPolynomial.sub_homogeneousPart_degreeLE line 127
  16. theorem OAI.Erdos3.VectorPolynomial.coordinate_homogeneousPart line 141
  17. theorem OAI.Erdos3.independentProductPMF_marginal line 158
  18. theorem OAI.Erdos3.linearFunctional_eq_coordinate_sum line 178
  19. theorem OAI.Erdos3.realPolynomialMass_fin_prod_le line 187
  20. def OAI.Erdos3.VectorPolynomial.contractedRow line 199
  21. theorem OAI.Erdos3.VectorPolynomial.contractedRow_apply line 203
  22. def OAI.Erdos3.VectorPolynomial.MonomialRowBound line 208
  23. theorem OAI.Erdos3.VectorPolynomial.contractedRow_le_mass line 212
  24. theorem OAI.Erdos3.VectorPolynomial.contractedRow_prod_bound line 219
  25. theorem OAI.Erdos3.dependentProductPMF_marginal line 241
  26. def OAI.Erdos3.VectorPolynomial.coefficientFunctional line 270
  27. theorem OAI.Erdos3.VectorPolynomial.coefficientFunctional_monomial line 274
  28. theorem OAI.Erdos3.VectorPolynomial.coefficientFunctional_unit line 281
  29. theorem OAI.Erdos3.VectorPolynomial.coefficientFunctional_rowBound line 288
  30. abbrev OAI.Erdos3.VectorPolynomial.BoundedCoefficientExponent line 306
  31. instance OAI.Erdos3.VectorPolynomial.boundedCoefficientExponentFintype line 309
  32. abbrev OAI.Erdos3.VectorPolynomial.CoefficientSlot line 312
  33. abbrev OAI.Erdos3.VectorPolynomial.CoefficientArray line 315
  34. def OAI.Erdos3.VectorPolynomial.coefficientArrayFunctional line 318
  35. theorem OAI.Erdos3.VectorPolynomial.coefficientArrayFunctional_single line 329
  36. theorem OAI.Erdos3.VectorPolynomial.coefficientArrayFunctional_eq_zero_iff line 344
  37. theorem OAI.Erdos3.VectorPolynomial.exists_homogeneous_monomial_nonzero line 369
  38. theorem OAI.Erdos3.VectorPolynomial.homogeneous_empty_factorization_iff line 383
  39. theorem OAI.Erdos3.VectorPolynomial.exists_restricted_coefficient_nonzero line 396
  40. theorem OAI.Erdos3.VectorPolynomial.boundedCoefficientExponent_card_le line 418
  41. def OAI.Erdos3.BooleanCubeKernel.integerCubeWitnessBound line 459
  42. theorem OAI.Erdos3.BooleanCubeKernel.integerCubeWitnessBound_nonneg line 463
  43. theorem OAI.Erdos3.BooleanCubeKernel.integer_coefficient_le_mass line 468
  44. theorem OAI.Erdos3.BooleanCubeKernel.exists_integral_vector_mode_witness line 473
  45. theorem OAI.Erdos3.productBlockExponent_degree line 511
  46. theorem OAI.Erdos3.canonicalPrincipalExponent_degree line 515
  47. def OAI.Erdos3.constantCoefficientSlot line 520
  48. def OAI.Erdos3.principalCoefficientSlot line 523
  49. theorem OAI.Erdos3.principalCoefficientSlot_injective line 528
  50. def OAI.Erdos3.principalCoefficientSlots line 534
  51. theorem OAI.Erdos3.mem_principalCoefficientSlots line 540
  52. theorem OAI.Erdos3.principalCoefficientSlots_card line 547
  53. theorem OAI.Erdos3.constantCoefficientSlot_not_principal line 554
  54. def OAI.Erdos3.principalCoefficientChoice line 571
  55. theorem OAI.Erdos3.principalCoefficientChoice_injective line 577
  56. theorem OAI.Erdos3.principalCoefficientMarginal line 596