OAI/Probability/JammingConcavity/RPCRankUniqueness.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

R P C Rank Uniqueness.

  1. lemma OAI.MicroscopicJamming.measurable_rpcStepLevel line 39
  2. lemma OAI.MicroscopicJamming.measurable_rankCovarianceArray line 50
  3. def OAI.MicroscopicJamming.rankMeshArray line 62
  4. lemma OAI.MicroscopicJamming.measurable_rankMeshArray line 65
  5. lemma OAI.MicroscopicJamming.rankMeshArray_tendsto line 68
  6. lemma OAI.MicroscopicJamming.hasRPC_rankMesh_law line 81
  7. theorem OAI.MicroscopicJamming.rpcRankLaw_unique line 97
  8. def OAI.MicroscopicJamming.rankLabelEvent line 131
  9. lemma OAI.MicroscopicJamming.measurableSet_rankLabelEvent line 134
  10. lemma OAI.MicroscopicJamming.rankLabelEvent_iff_sample line 143
  11. lemma OAI.MicroscopicJamming.cascadeSharedEdges_symm line 153
  12. def OAI.MicroscopicJamming.rankMixedSample line 163
  13. lemma OAI.MicroscopicJamming.rankMixedSample_signature line 167
  14. lemma OAI.MicroscopicJamming.rankLabelEvent_insert_iff line 182
  15. lemma OAI.MicroscopicJamming.rankLabelEvent_insert_parent line 200
  16. lemma OAI.MicroscopicJamming.rankLabelEvent_kernel line 210
  17. lemma OAI.MicroscopicJamming.rankGrowing_congr line 250
  18. def OAI.MicroscopicJamming.rankPastEmbed line 257
  19. lemma OAI.MicroscopicJamming.continuous_rankPastEmbed line 260
  20. lemma OAI.MicroscopicJamming.rankGrowing_past line 269
  21. lemma OAI.MicroscopicJamming.rankGrowing_indep_innovation line 275
  22. lemma OAI.MicroscopicJamming.rankGrowing_joint_law line 288
  23. lemma OAI.MicroscopicJamming.rankGrowing_succ_law line 296
  24. lemma OAI.MicroscopicJamming.measurableSet_finiteRank line 312
  25. lemma OAI.MicroscopicJamming.rankGrowing_law_finiteRank line 325
  26. lemma OAI.MicroscopicJamming.rankGrowing_pattern line 330
  27. def OAI.MicroscopicJamming.rankReindex line 378
  28. lemma OAI.MicroscopicJamming.measurable_rankReindex line 379
  29. lemma OAI.MicroscopicJamming.infinitePi_exchangeable line 383
  30. lemma OAI.MicroscopicJamming.cascadeReplicaLaw_exchangeable line 392
  31. lemma OAI.MicroscopicJamming.measurable_cascadeCovarianceArray line 404
  32. lemma OAI.MicroscopicJamming.rankReindex_cascadeCovariance line 417
  33. lemma OAI.MicroscopicJamming.cascadeCovarianceLaw_exchangeable line 423
  34. lemma OAI.MicroscopicJamming.hasRPCFiniteRankLaws_reindex line 431
  35. def OAI.MicroscopicJamming.cascadeFiniteEdges line 450
  36. lemma OAI.MicroscopicJamming.measurable_cascadeFiniteEdges line 454
  37. lemma OAI.MicroscopicJamming.cascadeReplicaLaw_pattern line 464
  38. def OAI.MicroscopicJamming.rankFiniteSteps line 501
  39. lemma OAI.MicroscopicJamming.measurable_rankFiniteSteps line 504
  40. lemma OAI.MicroscopicJamming.rankFiniteSteps_preimage line 511
  41. lemma OAI.MicroscopicJamming.rankFiniteSteps_covered line 516
  42. lemma OAI.MicroscopicJamming.cascadeFiniteEdges_covered line 527
  43. lemma OAI.MicroscopicJamming.rankGrowing_finiteSteps_law line 535
  44. def OAI.MicroscopicJamming.coordinateLaw line 571
  45. instance OAI.MicroscopicJamming.coordinateLaw_probability line 575
  46. lemma OAI.MicroscopicJamming.coordinateLaw_mgf line 579
  47. lemma OAI.MicroscopicJamming.coordinateLaw_subGaussian line 596
  48. lemma OAI.MicroscopicJamming.mixture_linear_subGaussian line 614