OAI/Probability/JammingConcavity/RowCalcJet.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Row Calc Jet.

  1. structure OAI.MicroscopicJamming.Hessian.CalcJet line 31
  2. def OAI.MicroscopicJamming.Hessian.CalcJet.add line 38
  3. def OAI.MicroscopicJamming.Hessian.CalcJet.neg line 41
  4. def OAI.MicroscopicJamming.Hessian.CalcJet.mul line 43
  5. def OAI.MicroscopicJamming.Hessian.CalcJet.const line 47
  6. def OAI.MicroscopicJamming.Hessian.CalcJet.smul line 48
  7. def OAI.MicroscopicJamming.Hessian.CalcJet.sq line 49
  8. def OAI.MicroscopicJamming.Hessian.CalcJet.rank line 50
  9. def OAI.MicroscopicJamming.Hessian.CalcJet.coeff line 51
  10. def OAI.MicroscopicJamming.Hessian.CalcJet.inv line 53
  11. def OAI.MicroscopicJamming.Hessian.CalcJet.gen line 57
  12. lemma OAI.MicroscopicJamming.Hessian.CalcJet.gen_add line 58
  13. lemma OAI.MicroscopicJamming.Hessian.CalcJet.gen_mul line 60
  14. lemma OAI.MicroscopicJamming.Hessian.CalcJet.gen_inv line 63
  15. lemma OAI.MicroscopicJamming.Hessian.jet_of_evolution line 79
  16. structure OAI.MicroscopicJamming.Hessian.EvolutionSystem line 86
  17. lemma OAI.MicroscopicJamming.Hessian.actual_evolution line 98
  18. def OAI.MicroscopicJamming.Hessian.EvolutionSystem.fj line 119
  19. def OAI.MicroscopicJamming.Hessian.EvolutionSystem.vj line 126
  20. def OAI.MicroscopicJamming.Hessian.EvolutionSystem.gj line 133
  21. def OAI.MicroscopicJamming.Hessian.EvolutionSystem.drift line 140
  22. def OAI.MicroscopicJamming.Hessian.EvolutionSystem.ell line 142
  23. def OAI.MicroscopicJamming.Hessian.EvolutionSystem.mu line 144
  24. def OAI.MicroscopicJamming.Hessian.EvolutionSystem.mainJet line 148
  25. lemma OAI.MicroscopicJamming.Hessian.EvolutionSystem.gen_ell line 162
  26. lemma OAI.MicroscopicJamming.Hessian.EvolutionSystem.gen_curvature line 170
  27. lemma OAI.MicroscopicJamming.Hessian.EvolutionSystem.gen_main line 177
  28. def OAI.MicroscopicJamming.Hessian.CalcJet.Controlled line 194
  29. lemma OAI.MicroscopicJamming.Hessian.CalcJet.Controlled.add line 197
  30. lemma OAI.MicroscopicJamming.Hessian.CalcJet.Controlled.mul line 199
  31. lemma OAI.MicroscopicJamming.Hessian.CalcJet.controlled_const line 201
  32. lemma OAI.MicroscopicJamming.Hessian.CalcJet.Controlled.smul line 203
  33. lemma OAI.MicroscopicJamming.Hessian.CalcJet.Controlled.neg line 205
  34. lemma OAI.MicroscopicJamming.Hessian.CalcJet.Controlled.sq line 207
  35. lemma OAI.MicroscopicJamming.Hessian.CalcJet.controlled_coeff line 208
  36. lemma OAI.MicroscopicJamming.Hessian.CalcJet.controlled_rank line 213
  37. lemma OAI.MicroscopicJamming.Hessian.CalcJet.Controlled.inv line 216
  38. lemma OAI.MicroscopicJamming.Hessian.CalcJet.nonpos_of_gen_nonneg line 223
  39. lemma OAI.MicroscopicJamming.Hessian.gen_square_quotient line 245
  40. lemma OAI.MicroscopicJamming.Hessian.EvolutionSystem.gen_corrected line 262
  41. lemma OAI.MicroscopicJamming.Hessian.EvolutionSystem.controlled_fj line 284
  42. lemma OAI.MicroscopicJamming.Hessian.EvolutionSystem.controlled_vj line 286
  43. lemma OAI.MicroscopicJamming.Hessian.EvolutionSystem.controlled_gj line 288
  44. lemma OAI.MicroscopicJamming.Hessian.EvolutionSystem.controlled_ell line 290
  45. lemma OAI.MicroscopicJamming.Hessian.EvolutionSystem.controlled_mu line 297
  46. lemma OAI.MicroscopicJamming.Hessian.EvolutionSystem.controlled_main line 302
  47. lemma OAI.MicroscopicJamming.Hessian.CalcJet.nonpos_of_reaction_nonneg line 317
  48. lemma OAI.MicroscopicJamming.Hessian.strict_negative_curvature line 341
  49. lemma OAI.MicroscopicJamming.Hessian.actual_second_nonpos line 394
  50. def OAI.MicroscopicJamming.canonicalRank line 481
  51. lemma OAI.MicroscopicJamming.canonicalRank_spec line 484
  52. lemma OAI.MicroscopicJamming.canonicalRank_eq line 487
  53. lemma OAI.MicroscopicJamming.rowSmooth_chord line 494
  54. lemma OAI.MicroscopicJamming.twice_derivative_local_shift line 520
  55. lemma OAI.MicroscopicJamming.canonicalRank_chord_second line 546
  56. lemma OAI.MicroscopicJamming.canonicalRank_chord_concave_strict line 577
  57. lemma OAI.MicroscopicJamming.rowTerminal_penalty_jets line 598
  58. lemma OAI.MicroscopicJamming.rowTerminal_penalty line 606
  59. lemma OAI.MicroscopicJamming.rowTerminal_penalty_strict line 637