OAI/Combinatorics/Progressions/Probability/AllocatedLongJetMixture.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.VectorPolynomial.AllocatedLongJetRows line 23
  2. def OAI.Erdos3.VectorPolynomial.allocatedLongJetReference line 26
  3. instance OAI.Erdos3.VectorPolynomial.allocatedLongJetReference_sigmaFinite line 30
  4. def OAI.Erdos3.VectorPolynomial.allocatedLongJetMap line 43
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetMap_measurable line 48
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetMap_reconstruct line 54
  7. def OAI.Erdos3.VectorPolynomial.allocatedLongJetFactor line 67
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetFactor_law line 76
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetFactor_measurable line 94
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetFactor_probability_data line 108
  11. def OAI.Erdos3.VectorPolynomial.allocatedLongJetDensity line 126
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetDensity_measurable line 129
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetDensity_probability_data line 134
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetDensity_law line 148
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJet_test_integral line 192
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJet_variable_test_mean line 205
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJet_test_mean line 225