OAI/Combinatorics/Progressions/Lattices/AllocatedAffineRadiusLog.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedAffineLongJetDensity line 36
  2. def OAI.Erdos3.VectorPolynomial.allocatedAffineLongJetProxy line 39
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLongJetDensity_measurable line 44
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLongJetDensity_probability line 57
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLongJetMap_measurable line 64
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLongJetProxy_image_law line 78
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLongJetProxy_probability line 98
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineLongJetProxy_test_integral line 108
  9. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_affine_tail_test_comparison line 166
  10. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_affine_proxy_comparison line 276
  11. def OAI.Erdos3.VectorPolynomial.allocatedAffineSourceTolerance line 322
  12. theorem OAI.Erdos3.VectorPolynomial.exists_early_allocated_affine_tail_test_comparison_with_scales line 328
  13. theorem OAI.Erdos3.VectorPolynomial.exists_early_allocated_affine_tail_test_comparison line 428
  14. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_affine_proxy_l1 line 492
  15. def OAI.Erdos3.VectorPolynomial.allocatedAffinePartitionLog line 542
  16. def OAI.Erdos3.VectorPolynomial.allocatedAffineToleranceLog line 554
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineSourceTolerance_log_bound line 557
  18. def OAI.Erdos3.VectorPolynomial.allocatedAffinePartitionRadiusLog line 588
  19. def OAI.Erdos3.VectorPolynomial.allocatedAffineRadiusLog line 595
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineSourceRadius_inverse_bound line 599
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineSourceRadius_uniform_floor line 614