OAI/Probability/JammingConcavity/GaussianTwiceTerminal.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Twice Terminal.

  1. structure OAI.MicroscopicJamming.Twice.RowTwiceTerminal line 29
  2. lemma OAI.MicroscopicJamming.Twice.row_terminal_deriv_linear line 43
  3. lemma OAI.MicroscopicJamming.Twice.row_terminal_quadratic_growth line 64
  4. lemma OAI.MicroscopicJamming.Twice.row_terminal_deriv_growth line 77
  5. lemma OAI.MicroscopicJamming.Twice.row_terminal_second_growth line 83
  6. lemma OAI.MicroscopicJamming.Twice.row_exp_derivatives line 93
  7. lemma OAI.MicroscopicJamming.Twice.row_exp_measurable line 107
  8. lemma OAI.MicroscopicJamming.Twice.row_exp_growth line 119
  9. lemma OAI.MicroscopicJamming.Twice.gaussianRowOperator_calculus line 171
  10. structure OAI.MicroscopicJamming.Twice.GaussianRowMoments line 205
  11. lemma OAI.MicroscopicJamming.Twice.gaussianRowMoments line 214
  12. lemma OAI.MicroscopicJamming.Twice.row_gaussian_stein line 258
  13. lemma OAI.MicroscopicJamming.Twice.gaussianRowOperator_second_exp line 306
  14. lemma OAI.MicroscopicJamming.Twice.gaussianRowOperator_second_moments line 332
  15. lemma OAI.MicroscopicJamming.Twice.row_slope_antitone line 364
  16. lemma OAI.MicroscopicJamming.Twice.gaussianRowOperator_second_zero line 378
  17. lemma OAI.MicroscopicJamming.Twice.gaussianRowOperator_curvature line 390
  18. lemma OAI.MicroscopicJamming.gaussianHeat_eq_variance_integral line 445
  19. lemma OAI.MicroscopicJamming.gaussianRowOperator_barrier line 456
  20. lemma OAI.MicroscopicJamming.gaussianStepTime_nonneg line 483
  21. lemma OAI.MicroscopicJamming.gaussian_curvature_update line 491
  22. theorem OAI.MicroscopicJamming.gaussian_step_bounds line 509
  23. lemma OAI.MicroscopicJamming.gaussianStepRemainder_valid line 566
  24. lemma OAI.MicroscopicJamming.gaussianStepRemainder_zero line 598
  25. lemma OAI.MicroscopicJamming.gaussianRowComposition_zero_time line 604
  26. lemma OAI.MicroscopicJamming.gaussianStepPath_zero line 622
  27. lemma OAI.MicroscopicJamming.gaussianStepPath_terminal line 628
  28. lemma OAI.MicroscopicJamming.gaussianStepPath_cons_le line 636
  29. lemma OAI.MicroscopicJamming.gaussianStepPath_cons_gt line 642
  30. def OAI.MicroscopicJamming.GaussianStepTimeStatement line 654
  31. def OAI.MicroscopicJamming.GaussianStepSlopeStatement line 670