OAI/Probability/JammingConcavity/RowSmoothApproxFinite.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Row Smooth Approx Finite.

  1. def OAI.MicroscopicJamming.rowTransitionStep line 68
  2. lemma OAI.MicroscopicJamming.rowTransitionStep_smooth line 70
  3. lemma OAI.MicroscopicJamming.rowTransitionStep_mono line 75
  4. lemma OAI.MicroscopicJamming.rowTransitionStep_endpoints line 81
  5. lemma OAI.MicroscopicJamming.rowTransitionStep_limit line 91
  6. def OAI.MicroscopicJamming.rowFiniteSmoothBase line 122
  7. def OAI.MicroscopicJamming.rowFiniteSmooth line 126
  8. lemma OAI.MicroscopicJamming.rowFiniteSmoothBase_smooth line 129
  9. lemma OAI.MicroscopicJamming.rowFiniteSmoothBase_mono line 136
  10. lemma OAI.MicroscopicJamming.rowFiniteSmooth_profile line 146
  11. lemma OAI.MicroscopicJamming.rowDelta_tendsto line 174
  12. lemma OAI.MicroscopicJamming.rowTransitionTail_limit line 177
  13. lemma OAI.MicroscopicJamming.rowFiniteSmooth_limit line 188
  14. lemma OAI.MicroscopicJamming.rowFiniteSmooth_L1 line 201
  15. def OAI.MicroscopicJamming.rowSmoothProfile line 249
  16. lemma OAI.MicroscopicJamming.RowFiniteProfile.smoothApprox line 253
  17. lemma OAI.MicroscopicJamming.rowSmooth_density line 281
  18. lemma OAI.MicroscopicJamming.rowSmooth_approximation line 290
  19. lemma OAI.MicroscopicJamming.rowChord_bound line 306
  20. lemma OAI.MicroscopicJamming.rowChord_smooth line 312
  21. lemma OAI.MicroscopicJamming.rowChord_distance line 318
  22. lemma OAI.MicroscopicJamming.rowProfileValue_tendsto line 325
  23. lemma OAI.MicroscopicJamming.rowProfileValue_smooth_concave line 335
  24. lemma OAI.MicroscopicJamming.rowProfileValue_concave line 346
  25. lemma OAI.MicroscopicJamming.gaussianRankProfile_nonneg line 375
  26. lemma OAI.MicroscopicJamming.gaussianRankProfile_zero_below line 382
  27. lemma OAI.MicroscopicJamming.profileRankLaw_Iio line 389
  28. lemma OAI.MicroscopicJamming.gaussianRankProfile_CDF line 397
  29. lemma OAI.MicroscopicJamming.RowPartition.CDF line 442
  30. lemma OAI.MicroscopicJamming.RowPartition.CDF_ae line 445
  31. lemma OAI.MicroscopicJamming.rowProfileValue_partition line 457
  32. theorem OAI.MicroscopicJamming.rowProfileAnalytic line 495
  33. def OAI.MicroscopicJamming.rowQuadraticHinge line 517
  34. def OAI.MicroscopicJamming.RowNonsmoothConcavityStatement line 520
  35. def OAI.MicroscopicJamming.RowConcavityMainStatement line 542
  36. lemma OAI.MicroscopicJamming.row_uniform_grid_passage line 557
  37. def OAI.MicroscopicJamming.RowProfileConclusions line 589
  38. lemma OAI.MicroscopicJamming.row_terminal_profile_passage line 596
  39. lemma OAI.MicroscopicJamming.row_composition_total_zero line 621
  40. lemma OAI.MicroscopicJamming.rowProfile_zero line 636
  41. lemma OAI.MicroscopicJamming.row_weighted_terminal_bound line 660