OAI/Probability/JammingConcavity/RowDerivativeApprox.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Row Derivative Approx.

  1. lemma OAI.MicroscopicJamming.Parameter.second_remainder_representation line 32
  2. lemma OAI.MicroscopicJamming.Parameter.first_derivative_error line 103
  3. lemma OAI.MicroscopicJamming.Parameter.second_derivative_error line 125
  4. lemma OAI.MicroscopicJamming.cylinder_of_poly_error line 158
  5. lemma OAI.MicroscopicJamming.smooth_limit_of_all_jet_convergence line 176
  6. lemma OAI.MicroscopicJamming.growth_limit line 204
  7. def OAI.MicroscopicJamming.Parameter.pjet line 220
  8. def OAI.MicroscopicJamming.Parameter.pjet2 line 223
  9. def OAI.MicroscopicJamming.Parameter.paramSeq line 226
  10. lemma OAI.MicroscopicJamming.Parameter.paramSeq_pos line 228
  11. lemma OAI.MicroscopicJamming.Parameter.paramSeq_bound line 229
  12. lemma OAI.MicroscopicJamming.Parameter.paramSeq_tendsto line 233
  13. lemma OAI.MicroscopicJamming.Parameter.paramSeq_mem line 236
  14. lemma OAI.MicroscopicJamming.Parameter.twice_paramSeq_mem line 238
  15. def OAI.MicroscopicJamming.Parameter.seqNodes2 line 241
  16. def OAI.MicroscopicJamming.Parameter.seqNodes3 line 243
  17. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.bound_dd2 line 246
  18. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.bound_dd3 line 260
  19. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.first_jet_limit line 274
  20. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.second_jet_limit line 289
  21. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.parameter_jets line 306
  22. def OAI.MicroscopicJamming.Parameter.endpointRhs line 324
  23. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.endpoint_rhs_poly line 329
  24. def OAI.MicroscopicJamming.Parameter.rhs1 line 346
  25. def OAI.MicroscopicJamming.Parameter.rhs2 line 349
  26. lemma OAI.MicroscopicJamming.Parameter.rhs1_poly line 353
  27. lemma OAI.MicroscopicJamming.Parameter.rhs2_poly line 356
  28. lemma OAI.MicroscopicJamming.time_derivative_limit_dominated line 368
  29. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.base_jet_limit line 419
  30. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.offaxis_jet_limit line 425
  31. def OAI.MicroscopicJamming.Parameter.linearRhs line 446
  32. def OAI.MicroscopicJamming.Parameter.quadraticRhs line 450
  33. lemma OAI.MicroscopicJamming.Parameter.linearRhs_smooth line 455
  34. lemma OAI.MicroscopicJamming.Parameter.quadraticRhs_smooth line 467
  35. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.rhs1_limit line 481
  36. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.rhs2_limit line 495
  37. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.parameter_equations line 513
  38. structure OAI.MicroscopicJamming.Hessian.Jet line 557
  39. lemma OAI.MicroscopicJamming.Hessian.Jet.spatial_deriv line 561
  40. lemma OAI.MicroscopicJamming.Hessian.Jet.spatial_deriv2 line 563
  41. lemma OAI.MicroscopicJamming.Hessian.Jet.add line 565
  42. lemma OAI.MicroscopicJamming.Hessian.Jet.neg line 571
  43. lemma OAI.MicroscopicJamming.Hessian.Jet.mul line 574
  44. lemma OAI.MicroscopicJamming.Hessian.Jet.const line 582
  45. lemma OAI.MicroscopicJamming.Hessian.Jet.rank line 585
  46. lemma OAI.MicroscopicJamming.Hessian.Jet.coeff line 588
  47. lemma OAI.MicroscopicJamming.Hessian.Jet.inv line 591
  48. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.parameter_growth line 609
  49. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.parameter_terminal line 624
  50. lemma OAI.MicroscopicJamming.Parameter.RankFamilyData.parameter_time_jets line 641
  51. lemma OAI.MicroscopicJamming.Hessian.smooth_jet line 665
  52. def OAI.MicroscopicJamming.Hessian.ftime line 671
  53. def OAI.MicroscopicJamming.Hessian.vtime line 673
  54. def OAI.MicroscopicJamming.Hessian.gtime line 676
  55. lemma OAI.MicroscopicJamming.Hessian.iterated_rhs line 679
  56. lemma OAI.MicroscopicJamming.Hessian.iterated_linearRhs line 692