OAI/Probability/JammingConcavity/GaussianStepSlope.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Step Slope.

  1. lemma OAI.MicroscopicJamming.slope_bound_from_curvature line 26
  2. theorem OAI.MicroscopicJamming.gaussian_step_slope line 49
  3. lemma OAI.MicroscopicJamming.heat_affine_continuousAt line 92
  4. lemma OAI.MicroscopicJamming.gaussianHeat_time_continuous line 123
  5. lemma OAI.MicroscopicJamming.gaussianRowOperator_time_continuous line 130
  6. lemma OAI.MicroscopicJamming.abs_sub_le_of_hasDerivAt_Ioo line 152
  7. theorem OAI.MicroscopicJamming.gaussian_step_time line 161
  8. lemma OAI.MicroscopicJamming.gaussianStepPath_time_bound line 254
  9. theorem OAI.MicroscopicJamming.gaussian_step_path line 306
  10. lemma OAI.MicroscopicJamming.gaussianStepPath_cylinder_lipschitz line 338
  11. lemma OAI.MicroscopicJamming.gaussianStepPath_cylinder_bound line 389
  12. lemma OAI.MicroscopicJamming.gaussianStepPath_jointly_continuous line 417
  13. lemma OAI.MicroscopicJamming.gaussianStepPath_global_value_bound line 440
  14. def OAI.MicroscopicJamming.GaussianStepPDEStatement line 460
  15. lemma OAI.MicroscopicJamming.gaussian_composition_twice line 479
  16. lemma OAI.MicroscopicJamming.gaussianStepTime_append line 504
  17. lemma OAI.MicroscopicJamming.gaussianStepPath_prefix line 508
  18. theorem OAI.MicroscopicJamming.gaussian_step_pde line 524
  19. def OAI.MicroscopicJamming.gaussianStepCoefficient line 560
  20. def OAI.MicroscopicJamming.RowClassicalVarianceSolution line 566
  21. def OAI.MicroscopicJamming.RowVarianceExistenceStatement line 579