OAI/Combinatorics/Progressions/Polynomial/PolynomialShearParameterBudget.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.shifted_power_le_fixed_base line 15
  2. theorem OAI.Erdos3.exists_natPolynomial_fixed_power_budget line 33
  3. theorem OAI.Erdos3.exists_natPolynomial_affine_budget line 41
  4. def OAI.Erdos3.relativeInductionBudgetPolynomial line 60
  5. theorem OAI.Erdos3.relativeInductionBudgetPolynomial_eval_zero line 65
  6. theorem OAI.Erdos3.relativeInductionBudgetPolynomial_eval_succ line 69
  7. theorem OAI.Erdos3.relativeInductionBudgetPolynomial_nonneg line 76
  8. theorem OAI.Erdos3.exists_relativeInductionPolynomialBudget line 80
  9. def OAI.Erdos3.relativeInductionBudgetValue line 96
  10. theorem OAI.Erdos3.relativeInductionBudgetValue_zero line 99
  11. theorem OAI.Erdos3.relativeInductionBudgetValue_succ line 103
  12. theorem OAI.Erdos3.relativeInductionBudgetValue_majorizes line 108
  13. theorem OAI.Erdos3.exists_relativeInductionBudget_majorization line 131
  14. theorem OAI.Erdos3.polynomialBudget_four_slack line 152
  15. theorem OAI.Erdos3.quarterAccuracy_polynomial_budget line 164
  16. theorem OAI.Erdos3.polynomialShearExp_sub_mass line 188
  17. theorem OAI.Erdos3.polynomialShearExp_displacement line 234
  18. theorem OAI.Erdos3.polynomialShearExp_X_displacement line 249
  19. def OAI.Erdos3.polynomialShearDisplacementBound line 274
  20. theorem OAI.Erdos3.polynomialShearRealPointAction_eq_exp line 277
  21. theorem OAI.Erdos3.polynomialShearRealPointAction_displacement line 287
  22. theorem OAI.Erdos3.polynomialShearRealification_ordered_repr line 310
  23. theorem OAI.Erdos3.polynomialShearRealPointAction_near_one line 338
  24. theorem OAI.Erdos3.PolynomialSlots.topResidualPoint_lipschitzOn_box line 393
  25. theorem OAI.Erdos3.PolynomialSlots.topResidualInversePoint_lipschitzOn_box line 410
  26. theorem OAI.Erdos3.PolynomialPatch.shearKernel_lipschitzOn_box line 434
  27. def OAI.Erdos3.PolynomialPatch.shearKernelLipBound line 441
  28. theorem OAI.Erdos3.PolynomialPatch.shearKernel_lipschitz line 445
  29. theorem OAI.Erdos3.PolynomialPatch.normalized_shearKernel_lipschitz line 461
  30. def OAI.Erdos3.PolynomialPatch.shearObservableLipBound line 486
  31. theorem OAI.Erdos3.PolynomialPatch.shearSummand_lipschitz line 496
  32. theorem OAI.Erdos3.PolynomialPatch.shearOrbitSum_lipschitz line 536
  33. theorem OAI.Erdos3.PolynomialPatch.shearObservable_lipschitz line 553
  34. theorem OAI.Erdos3.PolynomialPatch.normalized_shearObservable_lipschitz line 569
  35. def OAI.Erdos3.shearKernelLogBudget line 592
  36. def OAI.Erdos3.shearActionLogBudget line 595
  37. theorem OAI.Erdos3.shearKernelLogBudget_nonneg line 599
  38. theorem OAI.Erdos3.shearActionLogBudget_nonneg line 602
  39. theorem OAI.Erdos3.shearRadius_le_exp line 605
  40. theorem OAI.Erdos3.shearKernelLipBound_le_exp line 614
  41. theorem OAI.Erdos3.shearDisplacementBound_le_exp line 638
  42. theorem OAI.Erdos3.shearObservable_log_bound line 659
  43. theorem OAI.Erdos3.exists_shear_parameter_budget line 699