OAI/Probability/JammingConcavity/StableLawScaling.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Stable Law Scaling.

  1. lemma OAI.MicroscopicJamming.coloredStable_scaled_identDistrib line 35
  2. def OAI.MicroscopicJamming.extendedStableSum line 75
  3. lemma OAI.MicroscopicJamming.measurable_extendedStableSum line 78
  4. lemma OAI.MicroscopicJamming.extendedStableSum_colored line 84
  5. lemma OAI.MicroscopicJamming.extendedStable_scaled_identDistrib line 94
  6. lemma OAI.MicroscopicJamming.scaledENN_rpow line 121
  7. lemma OAI.MicroscopicJamming.scaledENN_log line 127
  8. lemma OAI.MicroscopicJamming.scaledLaw_rpow line 132
  9. lemma OAI.MicroscopicJamming.scaledLaw_positive line 145
  10. lemma OAI.MicroscopicJamming.scaledLaw_centered_log line 155
  11. lemma OAI.MicroscopicJamming.integral_pos_of_positive_ae line 175
  12. lemma OAI.MicroscopicJamming.scaled_family_rpow line 185
  13. lemma OAI.MicroscopicJamming.familyLeafTotal_identDistrib line 221
  14. lemma OAI.MicroscopicJamming.familyLeafTotal_zero line 292
  15. theorem OAI.MicroscopicJamming.familyCascadeLog line 303
  16. lemma OAI.MicroscopicJamming.measurable_measure_withDensity line 357
  17. def OAI.MicroscopicJamming.weightedMass line 365
  18. def OAI.MicroscopicJamming.weightedFiniteKernel line 368
  19. instance OAI.MicroscopicJamming.weightedFiniteKernel_finite line 377
  20. def OAI.MicroscopicJamming.weightedHullDensity line 389
  21. lemma OAI.MicroscopicJamming.measurable_weightedHullDensity line 393
  22. def OAI.MicroscopicJamming.weightedHull line 399
  23. lemma OAI.MicroscopicJamming.weightedHull_sfinite line 403
  24. lemma OAI.MicroscopicJamming.weightedHull_eq line 410
  25. lemma OAI.MicroscopicJamming.measurableSet_mem_evaluated_list line 439
  26. lemma OAI.MicroscopicJamming.measurable_distinctCloudIntegral line 451
  27. lemma OAI.MicroscopicJamming.distinctCloudIntegral_add_dirac line 485
  28. def OAI.MicroscopicJamming.finiteCounting line 509
  29. lemma OAI.MicroscopicJamming.measurable_finiteCounting line 512
  30. lemma OAI.MicroscopicJamming.finiteCounting_insert line 516
  31. lemma OAI.MicroscopicJamming.finite_counting_campbell line 523
  32. def OAI.MicroscopicJamming.poissonBinMeasure line 555
  33. lemma OAI.MicroscopicJamming.measurable_poissonBinMeasure line 558
  34. lemma OAI.MicroscopicJamming.lintegral_poissonBinMeasure line 564
  35. lemma OAI.MicroscopicJamming.measurable_bin_functional line 570
  36. lemma OAI.MicroscopicJamming.poisson_one_shift line 586
  37. lemma OAI.MicroscopicJamming.iid_prefix_counting line 597
  38. lemma OAI.MicroscopicJamming.poisson_bin_campbell line 604