OAI/Probability/JammingConcavity/RowWeightedStep.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Row Weighted Step.

  1. lemma OAI.MicroscopicJamming.row_step_weighted_terminal line 67
  2. lemma OAI.MicroscopicJamming.row_composition_weighted_Lipschitz line 103
  3. abbrev OAI.MicroscopicJamming.rowConv line 126
  4. lemma OAI.MicroscopicJamming.rowConv_integrable line 127
  5. lemma OAI.MicroscopicJamming.row_iterated_smooth line 130
  6. lemma OAI.MicroscopicJamming.row_iterated_compact line 135
  7. lemma OAI.MicroscopicJamming.rowConv_deriv line 140
  8. lemma OAI.MicroscopicJamming.rowConv_iterated line 144
  9. lemma OAI.MicroscopicJamming.row_integral_deriv_zero line 150
  10. lemma OAI.MicroscopicJamming.row_integral_iterated_zero line 157
  11. lemma OAI.MicroscopicJamming.rowConv_iterated_bound line 162
  12. lemma OAI.MicroscopicJamming.rowReal_Lipschitz line 198
  13. lemma OAI.MicroscopicJamming.rowConv_lipschitz line 204
  14. lemma OAI.MicroscopicJamming.rowConv_concave line 221
  15. lemma OAI.MicroscopicJamming.rowConv_upper line 240
  16. lemma OAI.MicroscopicJamming.rowConv_approx line 248
  17. lemma OAI.MicroscopicJamming.row_smooth_bounded_analytic line 278
  18. lemma OAI.MicroscopicJamming.rowCap_lipschitz line 301
  19. lemma OAI.MicroscopicJamming.rowCap_error line 308
  20. lemma OAI.MicroscopicJamming.row_lipschitz_analytic_approx_one line 324
  21. lemma OAI.MicroscopicJamming.rowBounded_lip line 368
  22. lemma OAI.MicroscopicJamming.row_pointwise_lip line 373
  23. lemma OAI.MicroscopicJamming.row_linear_limit_bound line 379
  24. lemma OAI.MicroscopicJamming.row_linear_operator_limit line 390
  25. lemma OAI.MicroscopicJamming.row_composition_terminal_limit line 426
  26. lemma OAI.MicroscopicJamming.row_lipschitz_profile_conclusions line 450
  27. def OAI.MicroscopicJamming.rowCapSlope line 492
  28. def OAI.MicroscopicJamming.rowHingeCap line 493
  29. lemma OAI.MicroscopicJamming.rowCapSlope_bounds line 494
  30. lemma OAI.MicroscopicJamming.rowHingeCap_opt line 497
  31. lemma OAI.MicroscopicJamming.rowHingeCap_concave line 510
  32. lemma OAI.MicroscopicJamming.rowHingeCap_sub_le line 525
  33. lemma OAI.MicroscopicJamming.rowHingeCap_lip line 534
  34. lemma OAI.MicroscopicJamming.rowHingeCap_upper line 541
  35. lemma OAI.MicroscopicJamming.rowHingeCap_lower line 544
  36. lemma OAI.MicroscopicJamming.rowHinge_quadratic line 551
  37. lemma OAI.MicroscopicJamming.rowHingeCap_eq line 558
  38. lemma OAI.MicroscopicJamming.rowHingeCap_error line 565
  39. lemma OAI.MicroscopicJamming.rowConv_quadratic_lower line 590
  40. lemma OAI.MicroscopicJamming.row_hinge_analytic_approx_one line 605
  41. lemma OAI.MicroscopicJamming.row_concave_quadratic_slope line 651
  42. lemma OAI.MicroscopicJamming.row_step_concave_slope line 683