OAI/Combinatorics/Progressions/Estimates/PreparedRelativeEndpointNumericalBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointForecastExponent line 10
  2. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointPerturbationExponent line 13
  3. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointGeometryScale line 16
  4. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointUniformKnob line 20
  5. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointGeometryScale_bounds line 25
  6. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointUniformKnob_bounds line 35
  7. theorem OAI.Erdos3.VectorPolynomial.exists_preparedRelativeEndpointUniformKnob_power_budget line 98
  8. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointPrimitiveExponent line 139
  9. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointInputBase line 142
  10. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointInputScale line 145
  11. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointInputBase_bounds line 150
  12. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointInputScale_bounds line 158
  13. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointInputScale_setup_bounds line 170
  14. theorem OAI.Erdos3.VectorPolynomial.exists_preparedRelativeEndpointInputScale_power_budget line 209
  15. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpoint_numerical_bounds line 235