OAI/Probability/JammingConcavity/CascadePathCoordinates.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Cascade Path Coordinates.

  1. def OAI.MicroscopicJamming.cascadePathIndex line 37
  2. lemma OAI.MicroscopicJamming.cascadePathIndex_depth line 42
  3. lemma OAI.MicroscopicJamming.cascadePathIndex_injective line 52
  4. lemma OAI.MicroscopicJamming.familyPathMark_zip line 58
  5. lemma OAI.MicroscopicJamming.familyPathMark_coordinates line 71
  6. lemma OAI.MicroscopicJamming.measurable_familyPathWeight line 85
  7. lemma OAI.MicroscopicJamming.measurable_familyPathMark line 102
  8. def OAI.MicroscopicJamming.normalizedFamilyPathWeight line 120
  9. lemma OAI.MicroscopicJamming.measurable_normalizedFamilyPathWeight line 124
  10. lemma OAI.MicroscopicJamming.normalized_familyPath_series line 129
  11. lemma OAI.MicroscopicJamming.normalized_familyPath_weights line 150
  12. lemma OAI.MicroscopicJamming.forgetFamilyMarks_zip line 168
  13. def OAI.MicroscopicJamming.normalizedCascadePathWeight line 181
  14. lemma OAI.MicroscopicJamming.normalizedFamilyPathWeight_zip line 184
  15. def OAI.MicroscopicJamming.rootMarkCoordinates line 192
  16. lemma OAI.MicroscopicJamming.measurable_rootMarkCoordinates line 195
  17. lemma OAI.MicroscopicJamming.rootMarkCoordinates_law line 203
  18. def OAI.MicroscopicJamming.rootPathField line 217
  19. lemma OAI.MicroscopicJamming.rootPathField_eq line 221
  20. def OAI.MicroscopicJamming.zipRootCascade line 227
  21. lemma OAI.MicroscopicJamming.measurable_zipRootCascade line 230
  22. lemma OAI.MicroscopicJamming.zipRootCascade_law line 235
  23. lemma OAI.MicroscopicJamming.integral_cascade_coordinates line 246
  24. lemma OAI.MicroscopicJamming.enn_pair_sum_mul line 274
  25. lemma OAI.MicroscopicJamming.enn_pair_same_block line 280
  26. lemma OAI.MicroscopicJamming.enn_pair_scale line 295
  27. def OAI.MicroscopicJamming.pathAgree line 314
  28. def OAI.MicroscopicJamming.familyLeafMass line 319
  29. def OAI.MicroscopicJamming.familyPairSum line 323
  30. lemma OAI.MicroscopicJamming.tsum_familyLeafMass line 328
  31. lemma OAI.MicroscopicJamming.pathAgree_zero line 334
  32. lemma OAI.MicroscopicJamming.familyPairSum_zero line 337
  33. lemma OAI.MicroscopicJamming.familyLeafMass_cons line 343
  34. lemma OAI.MicroscopicJamming.familyPairSum_cons line 353
  35. lemma OAI.MicroscopicJamming.cascadePathIndex_eq_iff line 390
  36. lemma OAI.MicroscopicJamming.cascadePathIndex_depth_eq line 405
  37. def OAI.MicroscopicJamming.rootPathIndex line 410
  38. lemma OAI.MicroscopicJamming.rootPathIndex_injective line 413
  39. lemma OAI.MicroscopicJamming.rootPathIndex_depth_eq line 428
  40. lemma OAI.MicroscopicJamming.rootPathIndex_eq_iff line 440
  41. lemma OAI.MicroscopicJamming.finite_incidence_covariance line 447
  42. def OAI.MicroscopicJamming.cascadeCoordinateSet line 483
  43. lemma OAI.MicroscopicJamming.rootPathIndex_mem line 486
  44. def OAI.MicroscopicJamming.finiteRootPathIndex line 491
  45. def OAI.MicroscopicJamming.finiteRootPathField line 494
  46. lemma OAI.MicroscopicJamming.rootPathField_finite line 497
  47. lemma OAI.MicroscopicJamming.measurable_finiteRootPathField line 503
  48. lemma OAI.MicroscopicJamming.integral_cascade_finite_coordinates line 509
  49. lemma OAI.MicroscopicJamming.weighted_incidence_covariance line 545
  50. def OAI.MicroscopicJamming.rootCoordinateVariance line 573
  51. def OAI.MicroscopicJamming.pathCovarianceDifference line 577
  52. lemma OAI.MicroscopicJamming.rootVariance_path line 582
  53. lemma OAI.MicroscopicJamming.finiteRoot_incidence_covariance line 590
  54. def OAI.MicroscopicJamming.rowReplicaCovariance line 623
  55. def OAI.MicroscopicJamming.rowReplicaGaussianField line 627
  56. def OAI.MicroscopicJamming.RowReplicaGaussianStatement line 631
  57. def OAI.MicroscopicJamming.rowReplicaResidualCovariance line 647
  58. def OAI.MicroscopicJamming.rowReplicaResidualField line 651
  59. def OAI.MicroscopicJamming.RowReplicaResidualStatement line 655
  60. def OAI.MicroscopicJamming.gaussianAdjunctionMap line 672
  61. def OAI.MicroscopicJamming.gaussianAdjunctionMeasure line 677
  62. def OAI.MicroscopicJamming.GaussianAdjunctionStatement line 682