OAI/Probability/JammingConcavity/ParabolicInterior.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Parabolic Interior.

  1. lemma OAI.MicroscopicJamming.backward_comparison_interior line 31
  2. lemma OAI.MicroscopicJamming.row_classical_variance_le line 79
  3. def OAI.MicroscopicJamming.RowVarianceUniquenessStatement line 134
  4. theorem OAI.MicroscopicJamming.row_variance_uniqueness line 141
  5. theorem OAI.MicroscopicJamming.row_variance_existence line 154
  6. def OAI.MicroscopicJamming.RowSmoothProfile line 184
  7. def OAI.MicroscopicJamming.RowClassicalRankSolution line 188
  8. def OAI.MicroscopicJamming.RowParameterStatement line 201
  9. lemma OAI.MicroscopicJamming.RowSmoothProfile.strictMonoOn line 217
  10. lemma OAI.MicroscopicJamming.RowSmoothProfile.mapsTo line 221
  11. lemma OAI.MicroscopicJamming.RowSmoothProfile.mapsTo_open line 227
  12. lemma OAI.MicroscopicJamming.rowSmooth_inverse line 236
  13. lemma OAI.MicroscopicJamming.rowSmooth_inverse_hasDerivAt line 269
  14. lemma OAI.MicroscopicJamming.rowVariance_to_rank line 285
  15. lemma OAI.MicroscopicJamming.rowSmooth_inverse_mapsTo_open line 308
  16. lemma OAI.MicroscopicJamming.rowRank_to_variance line 328
  17. lemma OAI.MicroscopicJamming.row_rank_existence_unique line 357
  18. lemma OAI.MicroscopicJamming.backward_reaction_source_upper line 381
  19. lemma OAI.MicroscopicJamming.backward_reaction_source_bound line 464
  20. lemma OAI.MicroscopicJamming.forward_reaction_source_bound line 493