OAI/Combinatorics/Progressions/Probability/AllocatedSlicedIdealDensity.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.jointSlicedPrincipalDensity line 17
  2. theorem OAI.Erdos3.jointSlicedPrincipalDensity_image_probability line 22
  3. theorem OAI.Erdos3.jointSlicedPrincipalDensity_measurable_family line 49
  4. theorem OAI.Erdos3.jointSlicedPrincipalDensity_coordinate_product line 71
  5. theorem OAI.Erdos3.jointSlicedPrincipalDensity_cap_lipschitz line 82
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedAxisProfilePolynomial_principal_coeff line 124
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedAxisProfilePolynomial_constant_coeff line 146
  8. def OAI.Erdos3.VectorPolynomial.allocatedFixedPathPrincipal line 170
  9. def OAI.Erdos3.VectorPolynomial.allocatedFixedPathShift line 175
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathPrincipal_eq line 179
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathShift_eq line 194
  12. def OAI.Erdos3.VectorPolynomial.allocatedFixedPathLiftMap line 201
  13. def OAI.Erdos3.VectorPolynomial.allocatedFixedPathLiftDensity line 207
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathPrincipal_bounds line 214
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathLiftDensity_law_probability line 224
  16. def OAI.Erdos3.VectorPolynomial.allocatedFixedPathLiftRowCap line 244
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathLiftDensity_cap_lipschitz line 251
  18. def OAI.Erdos3.VectorPolynomial.allocatedSlicedNormalizedIdeal line 297
  19. def OAI.Erdos3.VectorPolynomial.allocatedSlicedConditionalIdealDensity line 305
  20. def OAI.Erdos3.VectorPolynomial.allocatedSlicedAveragedIdealDensity line 313
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedNormalizedIdeal_measurable line 318
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedConditionalIdealDensity_measurable line 327
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedConditionalIdealDensity_law_probability line 346
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedAveragedIdealDensity_law_probability line 367