OAI/Probability/Honeycomb/FreeEnergy.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

Forced honeycomb walks and existence of their fixed-length free energy.

  1. structure OAI.HoneycombForce.Vertex line 13

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:13 (same declaration text).

  2. def OAI.HoneycombForce.up line 19

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:19 (same declaration text).

  3. def OAI.HoneycombForce.down line 20

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:21 (same declaration text).

  4. def OAI.HoneycombForce.UpDownAdj line 22
  5. def OAI.HoneycombForce.Adj line 28
  6. def OAI.HoneycombForce.rowSpacing line 30

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:23 (same declaration text).

  7. def OAI.HoneycombForce.position line 32

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:25 (same declaration text).

  8. def OAI.HoneycombForce.rho line 40

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:33 (same declaration text).

  9. def OAI.HoneycombForce.neighbors line 42

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:35 (same declaration text).

  10. def OAI.HoneycombForce.walkLists line 48

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:41 (same declaration text).

  11. def OAI.HoneycombForce.saws line 52

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:45 (same declaration text).

  12. def OAI.HoneycombForce.endpoint line 55

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:48 (same declaration text).

  13. def OAI.HoneycombForce.displacement line 57

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:50 (same declaration text).

  14. def OAI.HoneycombForce.projection line 60

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:53 (same declaration text).

  15. def OAI.HoneycombForce.z line 62
  16. def OAI.HoneycombForce.green line 64
  17. def OAI.HoneycombForce.susceptibility line 68
  18. def OAI.HoneycombForce.directionalSum line 71
  19. def OAI.HoneycombForce.radialSum line 75
  20. def OAI.HoneycombForce.directionalMass line 78
  21. def OAI.HoneycombForce.radialMass line 82
  22. def OAI.HoneycombForce.partition line 86

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:55 (same declaration text).

  23. def OAI.HoneycombForce.logPartition line 89

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:58 (same declaration text).

  24. def OAI.HoneycombForce.freeEnergy line 92

    Also declared: ComparatorChallenges/HoneycombFreeEnergy.lean:61 (same declaration text).

  25. def OAI.HoneycombForce.PowerAtZero line 95
  26. def OAI.HoneycombForce.UniformMassPowerAtZero line 99
  27. def OAI.HoneycombForce.UniformRealPowerAtZero line 105
  28. theorem OAI.HoneycombForce.mem_neighbors_iff line 110
  29. theorem OAI.HoneycombForce.mem_walkLists_iff line 116
  30. theorem OAI.HoneycombForce.mem_saws_iff line 153
  31. theorem OAI.HoneycombForce.saws_zero line 159
  32. theorem OAI.HoneycombForce.rho_pos line 162
  33. theorem OAI.HoneycombForce.rho_nonneg line 166
  34. theorem OAI.HoneycombForce.z_pos line 168
  35. theorem OAI.HoneycombForce.partition_nonneg line 170
  36. theorem OAI.HoneycombForce.partition_zero line 176
  37. theorem OAI.HoneycombForce.projection_le_norm line 180
  38. theorem OAI.HoneycombForce.directionalSum_le_radialSum line 186
  39. theorem OAI.HoneycombForce.radialMass_le_directionalMass line 196
  40. theorem OAI.HoneycombForce.directionalSum_zero line 202
  41. theorem OAI.HoneycombForce.radialSum_zero line 206
  42. theorem OAI.HoneycombForce.radialSum_mono line 210
  43. def OAI.HoneycombForce.shiftVertex line 218
  44. theorem OAI.HoneycombForce.shiftVertex_injective line 221
  45. theorem OAI.HoneycombForce.shiftVertex_adj line 230
  46. def OAI.HoneycombForce.rowVertex line 239
  47. theorem OAI.HoneycombForce.rowVertex_injective line 242
  48. theorem OAI.HoneycombForce.rowVertex_adj line 249
  49. def OAI.HoneycombForce.ray line 258
  50. theorem OAI.HoneycombForce.ray_zero line 261
  51. theorem OAI.HoneycombForce.ray_injective line 265
  52. theorem OAI.HoneycombForce.ray_adj line 269
  53. def OAI.HoneycombForce.rayPath line 274
  54. theorem OAI.HoneycombForce.rayPath_mem line 277
  55. theorem OAI.HoneycombForce.saws_nonempty line 289
  56. theorem OAI.HoneycombForce.partition_pos line 292
  57. theorem OAI.HoneycombForce.ennreal_tsum_finsetSum line 299
  58. theorem OAI.HoneycombForce.weighted_green_eq line 307
  59. theorem OAI.HoneycombForce.z_pow line 322
  60. theorem OAI.HoneycombForce.directionalSum_eq line 328
  61. theorem OAI.HoneycombForce.susceptibility_eq line 346
  62. theorem OAI.HoneycombForce.directionalSum_finite_of_logPartition_limit line 351
  63. theorem OAI.HoneycombForce.directionalSum_infinite_of_logPartition_limit line 374
  64. theorem OAI.HoneycombForce.shiftVertex_shift line 394
  65. theorem OAI.HoneycombForce.shiftVertex_zero line 399
  66. theorem OAI.HoneycombForce.position_shift line 403
  67. theorem OAI.HoneycombForce.displacement_shift line 409
  68. theorem OAI.HoneycombForce.mem_saws_shift line 415
  69. theorem OAI.HoneycombForce.saws_shift line 426
  70. theorem OAI.HoneycombForce.partition_shift line 438
  71. def OAI.HoneycombForce.baseVertex line 448
  72. theorem OAI.HoneycombForce.partition_eq_base line 450
  73. def OAI.HoneycombForce.splitWalk line 456
  74. theorem OAI.HoneycombForce.splitWalk_injective line 459
  75. theorem OAI.HoneycombForce.endpoint_take line 464
  76. theorem OAI.HoneycombForce.endpoint_drop line 468
  77. theorem OAI.HoneycombForce.splitWalk_mem line 474
  78. theorem OAI.HoneycombForce.displacement_split line 493
  79. theorem OAI.HoneycombForce.partition_split line 504
  80. def OAI.HoneycombForce.maxPartition line 536
  81. theorem OAI.HoneycombForce.partition_le_maxPartition line 539
  82. theorem OAI.HoneycombForce.maxPartition_pos line 546
  83. theorem OAI.HoneycombForce.maxPartition_zero line 549
  84. theorem OAI.HoneycombForce.partition_le_mul_maxPartition line 552
  85. theorem OAI.HoneycombForce.maxPartition_submultiplicative line 561
  86. theorem OAI.HoneycombForce.maxPartition_log_subadditive line 569
  87. theorem OAI.HoneycombForce.endpoint_one_type line 578
  88. theorem OAI.HoneycombForce.partition_succ_opposite line 587
  89. theorem OAI.HoneycombForce.maxPartition_succ_le line 598
  90. theorem OAI.HoneycombForce.endpoint_rayPath line 613
  91. theorem OAI.HoneycombForce.position_rowVertex line 619
  92. def OAI.HoneycombForce.rowCost line 631
  93. theorem OAI.HoneycombForce.rowPath_projection_lower line 634
  94. theorem OAI.HoneycombForce.maxPartition_log_linear_lower line 649
  95. theorem OAI.HoneycombForce.maxPartition_log_div_bddBelow line 671
  96. theorem OAI.HoneycombForce.exists_logPartition_limit line 682
  97. theorem OAI.HoneycombForce.logPartition_tendsto line 716

    Distinct definitions of this name: ComparatorChallenges/HoneycombFreeEnergy.lean:64 (same statement text; different proof or body). Qualify references as OAI.HoneycombForce.logPartition_tendsto@path.

  98. theorem OAI.HoneycombForce.directionalSum_finite_of_freeEnergy_lt line 720
  99. theorem OAI.HoneycombForce.directionalSum_infinite_of_lt_freeEnergy line 724
  100. theorem OAI.HoneycombForce.directionalSum_le_susceptibility_add line 728
  101. theorem OAI.HoneycombForce.directionalSum_finite_of_le line 751
  102. theorem OAI.HoneycombForce.freeEnergy_le_of_directionalSum_finite line 757
  103. theorem OAI.HoneycombForce.freeEnergy_le_of_lt_mass line 764
  104. theorem OAI.HoneycombForce.freeEnergy_ge_of_mass_lt line 773
  105. theorem OAI.HoneycombForce.susceptibility_finite_of_radialMass_pos line 782
  106. theorem OAI.HoneycombForce.freeEnergy_zero_le_of_radialMass_pos line 789
  107. theorem OAI.HoneycombForce.force_power_of_mass_powers line 794
  108. theorem OAI.HoneycombForce.upDownAdj_sq_norm line 852
  109. theorem OAI.HoneycombForce.norm_adj_le_one line 865
  110. theorem OAI.HoneycombForce.norm_displacement_one line 874
  111. theorem OAI.HoneycombForce.norm_displacement_le_length line 891
  112. theorem OAI.HoneycombForce.projection_abs_le_length line 909
  113. theorem OAI.HoneycombForce.partition_le_exp_mul line 917
  114. theorem OAI.HoneycombForce.freeEnergy_le_add_abs line 937
  115. theorem OAI.HoneycombForce.freeEnergy_zero_eq_of_mass_powers line 949