OAI/Combinatorics/Progressions/Dynamics/PreparedPerturbativeSeedPowerBudget.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.slicedPrincipalBoundaryRadius_inverse_le_exp line 11
  2. theorem OAI.Erdos3.slicedPrincipalMinor_inverse_le_exp line 31
  3. theorem OAI.Erdos3.slicedPrincipalComparisonBudget_le_exp line 50
  4. def OAI.Erdos3.slicedPrincipalComparisonBudgetLog line 92
  5. theorem OAI.Erdos3.slicedPrincipalComparisonBudget_le_exp_of_separate_logs line 96
  6. theorem OAI.Erdos3.slicedEndpointUniformScale_inverse_le_exp line 131
  7. theorem OAI.Erdos3.slicedEndpointUniformScale_log_inverse_le line 190
  8. theorem OAI.Erdos3.unitProfilePrincipalLowerBound_inv_le_exp line 214
  9. theorem OAI.Erdos3.principalBlock_card_le_input_card line 232
  10. theorem OAI.Erdos3.unitProfilePrincipalLowerBound_inv_le_exp_of_input_card line 241
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedUnitProfilePrincipalLowerBound_inv_le_exp line 252
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftLip_eq_card line 288
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftLip_coe_eq_card line 291
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceLip_le_two line 296
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceLip_coe_le_two line 306
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftInput_card_le_allAxis line 311
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftLip_le_fullInputCount line 321
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftLip_coe_le_allAxis line 328
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftLip_le_exp_of_allAxis line 333
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceLip_le_two_exp_of_allAxis line 339
  21. def OAI.Erdos3.fixedPathPerturbationLog line 357
  22. theorem OAI.Erdos3.fixedPathPerturbationLog_nonneg line 361
  23. theorem OAI.Erdos3.fixedPathPerturbation_scale_lower line 367
  24. theorem OAI.Erdos3.fixedPathPerturbation_tail line 401
  25. theorem OAI.Erdos3.fixedPathPerturbation_tolerance_ratio_lower line 414
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathPerturbation_tail_uniform line 447
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathPerturbation_ratio_lower_uniform line 470
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathPerturbation_tail_of_inputCount line 493
  29. theorem OAI.Erdos3.VectorPolynomial.exists_preparedPerturbativeSeed_power_budget line 520