OAI/Probability/JammingConcavity/RowReplicaMixtureFamilyReplicaNumeratorAe.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Row Replica Mixture Family Replica Numerator Ae.

  1. lemma OAI.MicroscopicJamming.rowReplicaMarkedLaw_eq line 55
  2. theorem OAI.MicroscopicJamming.rowReplicaMixture line 69
  3. lemma OAI.MicroscopicJamming.gaussianAdjunction_naturality_countable line 81
  4. theorem OAI.MicroscopicJamming.rowRankGaussian line 115
  5. lemma OAI.MicroscopicJamming.rowReplicaKernelView_factor line 136
  6. lemma OAI.MicroscopicJamming.rowReplicaKernel_law_marked line 145
  7. theorem OAI.MicroscopicJamming.rowReplicaKernel_exact line 165
  8. lemma OAI.MicroscopicJamming.rowCascadeProfile_top line 176
  9. lemma OAI.MicroscopicJamming.rowCascadeProfile_bound line 187
  10. lemma OAI.MicroscopicJamming.rowCascadeCovariance_ae line 192
  11. lemma OAI.MicroscopicJamming.gaussianAdjunction_naturality line 217
  12. lemma OAI.MicroscopicJamming.gaussianAdjunction_congr_ae line 236
  13. lemma OAI.MicroscopicJamming.rowReplicaFields_law line 242
  14. lemma OAI.MicroscopicJamming.rowReplicaRetainedRank_law line 265
  15. theorem OAI.MicroscopicJamming.rowRetainedRankLaw line 277
  16. lemma OAI.MicroscopicJamming.scaledFamilyWeightedMean line 310
  17. lemma OAI.MicroscopicJamming.familyPathMean_cons_ratio line 372
  18. lemma OAI.MicroscopicJamming.measurable_distinctCloudIntegral_param line 414
  19. lemma OAI.MicroscopicJamming.validMarked_shape line 454
  20. lemma OAI.MicroscopicJamming.measurable_familyReplicaWeight line 468
  21. lemma OAI.MicroscopicJamming.measurable_familyReplicaMean line 505
  22. lemma OAI.MicroscopicJamming.familyReplicaMean_le_one line 541
  23. lemma OAI.MicroscopicJamming.decoratedTransition_lintegral_ratio line 578
  24. lemma OAI.MicroscopicJamming.familyLeafTotal_positive_ae line 610
  25. lemma OAI.MicroscopicJamming.familyChildTotal_positive_ae line 619
  26. def OAI.MicroscopicJamming.familyWeightedBlocks line 635
  27. lemma OAI.MicroscopicJamming.familyTotal_expMarked_ae line 641
  28. lemma OAI.MicroscopicJamming.familyReplica_numerator_ae line 663