OAI/Probability/JammingConcavity/CylinderSecants.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Cylinder Secants.

  1. lemma OAI.MicroscopicJamming.deriv_difference_secant line 29
  2. def OAI.MicroscopicJamming.CylinderCauchy line 50
  3. lemma OAI.MicroscopicJamming.CylinderCauchy.deriv line 54
  4. lemma OAI.MicroscopicJamming.CylinderCauchy.exists_limit line 84
  5. lemma OAI.MicroscopicJamming.continuousOn_spatial_deriv line 102
  6. lemma OAI.MicroscopicJamming.cylinder_limit_continuous line 129
  7. def OAI.MicroscopicJamming.CylinderConvergence line 157
  8. lemma OAI.MicroscopicJamming.CylinderConvergence.tendsto_at line 161
  9. lemma OAI.MicroscopicJamming.cylinder_limit_hasDerivAt line 167
  10. lemma OAI.MicroscopicJamming.exists_cylinder_c2_limit line 188
  11. lemma OAI.MicroscopicJamming.gaussian_step_cylinder_cauchy line 235
  12. lemma OAI.MicroscopicJamming.gaussian_step_c2_limit line 266
  13. lemma OAI.MicroscopicJamming.gaussianStepRightCoefficient_close_continuous line 313
  14. lemma OAI.MicroscopicJamming.gaussianStepRightCoefficient_tendsto line 327
  15. lemma OAI.MicroscopicJamming.hasDerivAt_of_uniform_right_derivatives line 349
  16. lemma OAI.MicroscopicJamming.tendstoUniformlyOn_mul_bounded line 402
  17. lemma OAI.MicroscopicJamming.CylinderConvergence.time_slice line 432
  18. lemma OAI.MicroscopicJamming.gaussian_c2_limit_time line 440
  19. lemma OAI.MicroscopicJamming.gaussianStepPath_value_bounds line 504
  20. lemma OAI.MicroscopicJamming.gaussian_classical_limit line 516
  21. def OAI.MicroscopicJamming.gaussianGrid line 575
  22. lemma OAI.MicroscopicJamming.gaussianGrid_time line 579
  23. lemma OAI.MicroscopicJamming.gaussianGrid_valid line 588
  24. lemma OAI.MicroscopicJamming.gaussianGrid_coefficient_sample line 606
  25. lemma OAI.MicroscopicJamming.exists_gaussian_grid_approximation line 634