OAI/Probability/JammingConcavity/RowRankTerminalStability.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Row Rank Terminal Stability.

  1. lemma OAI.MicroscopicJamming.row_rank_uniform_gradient line 31
  2. lemma OAI.MicroscopicJamming.row_rank_difference_bound line 46
  3. lemma OAI.MicroscopicJamming.canonicalRank_exists line 123
  4. lemma OAI.MicroscopicJamming.canonicalRank_penalty_bound line 129
  5. lemma OAI.MicroscopicJamming.canonicalRank_penalty_limit line 154
  6. def OAI.MicroscopicJamming.RowSmoothConcavityStatement line 174
  7. lemma OAI.MicroscopicJamming.canonicalRank_chord_concavity line 190
  8. theorem OAI.MicroscopicJamming.rowSmoothConcavity line 218
  9. def OAI.MicroscopicJamming.rowTiltStep line 243
  10. def OAI.MicroscopicJamming.rowDerivativeDepthMoment line 249
  11. def OAI.MicroscopicJamming.GaussianDerivativeMartingaleStatement line 257
  12. def OAI.MicroscopicJamming.pointCloudMeasure line 280
  13. def OAI.MicroscopicJamming.PointCloudMeasureMarkingStatement line 284
  14. lemma OAI.MicroscopicJamming.pointCloudTilt_probability line 301
  15. lemma OAI.MicroscopicJamming.marked_intensity_scale line 311
  16. theorem OAI.MicroscopicJamming.pointCloudMarking line 332
  17. lemma OAI.MicroscopicJamming.expNeg_injective line 355
  18. lemma OAI.MicroscopicJamming.expNeg_nsmul line 369
  19. def OAI.MicroscopicJamming.laplaceCoordinate line 374
  20. def OAI.MicroscopicJamming.laplacePolynomial line 377
  21. lemma OAI.MicroscopicJamming.laplacePolynomial_monomial line 380
  22. lemma OAI.MicroscopicJamming.laplacePolynomial_separates line 389
  23. def OAI.MicroscopicJamming.compactLaplaceIntegral line 397
  24. lemma OAI.MicroscopicJamming.probability_eq_of_laplace line 407
  25. lemma OAI.MicroscopicJamming.probability_eq_of_finite_marginals line 441
  26. def OAI.MicroscopicJamming.measureEvaluations line 452
  27. lemma OAI.MicroscopicJamming.measurable_measureEvaluations line 455
  28. lemma OAI.MicroscopicJamming.measureEvaluations_comap line 459
  29. lemma OAI.MicroscopicJamming.measure_law_eq_of_evaluations line 465
  30. def OAI.MicroscopicJamming.finiteMeasureTest line 476
  31. lemma OAI.MicroscopicJamming.measurable_finiteMeasureTest line 480
  32. lemma OAI.MicroscopicJamming.integral_finiteMeasureTest line 486
  33. lemma OAI.MicroscopicJamming.probability_finite_measure_evaluations_eq line 500
  34. lemma OAI.MicroscopicJamming.probability_measure_law_eq_of_laplace line 520
  35. lemma OAI.MicroscopicJamming.measurable_pointCloudMeasure line 542
  36. lemma OAI.MicroscopicJamming.lintegral_pointCloudMeasure line 558
  37. theorem OAI.MicroscopicJamming.pointCloudMeasureMarking line 578
  38. def OAI.MicroscopicJamming.weightTreeSpace line 613
  39. abbrev OAI.MicroscopicJamming.WeightTree line 619
  40. instance OAI.MicroscopicJamming.weightTreeMeasurable line 621
  41. def OAI.MicroscopicJamming.weightTreeLaw line 623
  42. def OAI.MicroscopicJamming.FamilyCascadeTree line 627
  43. instance OAI.MicroscopicJamming.familyCascadeMeasurable line 631
  44. def OAI.MicroscopicJamming.familyCascadeLaw line 638
  45. def OAI.MicroscopicJamming.familyRecursion line 643
  46. def OAI.MicroscopicJamming.FamilyMomentsFinite line 649
  47. def OAI.MicroscopicJamming.familyEdgeMultiplier line 657
  48. def OAI.MicroscopicJamming.transformedWeightTree line 661
  49. def OAI.MicroscopicJamming.CascadeGenealogyStatement line 669