OAI/Probability/JammingConcavity/RowRefinementCovariance.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

Row Refinement Covariance.

  1. def OAI.MicroscopicJamming.rowMeshRanks line 57
  2. def OAI.MicroscopicJamming.rowMeshWeight line 60
  3. def OAI.MicroscopicJamming.rowMeshIncrement line 63
  4. def OAI.MicroscopicJamming.rowMeshTransport line 66
  5. lemma OAI.MicroscopicJamming.rowMeshRanks_sorted line 69
  6. lemma OAI.MicroscopicJamming.rowMeshRanks_mem line 72
  7. lemma OAI.MicroscopicJamming.rowGaussianBlocks_congr line 76
  8. lemma OAI.MicroscopicJamming.rowGaussianBlocks_getD line 88
  9. lemma OAI.MicroscopicJamming.rowGaussianBlocks_meshWeight line 97
  10. lemma OAI.MicroscopicJamming.rowMeshBlocks_filter line 106
  11. lemma OAI.MicroscopicJamming.rowGaussianBlocks_sum line 128
  12. lemma OAI.MicroscopicJamming.rowBlocks_sum_filter line 137
  13. lemma OAI.MicroscopicJamming.rowMesh_diagonal line 146
  14. lemma OAI.MicroscopicJamming.rowSorted_take_stepLevel line 158
  15. lemma OAI.MicroscopicJamming.rowMesh_transport line 173
  16. def OAI.MicroscopicJamming.rowTestExtend line 197
  17. def OAI.MicroscopicJamming.rowMeshTest line 200
  18. def OAI.MicroscopicJamming.rowFullRankView line 205
  19. def OAI.MicroscopicJamming.RowAllRankTestLawStatement line 211
  20. lemma OAI.MicroscopicJamming.probabilityMap_tendsto_of_ae line 237
  21. lemma OAI.MicroscopicJamming.rowTestExtend_continuous line 266
  22. lemma OAI.MicroscopicJamming.rowTestExtend_eq line 272
  23. lemma OAI.MicroscopicJamming.rowMesh_valid line 276
  24. lemma OAI.MicroscopicJamming.rowMeshTest_transport line 282
  25. lemma OAI.MicroscopicJamming.measurable_gaussianAdjunction_countable line 291
  26. lemma OAI.MicroscopicJamming.rowGaussianAdjunction_aemeasurable line 302
  27. lemma OAI.MicroscopicJamming.rowGaussianAdjunction_probability line 313
  28. lemma OAI.MicroscopicJamming.rowGaussianAdjunction_rank_mem line 321
  29. def OAI.MicroscopicJamming.rowMeshRankView line 332
  30. lemma OAI.MicroscopicJamming.measurable_rowFullRankView line 338
  31. lemma OAI.MicroscopicJamming.measurable_rowMeshRankView line 346
  32. lemma OAI.MicroscopicJamming.rowMesh_fields_exact line 358
  33. theorem OAI.MicroscopicJamming.rowAllRankTestLaw line 382
  34. lemma OAI.MicroscopicJamming.isClosed_matrix_nonneg line 412
  35. lemma OAI.MicroscopicJamming.measurable_matrix_sqrt line 426
  36. lemma OAI.MicroscopicJamming.continuous_matrix_clm line 438
  37. lemma OAI.MicroscopicJamming.measurable_matrix_gaussian_map line 442
  38. lemma OAI.MicroscopicJamming.matrix_gaussian_map_tendsto line 452
  39. lemma OAI.MicroscopicJamming.rowClosedProfile_integrable line 472
  40. lemma OAI.MicroscopicJamming.rowClosedProfile_eLpNorm_eq line 479
  41. lemma OAI.MicroscopicJamming.rowClosedProfile_tendstoInMeasure line 493
  42. lemma OAI.MicroscopicJamming.rowRankCovariance_tendsto_ae_of_profile_ae line 511
  43. def OAI.MicroscopicJamming.finiteSpinProfile line 538
  44. structure OAI.MicroscopicJamming.SphericalStepProfile line 541
  45. def OAI.MicroscopicJamming.SphericalStepProfile.val line 548
  46. def OAI.MicroscopicJamming.boundedSphericalProfiles line 551
  47. lemma OAI.MicroscopicJamming.finiteSpinProfile_monotone line 554
  48. lemma OAI.MicroscopicJamming.finiteSpinProfile_nonneg line 567
  49. def OAI.MicroscopicJamming.SphericalStepProfile.toProfile line 572
  50. lemma OAI.MicroscopicJamming.SphericalProfile.integrable line 577
  51. lemma OAI.MicroscopicJamming.SphericalStepProfile.integrable line 582
  52. lemma OAI.MicroscopicJamming.sphericalProfileDistance_nonneg line 585
  53. lemma OAI.MicroscopicJamming.sphericalProfileDistance_self line 591
  54. lemma OAI.MicroscopicJamming.sphericalProfileDistance_comm line 594
  55. lemma OAI.MicroscopicJamming.sphericalProfileDistance_triangle line 599
  56. def OAI.MicroscopicJamming.spinGridPoint line 618
  57. def OAI.MicroscopicJamming.spinGridRanks line 619
  58. lemma OAI.MicroscopicJamming.spinGridPoint_pos_denom line 621
  59. lemma OAI.MicroscopicJamming.spinGridPoint_mono line 622
  60. lemma OAI.MicroscopicJamming.spinGridPoint_mem line 625
  61. lemma OAI.MicroscopicJamming.spinGridPoint_zero line 630
  62. lemma OAI.MicroscopicJamming.spinGridPoint_last line 631
  63. lemma OAI.MicroscopicJamming.spinGridRanks_length line 633
  64. lemma OAI.MicroscopicJamming.spinGridRanks_get line 634
  65. lemma OAI.MicroscopicJamming.spinGridRanks_ordered line 637
  66. lemma OAI.MicroscopicJamming.spinGridRanks_mem line 644
  67. def OAI.MicroscopicJamming.SphericalProfile.gridStep line 653
  68. lemma OAI.MicroscopicJamming.gridStep_initial line 660
  69. lemma OAI.MicroscopicJamming.gridStep_variance line 662
  70. lemma OAI.MicroscopicJamming.sum_range_ite_lt_real line 668
  71. lemma OAI.MicroscopicJamming.gridStep_val_cell line 680