OAI/Probability/JammingConcavity/RowCommonRankContinuity.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Row Common Rank Continuity.

  1. def OAI.MicroscopicJamming.rowClosedProfile line 39
  2. def OAI.MicroscopicJamming.rowFullRankCovariance line 41
  3. def OAI.MicroscopicJamming.RowCommonRankContinuityStatement line 45
  4. def OAI.MicroscopicJamming.rowReplicaDiagonal line 64
  5. def OAI.MicroscopicJamming.RowReplicaMomentsStatement line 67
  6. lemma OAI.MicroscopicJamming.rpcStepLevel_monotone line 85
  7. def OAI.MicroscopicJamming.rowCascadeProfile line 99
  8. def OAI.MicroscopicJamming.RowCascadeLogContinuityStatement line 121
  9. def OAI.MicroscopicJamming.replicaFirst line 143
  10. def OAI.MicroscopicJamming.replicaFieldView line 146
  11. def OAI.MicroscopicJamming.replicaFieldLaw line 151
  12. def OAI.MicroscopicJamming.ReplicaLawContinuityStatement line 156
  13. def OAI.MicroscopicJamming.RowRetainedRankLawStatement line 185
  14. lemma OAI.MicroscopicJamming.rankBirth_nonneg line 207
  15. lemma OAI.MicroscopicJamming.rankBirth_le_one line 210
  16. lemma OAI.MicroscopicJamming.le_rankBirth_iff line 216
  17. lemma OAI.MicroscopicJamming.birth_cluster_iff line 224
  18. lemma OAI.MicroscopicJamming.rankCluster_nonempty line 239
  19. lemma OAI.MicroscopicJamming.rankBirth_lt_at_min line 244
  20. lemma OAI.MicroscopicJamming.le_rankBirth_of_not_min line 252
  21. lemma OAI.MicroscopicJamming.rankInsert_finiteRank line 260
  22. lemma OAI.MicroscopicJamming.continuous_rankBirth line 308
  23. lemma OAI.MicroscopicJamming.continuous_rankInsert_fixed line 316
  24. lemma OAI.MicroscopicJamming.continuous_rankInsert line 331
  25. lemma OAI.MicroscopicJamming.rankLink_volume line 340
  26. lemma OAI.MicroscopicJamming.rankInsert_cluster_probability line 380
  27. theorem OAI.MicroscopicJamming.rpcRankInsertion line 390
  28. lemma OAI.MicroscopicJamming.continuous_rankGrowing line 404
  29. lemma OAI.MicroscopicJamming.rankGrowing_stable line 410
  30. lemma OAI.MicroscopicJamming.realizedRank_stage line 428
  31. lemma OAI.MicroscopicJamming.continuous_realizedRank line 436
  32. lemma OAI.MicroscopicJamming.rankGrowing_finiteRank line 443
  33. lemma OAI.MicroscopicJamming.realizedRank_constraints line 452
  34. lemma OAI.MicroscopicJamming.realizedRank_pair line 481
  35. instance OAI.MicroscopicJamming.rankUnitInterval_probability line 502
  36. instance OAI.MicroscopicJamming.rankInnovationLaw_probability line 505
  37. instance OAI.MicroscopicJamming.rankSeedLaw_probability line 509
  38. instance OAI.MicroscopicJamming.realizedRankLaw_probability line 513
  39. lemma OAI.MicroscopicJamming.rankInnovation_second line 517
  40. lemma OAI.MicroscopicJamming.rankSeed_coordinate line 521
  41. lemma OAI.MicroscopicJamming.rankSeed_valid line 527
  42. lemma OAI.MicroscopicJamming.realizedRankLaw_constraints line 535
  43. lemma OAI.MicroscopicJamming.realizedRankLaw_uniform line 553
  44. theorem OAI.MicroscopicJamming.rpcRankRealization line 561
  45. def OAI.MicroscopicJamming.rankJoinEvent line 572
  46. lemma OAI.MicroscopicJamming.measurableSet_rankJoinEvent line 575
  47. lemma OAI.MicroscopicJamming.rankJoinEvent_real line 585
  48. lemma OAI.MicroscopicJamming.rankJoinEvent_zero line 609
  49. lemma OAI.MicroscopicJamming.rankJoinEvent_real_nonneg line 615
  50. lemma OAI.MicroscopicJamming.rankLink_parent_le line 627
  51. lemma OAI.MicroscopicJamming.rankLink_pair_le line 633
  52. lemma OAI.MicroscopicJamming.rankJoinEvent_subset line 639
  53. lemma OAI.MicroscopicJamming.rankJoinEvent_disjoint line 645
  54. lemma OAI.MicroscopicJamming.rankFreshBranch_real line 654