OAI/Probability/JammingConcavity/RowParameterData.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Row Parameter Data.

  1. structure OAI.MicroscopicJamming.Parameter.RankFamilyData line 32
  2. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.poly line 45
  3. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.diffusion_cont line 56
  4. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.endpoint_linear line 60
  5. lemma OAI.MicroscopicJamming.Parameter.actual_parameter_family line 123
  6. lemma OAI.MicroscopicJamming.Parameter.dd1_add line 196
  7. lemma OAI.MicroscopicJamming.Parameter.dd2_add line 197
  8. lemma OAI.MicroscopicJamming.Parameter.dd3_add line 198
  9. lemma OAI.MicroscopicJamming.Parameter.dd1_mul line 199
  10. lemma OAI.MicroscopicJamming.Parameter.dd2_mul line 200
  11. lemma OAI.MicroscopicJamming.Parameter.dd3_mul line 201
  12. lemma OAI.MicroscopicJamming.Parameter.dd1_rhs line 203
  13. lemma OAI.MicroscopicJamming.Parameter.dd2_rhs line 211
  14. lemma OAI.MicroscopicJamming.Parameter.dd3_rhs line 221
  15. lemma OAI.MicroscopicJamming.Parameter.field1_time line 243
  16. lemma OAI.MicroscopicJamming.Parameter.field2_time line 248
  17. lemma OAI.MicroscopicJamming.Parameter.field3_time line 253
  18. def OAI.MicroscopicJamming.Parameter.source1 line 258
  19. def OAI.MicroscopicJamming.Parameter.source2 line 261
  20. def OAI.MicroscopicJamming.Parameter.source3 line 266
  21. lemma OAI.MicroscopicJamming.Parameter.field1_equation line 273
  22. lemma OAI.MicroscopicJamming.Parameter.field2_equation line 283
  23. lemma OAI.MicroscopicJamming.Parameter.field3_equation line 300
  24. lemma OAI.MicroscopicJamming.Parameter.family_mul_time line 330
  25. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.mul_B line 336
  26. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.mul_at line 343
  27. lemma OAI.MicroscopicJamming.Parameter.source1_poly line 354
  28. lemma OAI.MicroscopicJamming.Parameter.field1_poly line 363
  29. lemma OAI.MicroscopicJamming.Parameter.source2_poly line 375
  30. lemma OAI.MicroscopicJamming.Parameter.field2_poly line 388
  31. lemma OAI.MicroscopicJamming.Parameter.source3_poly line 400
  32. lemma OAI.MicroscopicJamming.Parameter.field3_poly line 418
  33. lemma OAI.MicroscopicJamming.Parameter.differentiable_of_dd2_bound line 440
  34. lemma OAI.MicroscopicJamming.Parameter.tendsto_dd2_left line 466
  35. lemma OAI.MicroscopicJamming.Parameter.second_remainder_lipschitz line 480
  36. lemma OAI.MicroscopicJamming.Parameter.twice_differentiable_of_dd_bounds line 517
  37. lemma OAI.MicroscopicJamming.RankFamilyData.parameter_C2 line 594
  38. theorem OAI.MicroscopicJamming.row_parameter line 619