OAI/Combinatorics/Progressions/Estimates/PreparedRelativeEndpointSourceBounds.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.integerAxisSideLength_one_of_scale_one line 11
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.sides_free line 42
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.sides_continuous line 44
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.sides_integer line 48
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.sides_active line 54
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.sides_one_of_basisAxisScale_one line 61
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.sides_long_or_bounded_integer_axis line 68
  8. def OAI.Erdos3.VectorPolynomial.preparedNestedScalarAnchorFloor line 99
  9. theorem OAI.Erdos3.VectorPolynomial.preparedNestedScalarAnchorFloor_bounds line 103
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.free_axis_nested_floor line 130
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_free_axis_nested_floor line 142
  12. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointMinimumScale line 161
  13. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointMinimumLog line 166
  14. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointGoodCutoff line 171
  15. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointGoodLog line 174
  16. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointAmbientLog line 176
  17. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointMinimumScale_nested line 179
  18. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointMinimumScale_bounds line 188
  19. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointGoodCutoff_bounds line 220
  20. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointAmbientLog_bounds line 230
  21. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointScalarKnobs_power_bounds line 240
  22. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointSigmaLog_eq line 302
  23. theorem OAI.Erdos3.VectorPolynomial.preparedComparisonContinuousDimension_le_two line 318
  24. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpoint_source_bounds line 336