OAI/Probability/JammingConcavity/SpherePressure.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Sphere Pressure.

  1. def OAI.MicroscopicJamming.unitSphereLaw line 46
  2. instance OAI.MicroscopicJamming.unitSphereLaw_probability line 50
  3. lemma OAI.MicroscopicJamming.unitSphereLaw_cap line 56
  4. lemma OAI.MicroscopicJamming.surfaceLaw_as_map line 78
  5. lemma OAI.MicroscopicJamming.partition_rescale line 82
  6. def OAI.MicroscopicJamming.unitResidual line 92
  7. lemma OAI.MicroscopicJamming.unitEnergy_eq_half_norm_sq line 96
  8. lemma OAI.MicroscopicJamming.unitResidual_contract line 101
  9. lemma OAI.MicroscopicJamming.unitResidual_sq_le line 118
  10. lemma OAI.MicroscopicJamming.unitEnergy_sphere_lipschitz line 137
  11. def OAI.MicroscopicJamming.spherePartition line 167
  12. lemma OAI.MicroscopicJamming.continuous_sphere_integrand line 171
  13. lemma OAI.MicroscopicJamming.integrable_sphere_integrand line 177
  14. lemma OAI.MicroscopicJamming.spherePartition_bounds line 189
  15. lemma OAI.MicroscopicJamming.spherePartition_pos line 217
  16. lemma OAI.MicroscopicJamming.spherePartition_cap_lower line 221
  17. lemma OAI.MicroscopicJamming.log_spherePartition_bounds line 253
  18. abbrev OAI.MicroscopicJamming.UnitSpin line 283
  19. abbrev OAI.MicroscopicJamming.PerturbationIndex line 284
  20. def OAI.MicroscopicJamming.perturbationLaw line 285
  21. def OAI.MicroscopicJamming.coefficientLaw line 288
  22. instance OAI.MicroscopicJamming.coefficientLaw_probability line 289
  23. def OAI.MicroscopicJamming.coefficientProductLaw line 292
  24. def OAI.MicroscopicJamming.tensorField line 294
  25. def OAI.MicroscopicJamming.perturbation line 296
  26. def OAI.MicroscopicJamming.perturbedWeight line 301
  27. def OAI.MicroscopicJamming.perturbedPartition line 304
  28. def OAI.MicroscopicJamming.perturbedAverage line 309
  29. def OAI.MicroscopicJamming.unitOverlap line 317
  30. def OAI.MicroscopicJamming.replicaGram line 319
  31. def OAI.MicroscopicJamming.perturbationGGError line 323
  32. def OAI.MicroscopicJamming.ModelGGStatement line 336
  33. abbrev OAI.MicroscopicJamming.ModelOverlapArray line 353
  34. def OAI.MicroscopicJamming.perturbedSpinLaw line 355
  35. def OAI.MicroscopicJamming.infiniteReplicaGram line 360
  36. def OAI.MicroscopicJamming.perturbedArrayLaw line 363
  37. def OAI.MicroscopicJamming.ModelGGIdentities line 371
  38. def OAI.MicroscopicJamming.ModelArrayLimitStatement line 379
  39. def OAI.MicroscopicJamming.ArrayUltrametricityStatement line 403
  40. abbrev OAI.MicroscopicJamming.FiniteOverlapMatrix line 419
  41. def OAI.MicroscopicJamming.finiteArrayView line 421
  42. lemma OAI.MicroscopicJamming.measurable_finiteArrayView line 423
  43. lemma OAI.MicroscopicJamming.indicator_one_abs line 427
  44. lemma OAI.MicroscopicJamming.indicator_one_product line 431
  45. lemma OAI.MicroscopicJamming.indicator_one_preimage line 436
  46. lemma OAI.MicroscopicJamming.gg_avoid_one line 442
  47. def OAI.MicroscopicJamming.arrayFlatten line 495
  48. lemma OAI.MicroscopicJamming.measurable_arrayFlatten line 496
  49. def OAI.MicroscopicJamming.arrayUnflatten line 498
  50. lemma OAI.MicroscopicJamming.measurable_arrayUnflatten line 499
  51. lemma OAI.MicroscopicJamming.array_law_ext line 501
  52. def OAI.MicroscopicJamming.finiteRankCovariance line 543
  53. lemma OAI.MicroscopicJamming.measurable_finiteRankCovariance line 547
  54. lemma OAI.MicroscopicJamming.realizedRankLaw_finiteCovariance line 550
  55. lemma OAI.MicroscopicJamming.cascadeReplicaLaw_finiteCovariance line 563
  56. theorem OAI.MicroscopicJamming.realizedRankLaw_rpc line 575
  57. def OAI.MicroscopicJamming.RPCRankPositiveStatement line 596
  58. lemma OAI.MicroscopicJamming.block_indicator_psd line 609
  59. lemma OAI.MicroscopicJamming.integrable_rank_threshold line 649
  60. lemma OAI.MicroscopicJamming.integral_rank_threshold line 654
  61. lemma OAI.MicroscopicJamming.finite_ultrametric_psd line 668
  62. theorem OAI.MicroscopicJamming.rpcRankPositive line 700