OAI/Combinatorics/Progressions/Sampling/AllocatedIdealGridEnvelope.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedIdealRadiusEnvelope line 16
  2. def OAI.Erdos3.VectorPolynomial.allocatedProxyLipEnvelope line 19
  3. def OAI.Erdos3.VectorPolynomial.allocatedIdealLipEnvelope line 22
  4. def OAI.Erdos3.VectorPolynomial.allocatedIdealGridEnvelope line 25
  5. def OAI.Erdos3.VectorPolynomial.allocatedIdealMeshEnvelope line 29
  6. def OAI.Erdos3.VectorPolynomial.allocatedIdealVolumeEnvelope line 32
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealGridEnvelope_nonneg line 37
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealGridEnvelope_bounds line 46
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealRadius_le_exp line 69
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedProxyLip_le_exp line 92
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientErrorVolume_le_exp line 108
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealGridAllowance_le_exp line 118