OAI/Probability/JammingConcavity/RowReplicaMixture.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Row Replica Mixture.

  1. def OAI.MicroscopicJamming.cascadeFiniteReplicaLaw line 39
  2. def OAI.MicroscopicJamming.rowReplicaMarkedLaw line 42
  3. def OAI.MicroscopicJamming.RowReplicaMixtureStatement line 49
  4. def OAI.MicroscopicJamming.FiniteRank line 64
  5. def OAI.MicroscopicJamming.rankBirth line 69
  6. def OAI.MicroscopicJamming.rankLink line 72
  7. def OAI.MicroscopicJamming.rankInsert line 75
  8. def OAI.MicroscopicJamming.rankCluster line 80
  9. def OAI.MicroscopicJamming.RPCRankInsertionStatement line 83
  10. abbrev OAI.MicroscopicJamming.RankSeed line 101
  11. def OAI.MicroscopicJamming.rankInnovationLaw line 103
  12. def OAI.MicroscopicJamming.rankSeedLaw line 106
  13. def OAI.MicroscopicJamming.rankGrowing line 108
  14. def OAI.MicroscopicJamming.realizedRank line 112
  15. def OAI.MicroscopicJamming.realizedRankLaw line 116
  16. def OAI.MicroscopicJamming.RPCRankRealizationStatement line 118
  17. abbrev OAI.MicroscopicJamming.RowRankSignature line 136
  18. def OAI.MicroscopicJamming.cascadeGenealogySignature line 138
  19. def OAI.MicroscopicJamming.rankGenealogySignature line 141
  20. def OAI.MicroscopicJamming.rowSignatureCovariance line 144
  21. def OAI.MicroscopicJamming.RowRankGaussianStatement line 149
  22. def OAI.MicroscopicJamming.replicaClip line 166
  23. def OAI.MicroscopicJamming.replicaZ line 168
  24. def OAI.MicroscopicJamming.replicaNum line 172
  25. def OAI.MicroscopicJamming.ReplicaTruncationStatement line 178
  26. def OAI.MicroscopicJamming.gibbsZ line 212
  27. def OAI.MicroscopicJamming.gibbsMean line 213
  28. lemma OAI.MicroscopicJamming.integrable_exp_bounded line 216
  29. lemma OAI.MicroscopicJamming.gibbsZ_pos line 223
  30. lemma OAI.MicroscopicJamming.gibbsMean_eq_integral_tilted line 228
  31. lemma OAI.MicroscopicJamming.gibbsMean_const line 236
  32. lemma OAI.MicroscopicJamming.gibbsMean_abs_le line 242
  33. lemma OAI.MicroscopicJamming.integrable_gibbs_moment line 255
  34. lemma OAI.MicroscopicJamming.hasDerivAt_gibbs_moment line 266
  35. lemma OAI.MicroscopicJamming.hasDerivAt_gibbsZ line 305
  36. lemma OAI.MicroscopicJamming.hasDerivAt_log_gibbsZ line 314
  37. lemma OAI.MicroscopicJamming.hasDerivAt_gibbsMean line 327
  38. lemma OAI.MicroscopicJamming.continuous_gibbs_moment line 352
  39. lemma OAI.MicroscopicJamming.continuous_gibbsMean line 393
  40. lemma OAI.MicroscopicJamming.log_gibbsZ_abs_le line 417
  41. lemma OAI.MicroscopicJamming.gibbsMean_sq_le line 432
  42. def OAI.MicroscopicJamming.replicaPotential line 456
  43. lemma OAI.MicroscopicJamming.gibbsZ_replicas line 458
  44. lemma OAI.MicroscopicJamming.tilted_replicas line 465
  45. lemma OAI.MicroscopicJamming.gibbsMean_replicas_eq line 483
  46. lemma OAI.MicroscopicJamming.measurePreserving_snoc line 488
  47. lemma OAI.MicroscopicJamming.integral_replicas_mul_last line 495
  48. lemma OAI.MicroscopicJamming.integral_replicas_init line 510
  49. def OAI.MicroscopicJamming.replicaKernel line 527
  50. lemma OAI.MicroscopicJamming.measurable_replica_snoc line 531
  51. lemma OAI.MicroscopicJamming.replicaKernel_apply line 540
  52. instance OAI.MicroscopicJamming.(instance at line 552) line 552
  53. lemma OAI.MicroscopicJamming.measurable_replicaZ line 555
  54. lemma OAI.MicroscopicJamming.measurable_replicaNum line 559
  55. lemma OAI.MicroscopicJamming.measurable_replicaExpMoment line 572
  56. lemma OAI.MicroscopicJamming.pointCloud_position_preserving line 586
  57. lemma OAI.MicroscopicJamming.pointCloud_samebin_pair_preserving line 596
  58. lemma OAI.MicroscopicJamming.pointCloud_positions_ae line 610
  59. lemma OAI.MicroscopicJamming.pointCloud_samebin_distinct_ae line 618
  60. lemma OAI.MicroscopicJamming.cloudLabelPoint_injective_ae line 635