OAI/Combinatorics/Progressions/Estimates/AllocatedAmbientLogBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedLayerMixedCap line 15
  2. def OAI.Erdos3.VectorPolynomial.allocatedLayerMixedLip line 19
  3. def OAI.Erdos3.VectorPolynomial.allocatedAmbientFactorCap line 25
  4. def OAI.Erdos3.VectorPolynomial.allocatedAmbientLayerLip line 28
  5. def OAI.Erdos3.VectorPolynomial.allocatedAmbientFactorLip line 33
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientFactorCap_one_le line 37
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerMixedInterpolation_bounds line 44
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientFactor_bounds line 72
  9. def OAI.Erdos3.allocatedMixedLog line 108
  10. theorem OAI.Erdos3.allocatedMixedLog_nonneg line 111
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerMixed_exp_bounds line 124
  12. theorem OAI.Erdos3.ambientInterpolation_constants_exp_bounds line 155
  13. def OAI.Erdos3.allocatedAmbientLog line 180
  14. theorem OAI.Erdos3.allocatedAmbientLog_nonneg line 183
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientConstants_exp_bounds line 193