OAI/Probability/JammingConcavity/CloudCountingDecomposition.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Cloud Counting Decomposition.

  1. def OAI.MicroscopicJamming.cloudShift line 35
  2. lemma OAI.MicroscopicJamming.measurable_cloudShift line 37
  3. def OAI.MicroscopicJamming.cloudBinMeasure line 40
  4. lemma OAI.MicroscopicJamming.measurable_cloudBinMeasure line 43
  5. lemma OAI.MicroscopicJamming.poissonBinMeasure_eq_sum line 47
  6. lemma OAI.MicroscopicJamming.cloudBinMeasure_eq_sum line 65
  7. lemma OAI.MicroscopicJamming.pointCloudMeasure_bins line 76
  8. def OAI.MicroscopicJamming.pointCloudRest line 81
  9. lemma OAI.MicroscopicJamming.measurable_pointCloudRest line 84
  10. lemma OAI.MicroscopicJamming.pointCloudMeasure_split line 96
  11. lemma OAI.MicroscopicJamming.pointCloudMeasure_update line 106
  12. lemma OAI.MicroscopicJamming.measurable_cloudBin_functional line 118
  13. lemma OAI.MicroscopicJamming.measurable_iid_update line 136
  14. lemma OAI.MicroscopicJamming.iid_update_preserving line 144
  15. lemma OAI.MicroscopicJamming.lintegral_iid_refresh line 182
  16. lemma OAI.MicroscopicJamming.cloud_bin_campbell line 200
  17. lemma OAI.MicroscopicJamming.cloud_campbell_one_bin line 224
  18. theorem OAI.MicroscopicJamming.pointCloudCampbell line 267
  19. def OAI.MicroscopicJamming.cloudFiniteWeight line 308
  20. lemma OAI.MicroscopicJamming.measurable_cloudFiniteWeight line 310
  21. lemma OAI.MicroscopicJamming.cloudFiniteWeight_ne_zero line 313
  22. lemma OAI.MicroscopicJamming.cloudFiniteWeight_ne_top line 316
  23. lemma OAI.MicroscopicJamming.cloud_intensity_weight line 319
  24. lemma OAI.MicroscopicJamming.cloud_weightedMass_ae_finite line 328
  25. def OAI.MicroscopicJamming.cloudHull line 339
  26. instance OAI.MicroscopicJamming.cloudHull_sfinite line 342
  27. lemma OAI.MicroscopicJamming.cloudHull_eq line 345
  28. lemma OAI.MicroscopicJamming.cloud_weightedMass_add_dirac_finite line 349
  29. lemma OAI.MicroscopicJamming.measurable_distinct_cloud_hull line 365
  30. lemma OAI.MicroscopicJamming.measurable_distinct_cloud_hull_cons line 375
  31. lemma OAI.MicroscopicJamming.aemeasurable_distinct_cloud line 388
  32. def OAI.MicroscopicJamming.cloudLaplaceFactor line 398
  33. lemma OAI.MicroscopicJamming.measurable_cloudLaplaceFactor line 401
  34. lemma OAI.MicroscopicJamming.cloudLaplaceFactor_add_dirac line 405
  35. def OAI.MicroscopicJamming.cloudAtomKernel line 423
  36. instance OAI.MicroscopicJamming.cloudAtomKernel_finite line 429
  37. def OAI.MicroscopicJamming.cloudKernel line 434
  38. instance OAI.MicroscopicJamming.cloudKernel_sfinite line 437
  39. lemma OAI.MicroscopicJamming.cloudKernel_apply line 442
  40. lemma OAI.MicroscopicJamming.measurable_distinct_actual_cloud line 448
  41. lemma OAI.MicroscopicJamming.stable_positive_moment_value line 467
  42. lemma OAI.MicroscopicJamming.measurable_stableTotal line 529
  43. lemma OAI.MicroscopicJamming.stableTotal_is_integral line 533
  44. lemma OAI.MicroscopicJamming.stableTotal_properties line 539
  45. lemma OAI.MicroscopicJamming.stableTotal_moment line 577
  46. lemma OAI.MicroscopicJamming.measurable_expMarkedJump line 596
  47. lemma OAI.MicroscopicJamming.measurable_expMarkedBlock line 600
  48. lemma OAI.MicroscopicJamming.expMarkedTotal_integral line 606
  49. lemma OAI.MicroscopicJamming.measurable_expMarkedTotal line 615
  50. lemma OAI.MicroscopicJamming.expMarkedTotal_properties line 619
  51. lemma OAI.MicroscopicJamming.expMarkedTotal_moment_eq line 638