OAI/Probability/JammingConcavity/FamilyCascadeLog.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Family Cascade Log.

  1. def OAI.MicroscopicJamming.familyLeafTotal line 32
  2. def OAI.MicroscopicJamming.familyLogPartition line 39
  3. def OAI.MicroscopicJamming.FamilyCascadeLogStatement line 43
  4. def OAI.MicroscopicJamming.decoratedTreeSpace line 65
  5. abbrev OAI.MicroscopicJamming.DecoratedTree line 71
  6. instance OAI.MicroscopicJamming.decoratedTreeMeasurable line 72
  7. def OAI.MicroscopicJamming.transformedDecoratedTree line 75
  8. def OAI.MicroscopicJamming.decoratedTransition line 83
  9. def OAI.MicroscopicJamming.decoratedCascadeLaw line 87
  10. def OAI.MicroscopicJamming.DecoratedCascadeStatement line 94
  11. def OAI.MicroscopicJamming.rowGaussianBlocks line 109
  12. def OAI.MicroscopicJamming.rowGaussianLaw line 112
  13. def OAI.MicroscopicJamming.RowGaussianCascadeStatement line 115
  14. def OAI.MicroscopicJamming.familyPathGibbs line 138
  15. def OAI.MicroscopicJamming.familyPathMean line 146
  16. def OAI.MicroscopicJamming.FamilyPathStatement line 152
  17. def OAI.MicroscopicJamming.PointCloudCampbellStatement line 173
  18. def OAI.MicroscopicJamming.distinctCloudIntegral line 189
  19. def OAI.MicroscopicJamming.FactorialCloudStatement line 196
  20. def OAI.MicroscopicJamming.stableJump line 215
  21. def OAI.MicroscopicJamming.stableTotal line 218
  22. def OAI.MicroscopicJamming.poissonPartitionNumerator line 221
  23. def OAI.MicroscopicJamming.partitionProduct line 225
  24. def OAI.MicroscopicJamming.CascadeEPPFStatement line 230
  25. def OAI.MicroscopicJamming.expMarkedTotal line 246
  26. def OAI.MicroscopicJamming.unmarkedTotal line 249
  27. def OAI.MicroscopicJamming.cascadeLogIncrement line 252
  28. def OAI.MicroscopicJamming.CascadeLogStatement line 255
  29. def OAI.MicroscopicJamming.expMarkedJump line 272
  30. def OAI.MicroscopicJamming.expMarkedBlock line 275
  31. def OAI.MicroscopicJamming.markedPartitionNumerator line 278
  32. def OAI.MicroscopicJamming.tiltedChildProbability line 283
  33. def OAI.MicroscopicJamming.MarkedEPPFStatement line 288
  34. def OAI.MicroscopicJamming.ReplicaPattern line 308
  35. def OAI.MicroscopicJamming.replicaPatternSize line 312
  36. def OAI.MicroscopicJamming.ValidReplicaPattern line 316
  37. def OAI.MicroscopicJamming.rpcPatternWeight line 321
  38. def OAI.MicroscopicJamming.rpcPatternProduct line 329
  39. def OAI.MicroscopicJamming.RPCPartitionStatement line 334
  40. def OAI.MicroscopicJamming.MarkedReplicaPattern line 353
  41. def OAI.MicroscopicJamming.markedReplicaShape line 357
  42. def OAI.MicroscopicJamming.ValidMarkedReplicaPattern line 361
  43. def OAI.MicroscopicJamming.familyReplicaWeight line 367
  44. def OAI.MicroscopicJamming.familyReplicaMean line 379
  45. def OAI.MicroscopicJamming.FamilyReplicaStatement line 386
  46. lemma OAI.MicroscopicJamming.infinitePi_pair line 408
  47. def OAI.MicroscopicJamming.zipPoissonBin line 444
  48. lemma OAI.MicroscopicJamming.measurable_zipPoissonBin line 447
  49. lemma OAI.MicroscopicJamming.poissonBin_independent_marks line 451
  50. def OAI.MicroscopicJamming.zipPointCloud line 464
  51. lemma OAI.MicroscopicJamming.measurable_zipPointCloud line 467
  52. lemma OAI.MicroscopicJamming.pointCloud_independent_marks line 471
  53. lemma OAI.MicroscopicJamming.measurable_coloredStableSum line 502
  54. lemma OAI.MicroscopicJamming.coloredStable_laplace line 507
  55. lemma OAI.MicroscopicJamming.integrable_log_of_square line 533
  56. lemma OAI.MicroscopicJamming.coloredStable_log_integrable line 543
  57. lemma OAI.MicroscopicJamming.probability_eq_of_scalar_laplace line 560
  58. lemma OAI.MicroscopicJamming.law_eq_of_real_laplace line 582
  59. lemma OAI.MicroscopicJamming.coloredStable_log_shift line 618