OAI/Probability/JammingConcavity/RPCPatternInsertionEvents.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

R P C Pattern Insertion Events.

  1. lemma OAI.MicroscopicJamming.rpcSamplePattern_insert_left_iff line 39
  2. lemma OAI.MicroscopicJamming.rpcSamplePattern_insert_right_iff line 78
  3. lemma OAI.MicroscopicJamming.rpcSamplePattern_unique_insertion line 120
  4. def OAI.MicroscopicJamming.freshPatternSite line 169
  5. def OAI.MicroscopicJamming.childPatternSite line 173
  6. lemma OAI.MicroscopicJamming.patternSite_fresh_or_child line 178
  7. lemma OAI.MicroscopicJamming.patternSiteFold_fresh line 189
  8. lemma OAI.MicroscopicJamming.patternSiteFold_child line 196
  9. lemma OAI.MicroscopicJamming.rpcSamplePattern_insert_fresh_iff line 207
  10. lemma OAI.MicroscopicJamming.rpcSamplePattern_insert_child_iff line 239
  11. lemma OAI.MicroscopicJamming.rankCluster_card_of_embedding line 285
  12. lemma OAI.MicroscopicJamming.rankPattern_children line 297
  13. def OAI.MicroscopicJamming.rankPatternInsertEvent line 356
  14. lemma OAI.MicroscopicJamming.rankPatternInsertEvent_real line 364
  15. structure OAI.MicroscopicJamming.PatternLabelling line 439
  16. def OAI.MicroscopicJamming.PatternLabelling.singleton line 443
  17. def OAI.MicroscopicJamming.PatternLabelling.extend line 446
  18. inductive OAI.MicroscopicJamming.ReachablePatternLabelling line 451
  19. lemma OAI.MicroscopicJamming.ReachablePatternLabelling.valid line 456
  20. lemma OAI.MicroscopicJamming.PatternLabelling.size line 462
  21. lemma OAI.MicroscopicJamming.PatternLabelling.extend_old line 466
  22. lemma OAI.MicroscopicJamming.PatternLabelling.extend_new line 472
  23. lemma OAI.MicroscopicJamming.PatternLabelling.extend_sample line 478
  24. lemma OAI.MicroscopicJamming.reachablePatternLabelling_covers line 491
  25. def OAI.MicroscopicJamming.PatternLabelling.signature line 502
  26. lemma OAI.MicroscopicJamming.PatternLabelling.sample_iff_signature line 505
  27. lemma OAI.MicroscopicJamming.rpcSamplePattern_delete line 524
  28. lemma OAI.MicroscopicJamming.PatternLabelling.delete_sample line 578
  29. def OAI.MicroscopicJamming.rankMesh line 594
  30. def OAI.MicroscopicJamming.rankMeshValue line 596
  31. lemma OAI.MicroscopicJamming.rankMesh_increasing line 598
  32. lemma OAI.MicroscopicJamming.rankMesh_valid line 605
  33. lemma OAI.MicroscopicJamming.range_filter_lt_length line 614
  34. lemma OAI.MicroscopicJamming.rankMesh_count line 625
  35. lemma OAI.MicroscopicJamming.rankMeshValue_bounds line 640
  36. lemma OAI.MicroscopicJamming.rankMeshValue_tendsto line 658