OAI/Probability/JammingConcavity/UniversalRPCRank.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Universal R P C Rank.

  1. lemma OAI.MicroscopicJamming.realizedRankLaw_reindex line 49
  2. lemma OAI.MicroscopicJamming.realizedRankLaw_positive line 71
  3. theorem OAI.MicroscopicJamming.universalRPCRank line 83
  4. lemma OAI.MicroscopicJamming.rowClosedProfile_eq line 100
  5. lemma OAI.MicroscopicJamming.rowClosedProfile_monotone line 103
  6. lemma OAI.MicroscopicJamming.measurable_rowClosedProfile line 109
  7. lemma OAI.MicroscopicJamming.rowClosedProfile_bound line 111
  8. lemma OAI.MicroscopicJamming.rank_pair_permutation line 115
  9. lemma OAI.MicroscopicJamming.realizedRankLaw_pair_uniform line 128
  10. lemma OAI.MicroscopicJamming.measurable_rowFullRankCovariance line 139
  11. lemma OAI.MicroscopicJamming.rowFullRankCovariance_psd line 150
  12. lemma OAI.MicroscopicJamming.pi_prod_pair_map line 173
  13. lemma OAI.MicroscopicJamming.lintegral_cascadeFiniteReplicaLaw line 203
  14. lemma OAI.MicroscopicJamming.measurable_rootPathField_pair line 217
  15. lemma OAI.MicroscopicJamming.measurable_rowReplicaSiteField line 225
  16. lemma OAI.MicroscopicJamming.measurable_rowReplicaKernelView line 231
  17. def OAI.MicroscopicJamming.rowReplicaRearrange line 249
  18. lemma OAI.MicroscopicJamming.measurable_rowReplicaRearrange line 253
  19. lemma OAI.MicroscopicJamming.rowReplicaRearrangement_law line 257
  20. lemma OAI.MicroscopicJamming.rowPathAgree_iff_shared line 316
  21. lemma OAI.MicroscopicJamming.rowReplicaResidualCovariance_signature line 333
  22. lemma OAI.MicroscopicJamming.measurable_rankGenealogySignature line 346
  23. lemma OAI.MicroscopicJamming.rowRankSignature_law line 357
  24. lemma OAI.MicroscopicJamming.gaussianLinear_law line 403
  25. lemma OAI.MicroscopicJamming.pi_gaussian_scale line 450
  26. lemma OAI.MicroscopicJamming.pi_map_curry line 461
  27. def OAI.MicroscopicJamming.gaussianCoordinateRealization line 467
  28. lemma OAI.MicroscopicJamming.measurable_gaussianCoordinateRealization line 472
  29. lemma OAI.MicroscopicJamming.gaussianCoordinateRealization_law line 478
  30. def OAI.MicroscopicJamming.weightedGaussianMatrix line 502
  31. lemma OAI.MicroscopicJamming.gaussianWeightedLinear_law line 505
  32. lemma OAI.MicroscopicJamming.weightedGaussianMatrix_gram line 524
  33. def OAI.MicroscopicJamming.rowReplicaSupport line 543
  34. def OAI.MicroscopicJamming.rowReplicaLeaf line 546
  35. def OAI.MicroscopicJamming.rowReplicaMatrix line 549
  36. lemma OAI.MicroscopicJamming.rowReplicaMatrix_mulVec line 554
  37. lemma OAI.MicroscopicJamming.rowReplicaMatrix_gram line 564
  38. lemma OAI.MicroscopicJamming.rowReplicaGaussian_finite line 582
  39. theorem OAI.MicroscopicJamming.rowReplicaGaussian line 614
  40. lemma OAI.MicroscopicJamming.multivariateGaussian_zero_conv line 642
  41. lemma OAI.MicroscopicJamming.gaussianDiagonal_law line 655
  42. lemma OAI.MicroscopicJamming.measurable_rowReplicaGaussianField line 677
  43. theorem OAI.MicroscopicJamming.rowReplicaResidual line 682
  44. lemma OAI.MicroscopicJamming.gaussianJointLaw_of_fibers line 709