OAI/Combinatorics/Progressions/Probability/CoefficientJetDensityFactors.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerMatrixImagePMF line 19
  2. theorem OAI.Erdos3.integerMatrixImagePMF_law line 23
  3. def OAI.Erdos3.mixedArrayImageDensity line 30
  4. theorem OAI.Erdos3.mixedArrayImageDensity_measurable line 35
  5. theorem OAI.Erdos3.mixedArrayImageDensity_nonneg line 45
  6. theorem OAI.Erdos3.mixedArrayImageDensity_integrable line 52
  7. theorem OAI.Erdos3.mixedArrayImageDensity_law line 61
  8. theorem OAI.Erdos3.mixedArrayImageDensity_probability line 108
  9. theorem OAI.Erdos3.mixedArrayImageDensity_mass line 116
  10. def OAI.Erdos3.jointMixedCoefficientDensity line 140
  11. theorem OAI.Erdos3.jointMixedCoefficientDensity_expand line 145
  12. theorem OAI.Erdos3.jointMixedCoefficientDensity_measurable line 150
  13. theorem OAI.Erdos3.jointMixedCoefficientDensity_nonneg line 158
  14. theorem OAI.Erdos3.jointMixedCoefficientDensity_integrable line 163
  15. theorem OAI.Erdos3.jointMixedCoefficientDensity_law line 168
  16. theorem OAI.Erdos3.jointMixedCoefficientDensity_scaled line 183
  17. theorem OAI.Erdos3.jointMixedCoefficientDensity_test_mean line 189
  18. theorem OAI.Erdos3.mixedArrayImageDensity_eq_jointMixed line 212
  19. theorem OAI.Erdos3.coefficientPMF_smooth_eq line 234
  20. theorem OAI.Erdos3.coefficientImagePMF_smooth_eq line 241
  21. theorem OAI.Erdos3.integerMatrixImagePMF_smooth_eq line 248
  22. theorem OAI.Erdos3.coefficientImagePMF_affine_eq line 258
  23. theorem OAI.Erdos3.pmf_map_injective_comp_apply line 281
  24. theorem OAI.Erdos3.integerMatrixImagePMF_reindex_rows line 286
  25. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetDensity_reindex_rows line 299
  26. def OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetImageDensity line 333
  27. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetImageDensity_measurable line 342
  28. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetImageDensity_nonneg line 349
  29. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetImageDensity_integrable line 357
  30. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetImageDensity_law line 366
  31. def OAI.Erdos3.VectorPolynomial.coefficientJetDensityFactor line 403
  32. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetImageDensity_axis_product line 408