OAI/Combinatorics/Progressions/Probability/AllocatedActiveAxisSourceLaw.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.normalizedUniformCubeSource_toPMF line 11
  2. theorem OAI.Erdos3.integerScalarCubeWeights_normalized_source line 22
  3. theorem OAI.Erdos3.pmf_pair_law_map line 56
  4. theorem OAI.Erdos3.principalModerateSource_pair_law line 70
  5. theorem OAI.Erdos3.principalModerateSource_jet_law line 83
  6. def OAI.Erdos3.normalizedUniformTupleSources line 105
  7. theorem OAI.Erdos3.normalizedUniformTupleSources_law line 111
  8. theorem OAI.Erdos3.principalModerateSource_uniform_pair_law line 117
  9. theorem OAI.Erdos3.principalModerateSource_uniform_jet_law line 128
  10. theorem OAI.Erdos3.weightedModerateSource_pair_law line 156
  11. theorem OAI.Erdos3.weightedModerateSource_integer_pair_law line 168
  12. theorem OAI.Erdos3.dependentProductPMF_pair_transport line 193
  13. theorem OAI.Erdos3.finiteWeights_pi_pair_transport line 209
  14. theorem OAI.Erdos3.weightedModerateProductSource_pair_law line 232
  15. theorem OAI.Erdos3.weightedModerateProductSource_jet_sum_law line 254
  16. theorem OAI.Erdos3.pmf_map_law_transport line 285
  17. theorem OAI.Erdos3.integerScalarTuplePMF_congr line 290
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenTuple_single_block_marginal line 315
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenTuple_single_block_integer_law line 334
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenTuple_active_block_law line 351
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenTuple_active_normalized_block_law line 367
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenTuple_active_axis_normalized_law line 405
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveBlockSource_pair_law line 484
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveBlockSource_jet_law line 497
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveAxisSource_jet_sum_law line 541