OAI/Probability/JammingConcavity/RPCLabelBridge.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

R P C Label Bridge.

  1. lemma OAI.MicroscopicJamming.lintegral_pointCloudMeasure_labels line 39
  2. lemma OAI.MicroscopicJamming.labelCloudIntegral_points line 52
  3. instance OAI.MicroscopicJamming.replicaPatternEncodable line 81
  4. lemma OAI.MicroscopicJamming.rpcLabelPatternWeight_eq_ae line 87
  5. lemma OAI.MicroscopicJamming.ae_cloud_measure_marks line 133
  6. lemma OAI.MicroscopicJamming.distinctCloudIntegral_congr_ae line 143
  7. lemma OAI.MicroscopicJamming.exp_log_cascadeTotal_ae line 158
  8. lemma OAI.MicroscopicJamming.cascadeTotal_expMarked_ae line 165
  9. lemma OAI.MicroscopicJamming.exp_mul_log_cascadeTotal_ae line 184
  10. lemma OAI.MicroscopicJamming.gamma_lintegral line 199
  11. lemma OAI.MicroscopicJamming.mellin_negative_power line 221
  12. lemma OAI.MicroscopicJamming.generalized_gamma_lintegral line 227
  13. lemma OAI.MicroscopicJamming.weighted_mellin_lintegral line 247
  14. lemma OAI.MicroscopicJamming.weighted_mellin_comparison line 272
  15. def OAI.MicroscopicJamming.stableGammaProduct line 301
  16. lemma OAI.MicroscopicJamming.stableGammaProduct_pos line 304
  17. lemma OAI.MicroscopicJamming.stable_gamma_factor_product line 314
  18. lemma OAI.MicroscopicJamming.stable_mellin_factorial line 337
  19. lemma OAI.MicroscopicJamming.stable_partition_numerator_value line 378
  20. lemma OAI.MicroscopicJamming.gamma_nat_sub_product line 435
  21. lemma OAI.MicroscopicJamming.scaled_partition_product line 447
  22. lemma OAI.MicroscopicJamming.partition_denominator_pos line 458
  23. lemma OAI.MicroscopicJamming.stableGammaProduct_eq line 475
  24. lemma OAI.MicroscopicJamming.eppf_algebra line 488
  25. lemma OAI.MicroscopicJamming.partition_natural_bounds line 499
  26. lemma OAI.MicroscopicJamming.stable_partition_gamma_ratio line 503
  27. theorem OAI.MicroscopicJamming.cascadeEPPF line 535
  28. lemma OAI.MicroscopicJamming.marked_partition_comparison line 565
  29. theorem OAI.MicroscopicJamming.markedEPPF line 598
  30. def OAI.MicroscopicJamming.weightedMarkedBlock line 623
  31. def OAI.MicroscopicJamming.weightedChildMean line 626
  32. def OAI.MicroscopicJamming.weightedMarkedPartitionNumerator line 631
  33. lemma OAI.MicroscopicJamming.measurable_weightedMarkedBlock line 636
  34. lemma OAI.MicroscopicJamming.selected_exp_weighted_block line 647