OAI/Probability/JammingConcavity/PolynomialComparison.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Polynomial Comparison.

  1. lemma OAI.MicroscopicJamming.backward_positive_strict_compact line 29
  2. def OAI.MicroscopicJamming.polynomialBarrier line 82
  3. lemma OAI.MicroscopicJamming.polynomialBarrier_space line 85
  4. lemma OAI.MicroscopicJamming.polynomialBarrier_space2 line 92
  5. lemma OAI.MicroscopicJamming.polynomialBarrier_time line 103
  6. lemma OAI.MicroscopicJamming.polynomial_transport_neg line 110
  7. lemma OAI.MicroscopicJamming.backward_polynomial_bound line 134
  8. lemma OAI.MicroscopicJamming.backward_polynomial_comparison line 224
  9. lemma OAI.MicroscopicJamming.backward_reaction_upper line 266
  10. lemma OAI.MicroscopicJamming.backward_reaction_bound line 337
  11. lemma OAI.MicroscopicJamming.forward_reaction_bound line 366
  12. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_third_bound line 408
  13. lemma OAI.MicroscopicJamming.Higher.gaussianRowComposition_third_bound line 468
  14. theorem OAI.MicroscopicJamming.gaussian_step_third line 534
  15. def OAI.MicroscopicJamming.GaussianStepGradientTimeStatement line 562
  16. lemma OAI.MicroscopicJamming.deriv_secant_error line 580
  17. theorem OAI.MicroscopicJamming.gaussian_step_gradient_time line 598