OAI/Combinatorics/Progressions/Estimates/PreparedFiniteForwardTreeStorage.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardPrefixLog line 11
  2. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCumulative line 15
  3. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardModelPrecision line 19
  4. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardSourcePrecision line 24
  5. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardParameter_prefix line 29
  6. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForward_prefix_bounds line 43
  7. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForward_model_precision_bounds line 58
  8. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForward_phase_cap line 88
  9. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForward_branch_count_log line 110
  10. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForward_model_scalar_bounds line 122
  11. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCumulative_succ line 161
  12. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCumulative_nonneg line 168
  13. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCumulative_le_succ line 173
  14. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCumulative_monotone line 180
  15. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCap_le_cumulative_succ line 187
  16. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCap_le_cumulative line 194
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateForwardStage_bounds line 202
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateForwardStage_phase_bounds line 216
  19. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForward_controlled_slice_bounds line 245
  20. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForward_slice_mul_count_le_work line 287
  21. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForward_endpoint_scalar_bounds line 313
  22. def OAI.Erdos3.VectorPolynomial.allocatedCandidateForwardControlInput line 371
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateForwardControlInput_bounds line 374
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateForwardControlInput_denominator_bound line 393
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateForwardControlInput_cost_bound line 421
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateForwardControlInput_power_bound line 444
  27. theorem OAI.Erdos3.VectorPolynomial.le_preparedFiniteForwardCumulative line 502
  28. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardParameter_le_count line 526
  29. theorem OAI.Erdos3.VectorPolynomial.le_preparedFiniteForwardCount line 533
  30. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCap_le_count line 539
  31. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCumulative_le_count line 546
  32. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCount_le_parameter_succ line 553
  33. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCount_le_parameter line 561
  34. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardTreeStorage_bounds line 569
  35. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardTreeStorage_structural_bounds line 592