OAI/Combinatorics/Progressions/Estimates/AllocatedFiberCap.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.coefficientFiberMap line 16
  2. theorem OAI.Erdos3.VectorPolynomial.coefficientFiberMap_evaluation line 23
  3. theorem OAI.Erdos3.VectorPolynomial.coefficientFiberMap_retraction line 30
  4. theorem OAI.Erdos3.VectorPolynomial.coefficientFiberMap_nonconstant line 37
  5. theorem OAI.Erdos3.VectorPolynomial.coefficientFiberMap_continuous line 46
  6. def OAI.Erdos3.VectorPolynomial.coefficientConstantCenter line 66
  7. theorem OAI.Erdos3.VectorPolynomial.coefficientConstantCenter_continuous line 70
  8. theorem OAI.Erdos3.VectorPolynomial.coefficientConstantCenter_add_constant line 75
  9. theorem OAI.Erdos3.VectorPolynomial.coefficientConstantCenter_idempotent line 83
  10. theorem OAI.Erdos3.VectorPolynomial.coefficientConstantCenter_nonconstant line 88
  11. theorem OAI.Erdos3.VectorPolynomial.coefficientConstantCenter_integral_add_constant line 94
  12. def OAI.Erdos3.VectorPolynomial.coefficientFiberAverage line 114
  13. theorem OAI.Erdos3.VectorPolynomial.coefficientFiberAverage_bound line 122
  14. theorem OAI.Erdos3.VectorPolynomial.coefficientFiberAverage_approx line 133
  15. theorem OAI.Erdos3.VectorPolynomial.coefficientFiberAverage_nonneg line 147
  16. def OAI.Erdos3.VectorPolynomial.nonconstantCoefficientFactor line 165
  17. theorem OAI.Erdos3.VectorPolynomial.constantCoefficientCap_product line 171
  18. theorem OAI.Erdos3.VectorPolynomial.coefficientProductDensity_fiber_bound line 183
  19. theorem OAI.Erdos3.VectorPolynomial.coefficientFiberMap_translate line 217
  20. theorem OAI.Erdos3.VectorPolynomial.coefficientFiberAverage_translate line 224
  21. theorem OAI.Erdos3.VectorPolynomial.coefficientMixedFiber_joint_measurable line 252
  22. theorem OAI.Erdos3.VectorPolynomial.coefficientMixedFiber_joint_integrable line 260
  23. theorem OAI.Erdos3.VectorPolynomial.coefficientMixedFiber_integrable line 269
  24. theorem OAI.Erdos3.VectorPolynomial.coefficientMixedFiber_average line 277
  25. theorem OAI.Erdos3.VectorPolynomial.nonconstantCoefficientDensity_probability line 321
  26. theorem OAI.Erdos3.VectorPolynomial.coefficientProductDensity_fiberAverage_cap line 353
  27. def OAI.Erdos3.VectorPolynomial.canonicalCoefficientFactor line 407
  28. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDensity_product line 413
  29. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientFactor_measurable line 425
  30. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDensity_fiber_cap line 439
  31. theorem OAI.Erdos3.VectorPolynomial.exists_subtractive_constant_center line 478
  32. theorem OAI.Erdos3.VectorPolynomial.centeredAffineCoefficientTorus_eq_subtractive line 494
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientFactor_constant_cap line 527
  34. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientDensity_fiber_cap line 556
  35. theorem OAI.Erdos3.VectorPolynomial.selectedCoefficientDensity_fiber_cap line 568