OAI/Probability/JammingConcavity/RowProfileAnalytic.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Row Profile Analytic.

  1. def OAI.MicroscopicJamming.profileRankLaw line 65
  2. def OAI.MicroscopicJamming.profileCDF line 66
  3. structure OAI.MicroscopicJamming.RowPartition line 68
  4. def OAI.MicroscopicJamming.RowPartition.profile line 74
  5. def OAI.MicroscopicJamming.rowProfileSequence line 97
  6. def OAI.MicroscopicJamming.rowProfileValue line 100
  7. def OAI.MicroscopicJamming.SphericalProfile.rowChord line 103
  8. def OAI.MicroscopicJamming.RowProfileAnalyticStatement line 113
  9. instance OAI.MicroscopicJamming.(instance at line 137) line 137
  10. lemma OAI.MicroscopicJamming.profileCDF_monotone line 141
  11. lemma OAI.MicroscopicJamming.profileCDF_bounds line 145
  12. lemma OAI.MicroscopicJamming.profileCDF_closed line 150
  13. lemma OAI.MicroscopicJamming.profileCDF_integral line 159
  14. lemma OAI.MicroscopicJamming.profileCDF_ae_continuous line 166
  15. lemma OAI.MicroscopicJamming.rowAnalytic_bounded line 171
  16. lemma OAI.MicroscopicJamming.row_integrated_difference_le line 187
  17. lemma OAI.MicroscopicJamming.gaussianStepRightCoefficient_measurable line 263
  18. lemma OAI.MicroscopicJamming.gaussianStepRightCoefficient_local line 271
  19. lemma OAI.MicroscopicJamming.gaussianStepRightCoefficient_rightContinuous line 289
  20. lemma OAI.MicroscopicJamming.rowStepDifference_integrable line 297
  21. lemma OAI.MicroscopicJamming.rowStepDifference_primitive line 309
  22. lemma OAI.MicroscopicJamming.row_step_L1_stability line 339
  23. lemma OAI.MicroscopicJamming.row_composition_L1_stability line 405
  24. lemma OAI.MicroscopicJamming.gaussianStepCoefficient_ae_right line 422
  25. def OAI.MicroscopicJamming.rowCDFGrid line 435
  26. lemma OAI.MicroscopicJamming.rowCDFGrid_valid line 437
  27. lemma OAI.MicroscopicJamming.rowCDFGrid_time line 441
  28. lemma OAI.MicroscopicJamming.rowCDFGrid_tendsto line 444
  29. lemma OAI.MicroscopicJamming.rowCDFGrid_L1 line 461
  30. lemma OAI.MicroscopicJamming.row_indicator_distance_integral line 491
  31. lemma OAI.MicroscopicJamming.profileCDF_distance line 522
  32. def OAI.MicroscopicJamming.rowCoeffDistance line 566
  33. lemma OAI.MicroscopicJamming.rowCoeff_integrable line 567
  34. lemma OAI.MicroscopicJamming.rowCoeffDistance_triangle line 575
  35. lemma OAI.MicroscopicJamming.rowCoeffDistance_comm line 584
  36. lemma OAI.MicroscopicJamming.rowCoeffDistance_nonneg line 586
  37. lemma OAI.MicroscopicJamming.row_cauchy_error line 588
  38. lemma OAI.MicroscopicJamming.rowProfileSequence_converges line 596
  39. lemma OAI.MicroscopicJamming.rowProfileValue_lipschitz line 620
  40. lemma OAI.MicroscopicJamming.profileCDF_smooth_inverse line 656
  41. lemma OAI.MicroscopicJamming.rowCDFGrid_uniform line 675
  42. lemma OAI.MicroscopicJamming.rowProfileValue_smooth line 697