OAI/Combinatorics/Progressions/Lattices/AllocatedCoefficientIntegerMarginal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.mixedScalarArrayLaw_integer_marginal line 11
  2. theorem OAI.Erdos3.pmf_bind_pair_toMeasure line 20
  3. abbrev OAI.Erdos3.VectorPolynomial.CoefficientIntegerScalarIndex line 36
  4. def OAI.Erdos3.VectorPolynomial.coefficientIntegerScalars line 39
  5. theorem OAI.Erdos3.VectorPolynomial.coefficientIntegerScalars_measurable line 43
  6. theorem OAI.Erdos3.VectorPolynomial.coefficientIntegerScalars_measurePreserving line 51
  7. def OAI.Erdos3.VectorPolynomial.allocatedCoefficientIntegerPMF line 87
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientSource_integer_measurePreserving line 91
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientSource_integer_map line 101
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientSource_integer_prod_measurePreserving line 106
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientSource_integer_prod_integral line 119
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientSource_integer_prod_complexMean line 132
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientSource_integer_prod_eventProbability line 150
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientSource_integer_prod_indicator line 179