OAI/Probability/JammingConcavity/StableJumpIntegral.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Stable Jump Integral.

  1. lemma OAI.MicroscopicJamming.lintegral_comp_rpow_positive_halfline line 35
  2. lemma OAI.MicroscopicJamming.unscaled_jump_gamma line 56
  3. lemma OAI.MicroscopicJamming.measurable_stableJump line 89
  4. lemma OAI.MicroscopicJamming.stableJump_eq_div line 92
  5. lemma OAI.MicroscopicJamming.selected_jump_gamma line 98
  6. lemma OAI.MicroscopicJamming.stableJump_exp line 133
  7. lemma OAI.MicroscopicJamming.selected_exp_jump line 140
  8. lemma OAI.MicroscopicJamming.tiltedChildProbability_ne_top line 155
  9. lemma OAI.MicroscopicJamming.selected_exp_marked_block line 166
  10. lemma OAI.MicroscopicJamming.cloud_intensity_ae_not_in line 208
  11. lemma OAI.MicroscopicJamming.factorial_cloud_exclusions line 217
  12. theorem OAI.MicroscopicJamming.factorialCloud line 297
  13. lemma OAI.MicroscopicJamming.stable_cloudLaplaceFactor line 310
  14. lemma OAI.MicroscopicJamming.stable_cloudLaplaceFactor_ae line 320
  15. lemma OAI.MicroscopicJamming.stable_laplace_ennreal line 328
  16. lemma OAI.MicroscopicJamming.stable_factorial_laplace line 338
  17. instance OAI.MicroscopicJamming.measurableEq_product line 362
  18. lemma OAI.MicroscopicJamming.expMarked_laplaceFactor_ae line 373
  19. lemma OAI.MicroscopicJamming.expMarked_laplace_ennreal line 386
  20. lemma OAI.MicroscopicJamming.expMarked_factorial_laplace line 399
  21. lemma OAI.MicroscopicJamming.expMarked_factorial_comparison line 418
  22. instance OAI.MicroscopicJamming.measurableEq_countableFun line 474
  23. instance OAI.MicroscopicJamming.cascadeTree_measurableEq line 485
  24. lemma OAI.MicroscopicJamming.replicaPatternSize_pos line 491
  25. lemma OAI.MicroscopicJamming.measurable_rpcPatternWeight line 505
  26. instance OAI.MicroscopicJamming.familyCascadeTree_measurableEq line 533
  27. lemma OAI.MicroscopicJamming.pointCloudFunctional_mono line 540
  28. lemma OAI.MicroscopicJamming.measurable_familyPathGibbs line 548
  29. lemma OAI.MicroscopicJamming.familyPathGibbs_le_one line 565
  30. lemma OAI.MicroscopicJamming.measurable_familyPathMean line 578
  31. lemma OAI.MicroscopicJamming.decoratedTransition_probability line 597
  32. lemma OAI.MicroscopicJamming.familyPathMean_le_one line 605