OAI/Combinatorics/Progressions/Estimates/PreparedFiniteForwardFixedCenterThreshold.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardPairedSourcePrecision line 11
  2. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardPairedSourcePrecision_model line 20
  3. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardPairedSourcePrecision_direct line 26
  4. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardPairedSourcePrecision_nonneg line 34
  5. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardPairedSourcePrecision_budget line 44
  6. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardPairedSourcePrecision_threshold line 78
  7. def OAI.Erdos3.VectorPolynomial.candidateNestedForwardSeedPolynomial line 114
  8. def OAI.Erdos3.VectorPolynomial.candidateNestedForwardSeed line 120
  9. theorem OAI.Erdos3.VectorPolynomial.candidateNestedForwardSeed_zero line 124
  10. theorem OAI.Erdos3.VectorPolynomial.candidateNestedForwardSeed_succ line 128
  11. theorem OAI.Erdos3.VectorPolynomial.candidateNestedForwardSeed_nonneg line 136
  12. theorem OAI.Erdos3.VectorPolynomial.candidateNestedForwardSeed_monotone line 141
  13. theorem OAI.Erdos3.VectorPolynomial.le_candidateNestedForwardSeed line 157
  14. theorem OAI.Erdos3.VectorPolynomial.candidateNestedForwardWork_le_next_seed line 163
  15. theorem OAI.Erdos3.VectorPolynomial.exists_candidateNestedForwardSeed_polynomial_budget line 175
  16. theorem OAI.Erdos3.VectorPolynomial.exists_candidateNestedForwardLocal_budget line 191
  17. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardInnerDetectionThreshold_bound line 241
  18. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardInnerDetectionThreshold_loss line 265
  19. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardInnerDetectionThreshold_le_gain_half line 287
  20. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceRequired line 317
  21. theorem OAI.Erdos3.VectorPolynomial.one_le_preparedFiniteNestedSourceRequired line 331
  22. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceRequired_nonneg line 344
  23. theorem OAI.Erdos3.VectorPolynomial.anchorGoodRequired_le_preparedFiniteNestedSourceRequired line 351
  24. theorem OAI.Erdos3.VectorPolynomial.conditionalRequired_le_preparedFiniteNestedSourceRequired line 364
  25. theorem OAI.Erdos3.VectorPolynomial.detectorRequired_le_preparedFiniteNestedSourceRequired line 377
  26. theorem OAI.Erdos3.VectorPolynomial.cumulative_le_preparedFiniteNestedSourceRequired line 390
  27. theorem OAI.Erdos3.VectorPolynomial.cumulative_le_preparedFiniteNestedSourceRequired_of_le line 423
  28. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceRequired_size_rank line 433
  29. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedSourceRequired_power_budget line 474
  30. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedSourceRequired_raised_power_budget line 559
  31. theorem OAI.Erdos3.four_le_exp_neg_mul_of_exp_floor line 597
  32. theorem OAI.Erdos3.preparedFiniteNestedSourceTrimExponential line 615
  33. theorem OAI.Erdos3.VectorPolynomial.two_mul_add_ten_le_preparedFiniteForwardCumulative_one line 636
  34. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceRequired_trim_log line 653
  35. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceRequired_trim_bounds line 674
  36. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardPairedSourcePrecision_model_lower line 701
  37. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardFixedCenterThreshold_lower line 719
  38. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardFixedCenterThreshold_half_le_one line 732