OAI/Combinatorics/Progressions/Probability/AllocatedDensityParameterBounds.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedProfileJet line 34
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedProfileJet_measurable line 41
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedKernelJet_eq line 63
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedMonomialProfile_unit_law line 74
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousProfileJet_unit_law line 106
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerProfileJet_unit_law line 125
  7. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedLongJetFactor line 175
  8. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedLongJetMap line 180
  9. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedLongJetDensity line 185
  10. def OAI.Erdos3.VectorPolynomial.allocatedContinuousLongJetProxy line 189
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedLongJetFactor_probability line 194
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedLongJetFactor_measurable line 205
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedLongJetMap_measurable line 215
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedLongJetDensity_measurable line 231
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedLongJetDensity_probability line 245
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedLongJetDensity_unit_law line 259
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousLongJetProxy_image_law line 284
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousLongJetProxy_probability line 296
  19. theorem OAI.Erdos3.principalAxisParameter_card_le line 315
  20. theorem OAI.Erdos3.principalAxisColumnLip_le_exp line 329
  21. def OAI.Erdos3.VectorPolynomial.allocatedDensityColumnLog line 347
  22. def OAI.Erdos3.VectorPolynomial.allocatedDensityLog line 352
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedDensityLog_bounds line 358
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedDensityKernel_bounds line 425
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousKernelDensity_exp_bounds line 480
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerKernelDensity_exp_bounds line 490
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetTarget_exp_bounds line 501
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedLongJetDensity_parameter_bounds line 564