OAI/Probability/JammingConcavity/CascadeGenealogyBase.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Cascade Genealogy Base.

  1. lemma OAI.MicroscopicJamming.weightTreeLaw_probability line 33
  2. lemma OAI.MicroscopicJamming.familyCascadeLaw_probability line 41
  3. lemma OAI.MicroscopicJamming.measurable_familyRecursion line 51
  4. lemma OAI.MicroscopicJamming.measurable_familyEdgeMultiplier line 63
  5. lemma OAI.MicroscopicJamming.familyEdgeMultiplier_moment line 72
  6. lemma OAI.MicroscopicJamming.pointCloudMeasure_pushforward line 102
  7. lemma OAI.MicroscopicJamming.measurable_parameterized_cloud_map line 122
  8. lemma OAI.MicroscopicJamming.pointCloudMeasure_markLaw line 157
  9. lemma OAI.MicroscopicJamming.measurable_transformedWeightTree line 173
  10. lemma OAI.MicroscopicJamming.pointCloudTilt_prod line 199
  11. lemma OAI.MicroscopicJamming.pointCloud_scaled_forget_law line 207
  12. lemma OAI.map_fiber_product line 253
  13. theorem OAI.MicroscopicJamming.cascadeGenealogy line 276
  14. def OAI.MicroscopicJamming.CascadeMarkTree line 341
  15. instance OAI.MicroscopicJamming.cascadeMarkMeasurable line 345
  16. def OAI.MicroscopicJamming.cascadeMarkLaw line 352
  17. instance OAI.MicroscopicJamming.cascadeMarkLaw_probability line 358
  18. def OAI.MicroscopicJamming.zipCascade line 368
  19. lemma OAI.MicroscopicJamming.measurable_zipCascade line 373
  20. lemma OAI.MicroscopicJamming.prod_rotate_map line 382
  21. theorem OAI.MicroscopicJamming.cascade_independent_marks line 391
  22. def OAI.MicroscopicJamming.spinI line 430
  23. def OAI.MicroscopicJamming.spinLambda line 434
  24. def OAI.MicroscopicJamming.spinC line 436
  25. def OAI.MicroscopicJamming.spinV line 441
  26. def OAI.MicroscopicJamming.spinTerminal line 446
  27. def OAI.MicroscopicJamming.spinIncrementLaw line 448
  28. def OAI.MicroscopicJamming.spinSampleTest line 450
  29. def OAI.MicroscopicJamming.GaussianHierarchyStatement line 453
  30. def OAI.MicroscopicJamming.vectorSpinTerminal line 478
  31. def OAI.MicroscopicJamming.vectorSpinLaw line 481
  32. def OAI.MicroscopicJamming.vectorSpinTest line 484
  33. def OAI.MicroscopicJamming.GaussianVectorStatement line 487
  34. def OAI.MicroscopicJamming.spinTotalIncrement line 514
  35. def OAI.MicroscopicJamming.spinX line 518
  36. def OAI.MicroscopicJamming.spinSaddleLHS line 521
  37. def OAI.MicroscopicJamming.SpinSaddleStatement line 524
  38. def OAI.MicroscopicJamming.spinShellBad line 542
  39. def OAI.MicroscopicJamming.gaussianSpinDisorder line 545
  40. def OAI.MicroscopicJamming.gaussianSpinBadMass line 550
  41. def OAI.MicroscopicJamming.GaussianShellStatement line 555
  42. def OAI.MicroscopicJamming.gaussianSpinLog line 575
  43. def OAI.MicroscopicJamming.GaussianLogMomentStatement line 579
  44. def OAI.MicroscopicJamming.forgetFamilyMarks line 595
  45. def OAI.MicroscopicJamming.familyUnmarkedTotal line 599
  46. lemma OAI.MicroscopicJamming.measurable_forgetFamilyMarks line 603
  47. lemma OAI.MicroscopicJamming.familyCascadeLaw_forget line 609
  48. lemma OAI.MicroscopicJamming.measurable_familyLeafTotal line 626
  49. lemma OAI.MicroscopicJamming.measurable_familyUnmarkedTotal line 637
  50. lemma OAI.MicroscopicJamming.familyUnmarkedTotal_cons line 641
  51. lemma OAI.MicroscopicJamming.familyUnmarkedTotal_properties line 647
  52. def OAI.MicroscopicJamming.familyPositiveTotal line 671
  53. def OAI.MicroscopicJamming.gaussianSpinShellTerminal line 677
  54. def OAI.MicroscopicJamming.gaussianSpinShellPartition line 681
  55. def OAI.MicroscopicJamming.gaussianSpinShellLog line 686
  56. def OAI.MicroscopicJamming.GaussianShellLogStatement line 690