OAI/Combinatorics/Progressions/Estimates/PreparedFiniteNestedSourceRelativeInitializerBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.exists_preparedUniformEarlyRadius line 12
  2. theorem OAI.Erdos3.twice_chartCoefficient_le_exp line 72
  3. theorem OAI.Erdos3.VectorPolynomial.preparedEarlyRadius_eighth_of_universal line 86
  4. theorem OAI.Erdos3.VectorPolynomial.preparedUniformEarlyRadius_eighth line 102
  5. theorem OAI.Erdos3.VectorPolynomial.preparedBadProduct_dimension_le_initial_allocation line 147
  6. theorem OAI.Erdos3.VectorPolynomial.preparedBadProduct_witness_count_le_dimension_sq line 153
  7. theorem OAI.Erdos3.VectorPolynomial.preparedBadProductWitnessGap_bounds line 161
  8. theorem OAI.Erdos3.VectorPolynomial.exists_preparedBadProductWitnessScale line 193
  9. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteCanonicalSource_counts line 235
  10. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSource_counts line 266
  11. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSource_relative_radius line 296
  12. def OAI.Erdos3.VectorPolynomial.preparedNestedRelativeCommonFloor line 325
  13. def OAI.Erdos3.VectorPolynomial.preparedNestedRelativeCommonFloorLog line 331
  14. theorem OAI.Erdos3.VectorPolynomial.preparedNestedRelativeCommonFloor_bounds line 337
  15. theorem OAI.Erdos3.VectorPolynomial.exists_preparedNestedRelativeCommonFloorLog_power_budget line 367
  16. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSource_relative_initializer_bounds line 411