OAI/Probability/JammingConcavity/RowIntegralJets.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Row Integral Jets.

  1. lemma OAI.MicroscopicJamming.integral_hasDerivAt_of_jointly_continuous line 30
  2. lemma OAI.MicroscopicJamming.iteratedDeriv_integral_of_jets line 51
  3. lemma OAI.MicroscopicJamming.evolution_all_jets line 72
  4. lemma OAI.MicroscopicJamming.Higher.sum_linear_jet_decompose line 132
  5. lemma OAI.MicroscopicJamming.Higher.family_linear_bound line 149
  6. lemma OAI.MicroscopicJamming.Higher.linear_all_jets_growth line 183
  7. lemma OAI.MicroscopicJamming.Higher.JointSpatialSmooth.sub line 254
  8. lemma OAI.MicroscopicJamming.Higher.linear_evolution_jets line 259
  9. structure OAI.MicroscopicJamming.Higher.PolynomialJetFamily line 295
  10. lemma OAI.MicroscopicJamming.Higher.PolynomialJetFamily.jet line 300
  11. lemma OAI.MicroscopicJamming.Higher.PolynomialJetFamily.comp line 306
  12. lemma OAI.MicroscopicJamming.Higher.PolynomialJetFamily.add line 311
  13. lemma OAI.MicroscopicJamming.Higher.PolynomialJetFamily.coeff_mul line 320
  14. lemma OAI.MicroscopicJamming.Higher.PolynomialJetFamily.const_mul line 330
  15. lemma OAI.MicroscopicJamming.Higher.PolynomialJetFamily.sub line 335
  16. lemma OAI.MicroscopicJamming.Higher.PolynomialJetFamily.mul line 340
  17. def OAI.MicroscopicJamming.Parameter.dd1 line 364
  18. def OAI.MicroscopicJamming.Parameter.dd2 line 365
  19. def OAI.MicroscopicJamming.Parameter.dd3 line 366
  20. lemma OAI.MicroscopicJamming.Parameter.dd1_sub_slope line 368
  21. lemma OAI.MicroscopicJamming.Parameter.dd2_sub_last line 375
  22. lemma OAI.MicroscopicJamming.Parameter.dd1_square line 383
  23. lemma OAI.MicroscopicJamming.Parameter.dd2_square line 386
  24. lemma OAI.MicroscopicJamming.Parameter.dd3_square line 393
  25. lemma OAI.MicroscopicJamming.Parameter.dd1_affine_mul line 402
  26. lemma OAI.MicroscopicJamming.Parameter.dd2_affine_mul line 408
  27. lemma OAI.MicroscopicJamming.Parameter.dd3_affine_mul line 415
  28. structure OAI.MicroscopicJamming.Parameter.Nodes2 line 434
  29. structure OAI.MicroscopicJamming.Parameter.Nodes3 line 441
  30. structure OAI.MicroscopicJamming.Parameter.Nodes4 line 447
  31. def OAI.MicroscopicJamming.Parameter.Nodes3.bc line 454
  32. def OAI.MicroscopicJamming.Parameter.Nodes4.bcd line 455
  33. def OAI.MicroscopicJamming.Parameter.Nodes4.cd line 456
  34. def OAI.MicroscopicJamming.Parameter.field1 line 458
  35. def OAI.MicroscopicJamming.Parameter.field2 line 459
  36. def OAI.MicroscopicJamming.Parameter.field3 line 460
  37. lemma OAI.MicroscopicJamming.Parameter.divided_smooth line 462
  38. lemma OAI.MicroscopicJamming.Parameter.divided_jet line 467
  39. lemma OAI.MicroscopicJamming.Parameter.field1_smooth line 476
  40. lemma OAI.MicroscopicJamming.Parameter.field2_smooth line 480
  41. lemma OAI.MicroscopicJamming.Parameter.field3_smooth line 484
  42. lemma OAI.MicroscopicJamming.Parameter.field1_jet line 488
  43. lemma OAI.MicroscopicJamming.Parameter.field2_jet line 493
  44. lemma OAI.MicroscopicJamming.Parameter.field3_jet line 505
  45. lemma OAI.MicroscopicJamming.Parameter.fixed_family line 517
  46. lemma OAI.MicroscopicJamming.Parameter.field1_individual line 522
  47. lemma OAI.MicroscopicJamming.Parameter.field2_individual line 529
  48. lemma OAI.MicroscopicJamming.Parameter.field3_individual line 536
  49. lemma OAI.MicroscopicJamming.rowSmooth_perturbation line 551
  50. lemma OAI.MicroscopicJamming.row_rank_neighborhood_existence line 580
  51. lemma OAI.MicroscopicJamming.row_variance_jet_uniform line 603
  52. lemma OAI.MicroscopicJamming.row_rank_smooth line 637
  53. lemma OAI.MicroscopicJamming.row_rank_jets_time line 654
  54. lemma OAI.MicroscopicJamming.row_rank_uniform_bounds line 669