OAI/Probability/JammingConcavity/CascadeNormalization.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Cascade Normalization.

  1. def OAI.MicroscopicJamming.CascadeTree line 22
  2. instance OAI.MicroscopicJamming.cascadeTreeMeasurable line 26
  3. def OAI.MicroscopicJamming.cascadeLaw line 32
  4. def OAI.MicroscopicJamming.cascadeTotal line 36
  5. def OAI.MicroscopicJamming.CascadeNormalizationStatement line 41
  6. def OAI.MicroscopicJamming.mapPoissonBin line 55
  7. lemma OAI.MicroscopicJamming.measurable_mapPoissonBin line 58
  8. lemma OAI.MicroscopicJamming.poissonBinLaw_map line 63
  9. lemma OAI.MicroscopicJamming.poissonSeriesLaw_map line 71
  10. def OAI.MicroscopicJamming.mapPointCloud line 79
  11. lemma OAI.MicroscopicJamming.measurable_mapPointCloud line 82
  12. lemma OAI.MicroscopicJamming.pointCloudLaw_map line 88
  13. lemma OAI.MicroscopicJamming.integrable_one_sub_expNeg line 103
  14. lemma OAI.MicroscopicJamming.poisson_series_laplace_general line 108
  15. lemma OAI.MicroscopicJamming.lintegral_unit_shift line 142
  16. lemma OAI.MicroscopicJamming.tsum_lintegral_unit_shifts line 150
  17. lemma OAI.MicroscopicJamming.lintegral_Ioi_div line 156
  18. instance OAI.MicroscopicJamming.pointCloudLaw_probability line 174
  19. lemma OAI.MicroscopicJamming.measurable_pointCloudFunctional line 178
  20. lemma OAI.MicroscopicJamming.pointCloud_laplace line 185
  21. lemma OAI.MicroscopicJamming.laplace_ae_ne_top line 212
  22. lemma OAI.MicroscopicJamming.laplace_real_ae_pos line 265
  23. lemma OAI.MicroscopicJamming.integrable_exp_neg_mul line 318
  24. lemma OAI.MicroscopicJamming.stable_positive_moment line 327
  25. lemma OAI.MicroscopicJamming.stable_negative_moment line 373
  26. lemma OAI.MicroscopicJamming.log_square_le_powers line 423
  27. lemma OAI.MicroscopicJamming.integrable_log_square line 453
  28. theorem OAI.MicroscopicJamming.stableCloud line 472
  29. lemma OAI.MicroscopicJamming.pointCloud_mark_preserving line 525
  30. lemma OAI.MicroscopicJamming.ae_pointCloud_marks line 535
  31. def OAI.MicroscopicJamming.coloredStableSum line 544
  32. lemma OAI.MicroscopicJamming.stableCloudSum_mapPointCloud line 547
  33. lemma OAI.MicroscopicJamming.coloredStable_properties line 552
  34. instance OAI.MicroscopicJamming.cascadeLaw_probability line 586
  35. lemma OAI.MicroscopicJamming.measurable_cascadeTotal line 593
  36. lemma OAI.MicroscopicJamming.pointCloudFunctional_mark_congr line 601
  37. lemma OAI.MicroscopicJamming.cascadeTotal_colored line 614
  38. lemma OAI.MicroscopicJamming.cascadeTotal_properties line 624
  39. theorem OAI.MicroscopicJamming.cascadeNormalization line 668