OAI/Probability/JammingConcavity/RPCSamplePattern.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

R P C Sample Pattern.

  1. def OAI.MicroscopicJamming.PatternIndex line 39
  2. instance OAI.MicroscopicJamming.patternIndexFintype line 43
  3. def OAI.MicroscopicJamming.RPCSamplePattern line 52
  4. def OAI.MicroscopicJamming.sampledPatternProbability line 58
  5. def OAI.MicroscopicJamming.RPCSamplePatternStatement line 63
  6. def OAI.MicroscopicJamming.singletonReplicaPattern line 82
  7. inductive OAI.MicroscopicJamming.RPCInsertion line 88
  8. def OAI.MicroscopicJamming.RPCPredictiveStatement line 99
  9. lemma OAI.MicroscopicJamming.partitionProduct_add_new line 120
  10. lemma OAI.MicroscopicJamming.partitionProduct_add_old line 138
  11. lemma OAI.MicroscopicJamming.singletonReplicaPattern_size line 159
  12. lemma OAI.MicroscopicJamming.singletonReplicaPattern_valid line 164
  13. lemma OAI.MicroscopicJamming.singletonReplicaPattern_product line 175
  14. lemma OAI.MicroscopicJamming.pi_grouping line 192
  15. lemma OAI.MicroscopicJamming.pi_fixed_root line 210
  16. lemma OAI.MicroscopicJamming.pi_distinct_roots line 255
  17. def OAI.MicroscopicJamming.GoodCloudLabels line 299
  18. lemma OAI.MicroscopicJamming.goodCloudLabels_cons line 303
  19. lemma OAI.MicroscopicJamming.labelCloudIntegral_tuple line 319
  20. lemma OAI.MicroscopicJamming.labelCloudIntegral_injective line 356
  21. lemma OAI.MicroscopicJamming.patternIndex_card line 389
  22. lemma OAI.MicroscopicJamming.patternIndex_nonempty line 402
  23. lemma OAI.MicroscopicJamming.labelCloudIntegral_map line 408
  24. lemma OAI.MicroscopicJamming.cascadeLeafLaw_child_density line 424
  25. lemma OAI.MicroscopicJamming.ofReal_toReal_neg_nat line 458
  26. lemma OAI.MicroscopicJamming.sampledPatternProbability_cons line 464
  27. lemma OAI.MicroscopicJamming.sampledPatternProbability_eq_ae line 518
  28. theorem OAI.MicroscopicJamming.rpcSamplePattern line 537
  29. lemma OAI.MicroscopicJamming.rpcInsertion_properties line 555
  30. theorem OAI.MicroscopicJamming.rpcPredictive line 650