OAI/Combinatorics/Progressions/Geometry/AllocatedGeometricInputBudget.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.allocatedUniformChartLog line 12
  2. theorem OAI.Erdos3.allocatedUniformChartLog_nonneg line 14
  3. theorem OAI.Erdos3.exists_uniform_projected_chart line 17
  4. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_uniform_charts line 41
  5. def OAI.Erdos3.VectorPolynomial.allocatedGeometryInput line 68
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedGeometryInput_bounds line 72
  7. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedGeometryInput_bound line 88
  8. def OAI.Erdos3.VectorPolynomial.allocatedGeometrySourceInput line 97
  9. theorem OAI.Erdos3.VectorPolynomial.exists_geometric_good_kernel_ideal_cover_family line 152
  10. theorem OAI.Erdos3.VectorPolynomial.geometric_good_kernel_ideal_cover_at_sampling line 351
  11. def OAI.Erdos3.VectorPolynomial.allocatedGeometricSourceBudget line 488
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedGeometricSourceBudget_controls line 493
  13. theorem OAI.Erdos3.VectorPolynomial.map_allocatedGeometricSourceBudget line 507
  14. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedGeometricSourceBudget_bound line 523