OAI/Combinatorics/Progressions/Estimates/AllocatedIdealRefinedPointwise.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.AllocatedComparisonDimensions.active_outputs line 18
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskPower_le_exp line 27
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalIdeal_error_le line 36
  4. def OAI.Erdos3.VectorPolynomial.allocatedPhysicalIdealLengthEnvelope line 81
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalIdealLengthEnvelope_nonneg line 86
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalIdealLengthEnvelope_bounds line 102
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalIdealLength_spec line 128
  8. def OAI.Erdos3.VectorPolynomial.allocatedIdealScaleInput line 154
  9. def OAI.Erdos3.VectorPolynomial.allocatedIdealScaleLog line 158
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealScaleInput_bounds line 163
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedComparisonDimensions.integer_axes line 181
  12. def OAI.Erdos3.VectorPolynomial.allocatedIdealScale line 195
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealScale_lower line 200
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealScale_upper line 206
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealScale_ready line 225
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalIdealLengthEnvelope_ge_parameter line 244
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealScale_principal_profile_le line 271
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealMeshEnvelope_ge_input line 294
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedIdeal_refined_length_bound line 321
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealScale_refined_threshold line 353
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealScale_refined_pointwise line 383