OAI/Probability/JammingConcavity/FamilyPositiveTotal.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Family Positive Total.

  1. lemma OAI.MicroscopicJamming.pointCloudFunctional_const_mul line 35
  2. lemma OAI.MicroscopicJamming.pointCloudFunctional_add line 40
  3. lemma OAI.MicroscopicJamming.measurable_familyPositiveTotal line 47
  4. lemma OAI.MicroscopicJamming.familyPositiveTotal_mono line 58
  5. lemma OAI.MicroscopicJamming.familyPositiveTotal_exp line 69
  6. lemma OAI.MicroscopicJamming.familyPositiveTotal_const line 77
  7. lemma OAI.MicroscopicJamming.familyPositiveTotal_add line 88
  8. lemma OAI.MicroscopicJamming.familyPathGibbs_positive_ratio line 98
  9. def OAI.MicroscopicJamming.CascadePath line 157
  10. instance OAI.MicroscopicJamming.cascadePathEncodable line 161
  11. def OAI.MicroscopicJamming.cascadePathWeight line 167
  12. def OAI.MicroscopicJamming.familyPathWeight line 173
  13. def OAI.MicroscopicJamming.familyPathMark line 180
  14. lemma OAI.MicroscopicJamming.familyPathWeight_zip line 186
  15. lemma OAI.MicroscopicJamming.tsum_familyPathWeight_terminal line 198
  16. lemma OAI.MicroscopicJamming.tsum_familyPathWeight line 231
  17. abbrev OAI.MicroscopicJamming.CloudLabel line 246
  18. def OAI.MicroscopicJamming.cloudLabelPoint line 248
  19. def OAI.MicroscopicJamming.labelCloudIntegral line 251
  20. def OAI.MicroscopicJamming.rpcLabelPatternWeight line 260
  21. def OAI.MicroscopicJamming.RPCLabelSamplingStatement line 270
  22. instance OAI.MicroscopicJamming.cascadePathMeasurableSpace line 289
  23. instance OAI.MicroscopicJamming.cascadePathMeasurableSingleton line 290
  24. def OAI.MicroscopicJamming.cascadeZeroPath line 293
  25. def OAI.MicroscopicJamming.cascadeLeafLaw line 297
  26. def OAI.MicroscopicJamming.cascadeReplicaLaw line 303
  27. def OAI.MicroscopicJamming.RPCLeafKernelStatement line 306
  28. def OAI.MicroscopicJamming.MarkedPatternIndex line 327
  29. instance OAI.MicroscopicJamming.markedPatternIndexFintype line 331
  30. def OAI.MicroscopicJamming.familySampleLeafLaw line 339
  31. def OAI.MicroscopicJamming.familySampleObservable line 350
  32. def OAI.MicroscopicJamming.familySampleMean line 362
  33. def OAI.MicroscopicJamming.FamilySampleStatement line 368
  34. def OAI.MicroscopicJamming.rowDerivativeTest line 390
  35. def OAI.MicroscopicJamming.rowSinglePattern line 392
  36. def OAI.MicroscopicJamming.rowPairPattern line 397
  37. def OAI.MicroscopicJamming.RowGaussianPairStatement line 403
  38. abbrev OAI.MicroscopicJamming.RankArray line 425
  39. def OAI.MicroscopicJamming.cascadeSharedEdges line 427
  40. def OAI.MicroscopicJamming.rpcStepLevel line 431
  41. def OAI.MicroscopicJamming.cascadeCovarianceArray line 433
  42. def OAI.MicroscopicJamming.rankCovarianceArray line 437
  43. def OAI.MicroscopicJamming.HasRPCFiniteRankLaws line 440
  44. def OAI.MicroscopicJamming.UniversalRPCRankStatement line 447
  45. def OAI.MicroscopicJamming.rowPairIidObservable line 472
  46. def OAI.MicroscopicJamming.RowPairSemanticStatement line 478
  47. def OAI.MicroscopicJamming.rowSignedPairObservable line 492
  48. def OAI.MicroscopicJamming.RowSignedPairStatement line 498
  49. def OAI.MicroscopicJamming.RowFiniteRankTestStatement line 519
  50. lemma OAI.MicroscopicJamming.infinitePi_option line 544
  51. def OAI.MicroscopicJamming.CascadeMarkIndex line 607
  52. instance OAI.MicroscopicJamming.cascadeMarkIndexEncodable line 611
  53. def OAI.MicroscopicJamming.cascadeMarkDepth line 617
  54. def OAI.MicroscopicJamming.cascadeMarkCoordinates line 621
  55. lemma OAI.MicroscopicJamming.measurable_cascadeMarkCoordinates line 626
  56. lemma OAI.MicroscopicJamming.cascadeMarkCoordinates_law line 637