OAI/Probability/JammingConcavity/GaussianStepRight.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Step Right.

  1. def OAI.MicroscopicJamming.gaussianStepRightCoefficient line 29
  2. lemma OAI.MicroscopicJamming.gaussianStepRightCoefficient_bounds line 33
  3. lemma OAI.MicroscopicJamming.gaussianStepRightCoefficient_trace line 45
  4. lemma OAI.MicroscopicJamming.gaussianStepRightCoefficient_close line 64
  5. lemma OAI.MicroscopicJamming.gaussianStepPath_cons_ge line 81
  6. lemma OAI.MicroscopicJamming.gaussianStepPath_right_pde line 92
  7. lemma OAI.MicroscopicJamming.localMax_second_deriv_nonpos line 146
  8. lemma OAI.MicroscopicJamming.backward_strict_compact line 176
  9. def OAI.MicroscopicJamming.quarticBarrier line 229
  10. lemma OAI.MicroscopicJamming.quarticBarrier_space line 232
  11. lemma OAI.MicroscopicJamming.quarticBarrier_space2 line 239
  12. lemma OAI.MicroscopicJamming.quarticBarrier_time line 250
  13. lemma OAI.MicroscopicJamming.quartic_transport_neg line 257
  14. lemma OAI.MicroscopicJamming.backward_quartic_bound line 270
  15. def OAI.MicroscopicJamming.BackwardComparisonStatement line 352
  16. theorem OAI.MicroscopicJamming.backward_comparison line 365
  17. def OAI.MicroscopicJamming.quadraticSourceBarrier line 392
  18. lemma OAI.MicroscopicJamming.quadraticSourceBarrier_space line 395
  19. lemma OAI.MicroscopicJamming.quadraticSourceBarrier_space2 line 403
  20. lemma OAI.MicroscopicJamming.quadraticSourceBarrier_time line 413
  21. lemma OAI.MicroscopicJamming.quadratic_transport_bound line 421
  22. def OAI.MicroscopicJamming.BackwardSourceComparisonStatement line 442
  23. theorem OAI.MicroscopicJamming.backward_source_comparison line 455
  24. lemma OAI.MicroscopicJamming.variance_difference_le line 515
  25. def OAI.MicroscopicJamming.GaussianStepStabilityStatement line 599
  26. theorem OAI.MicroscopicJamming.gaussian_step_stability line 611
  27. def OAI.MicroscopicJamming.GaussianStepThirdStatement line 683