OAI/Probability/JammingConcavity/WeightedMarkedFactorial.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Weighted Marked Factorial.

  1. lemma OAI.MicroscopicJamming.weightedMarked_factorial_comparison line 38
  2. lemma OAI.MicroscopicJamming.weighted_partition_comparison line 96
  3. theorem OAI.MicroscopicJamming.weightedEPPF line 130
  4. def OAI.MicroscopicJamming.rpcWeightedBlocks line 162
  5. lemma OAI.MicroscopicJamming.weightedChildMean_cascade line 166
  6. lemma OAI.MicroscopicJamming.rpcPattern_numerator_ae line 180
  7. lemma OAI.MicroscopicJamming.partitionProduct_nonneg line 224
  8. lemma OAI.MicroscopicJamming.rpcPatternProduct_nonneg line 245
  9. lemma OAI.MicroscopicJamming.ofReal_list_prod line 261
  10. theorem OAI.MicroscopicJamming.rpcPartition line 278
  11. lemma OAI.MicroscopicJamming.tsum_cascadePathWeight line 357
  12. lemma OAI.MicroscopicJamming.cascadePathWeights_sum_one line 391
  13. theorem OAI.MicroscopicJamming.rpcLabelSampling line 397
  14. lemma OAI.MicroscopicJamming.measurable_cascadePathWeight line 417
  15. lemma OAI.MicroscopicJamming.cascadeLeafLaw_apply_good line 434
  16. lemma OAI.MicroscopicJamming.cascadeLeafLaw_probability line 445
  17. lemma OAI.MicroscopicJamming.measurable_cascadeLeafLaw line 455
  18. lemma OAI.MicroscopicJamming.measurable_infinitePi_kernel line 482
  19. lemma OAI.MicroscopicJamming.cascadeLeafLaw_singleton_good line 493
  20. lemma OAI.MicroscopicJamming.measurable_cascadeReplicaKernel line 500
  21. lemma OAI.MicroscopicJamming.cascadeReplicaLaw_probability line 505
  22. lemma OAI.MicroscopicJamming.cascadeReplicaLaw_cylinder line 512
  23. theorem OAI.MicroscopicJamming.rpcLeafKernel line 529
  24. abbrev OAI.MicroscopicJamming.RowReplicaEnvironment line 547
  25. abbrev OAI.MicroscopicJamming.RowReplicaSite line 548
  26. def OAI.MicroscopicJamming.rowReplicaEnvironmentLaw line 550
  27. def OAI.MicroscopicJamming.rowReplicaKernel line 554
  28. instance OAI.MicroscopicJamming.rowReplicaKernel_markov line 565
  29. def OAI.MicroscopicJamming.rowReplicaSiteField line 571
  30. def OAI.MicroscopicJamming.rowReplicaKernelView line 574
  31. def OAI.MicroscopicJamming.RowReplicaKernelStatement line 578
  32. def OAI.MicroscopicJamming.rowCoordinateLeafKernel line 594
  33. instance OAI.MicroscopicJamming.(instance at line 597) line 597
  34. def OAI.MicroscopicJamming.rowCoordinatePotential line 599
  35. def OAI.MicroscopicJamming.rowCoordinatePair line 602
  36. def OAI.MicroscopicJamming.RowDirectingPairStatement line 607
  37. def OAI.MicroscopicJamming.rowFullPotential line 627
  38. def OAI.MicroscopicJamming.rowFullPair line 630
  39. def OAI.MicroscopicJamming.RowResidualPairStatement line 637
  40. instance OAI.MicroscopicJamming.gaussianMatrixMeasurable line 660
  41. instance OAI.MicroscopicJamming.gaussianMatrixBorel line 662
  42. def OAI.MicroscopicJamming.gaussianObservableKernel line 664
  43. def OAI.MicroscopicJamming.GaussianConditionalL1Statement line 669
  44. structure OAI.MicroscopicJamming.SphericalProfile line 695
  45. def OAI.MicroscopicJamming.sphericalProfileDistance line 700
  46. lemma OAI.MicroscopicJamming.SphericalProfile.bound line 702