OAI/Probability/JammingConcavity/RPCPatternExtension.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

R P C Pattern Extension.

  1. def OAI.MicroscopicJamming.patternConsEquiv line 41
  2. def OAI.MicroscopicJamming.optionSumLeft line 53
  3. def OAI.MicroscopicJamming.optionSumRight line 65
  4. def OAI.MicroscopicJamming.PatternSite line 71
  5. instance OAI.MicroscopicJamming.patternSiteFintype line 75
  6. structure OAI.MicroscopicJamming.PatternExtension line 86
  7. lemma OAI.MicroscopicJamming.patternIndex_singleton_card line 90
  8. def OAI.MicroscopicJamming.patternExtension line 96
  9. lemma OAI.MicroscopicJamming.rpcSamplePattern_nil line 133
  10. lemma OAI.MicroscopicJamming.rpcSamplePattern_cons_iff line 140
  11. lemma OAI.MicroscopicJamming.rpcSamplePattern_congr line 179
  12. lemma OAI.MicroscopicJamming.rpcSamplePattern_singleton line 184
  13. def OAI.MicroscopicJamming.insertedSample line 208
  14. lemma OAI.MicroscopicJamming.insertedSample_old line 212
  15. lemma OAI.MicroscopicJamming.insertedSample_new line 216
  16. def OAI.MicroscopicJamming.patternCanonicalPath line 230
  17. def OAI.MicroscopicJamming.patternSignature line 234
  18. lemma OAI.MicroscopicJamming.patternCanonicalPath_sample line 237
  19. lemma OAI.MicroscopicJamming.cascadeSharedEdges_le line 248
  20. lemma OAI.MicroscopicJamming.cascadeSharedEdges_self line 257
  21. lemma OAI.MicroscopicJamming.cascadeSharedEdges_pos_iff line 262
  22. lemma OAI.MicroscopicJamming.patternSignature_root_iff line 267
  23. lemma OAI.MicroscopicJamming.rpcSamplePattern_signature line 273
  24. lemma OAI.MicroscopicJamming.rpcSamplePattern_of_signature line 298
  25. lemma OAI.MicroscopicJamming.rpcSamplePattern_iff_signature line 330
  26. def OAI.MicroscopicJamming.rankProfileCode line 346
  27. lemma OAI.MicroscopicJamming.rankProfileCode_eq_iff line 349
  28. lemma OAI.MicroscopicJamming.measurable_rankProfileCode line 354
  29. def OAI.MicroscopicJamming.rankProfilePath line 363
  30. lemma OAI.MicroscopicJamming.measurable_rankProfilePath line 367
  31. lemma OAI.MicroscopicJamming.rankProfileCode_rows line 375
  32. lemma OAI.MicroscopicJamming.rankProfileCode_link line 389
  33. lemma OAI.MicroscopicJamming.rankProfilePath_sharedEdges line 403
  34. lemma OAI.MicroscopicJamming.rankProfilePath_rows line 422
  35. lemma OAI.MicroscopicJamming.rankProfilePath_link line 428
  36. lemma OAI.MicroscopicJamming.insertedSample_left_head line 442
  37. lemma OAI.MicroscopicJamming.insertedSample_left_tail line 452
  38. lemma OAI.MicroscopicJamming.insertedSample_right_head line 458
  39. lemma OAI.MicroscopicJamming.insertedSample_right_tail line 464
  40. lemma OAI.MicroscopicJamming.insertedSample_comp line 475
  41. lemma OAI.MicroscopicJamming.insertedSample_forall line 482
  42. def OAI.MicroscopicJamming.patternSiteFold line 502
  43. def OAI.MicroscopicJamming.patternSiteWeight line 508
  44. lemma OAI.MicroscopicJamming.patternExtension_cases line 516
  45. lemma OAI.MicroscopicJamming.patternExtension_insertion line 534
  46. lemma OAI.MicroscopicJamming.patternExtension_valid line 550
  47. lemma OAI.MicroscopicJamming.patternExtension_valid_generic line 565
  48. lemma OAI.MicroscopicJamming.patternExtension_blocks_valid line 598