OAI/Dynamics/StandardMap/LocalScarcity.lean

GitHub source file

535 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.StandardMapEntropy.Circle line 10

    Also declared: ComparatorChallenges/StandardMapComponents.lean:10 (same declaration text), ComparatorChallenges/StandardMapEntropy.lean:10 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:10 (same declaration text).

  2. abbrev OAI.StandardMapEntropy.Torus line 11

    Also declared: ComparatorChallenges/StandardMapComponents.lean:11 (same declaration text), ComparatorChallenges/StandardMapEntropy.lean:11 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:11 (same declaration text).

  3. lemma OAI.StandardMapEntropy.sine_periodic line 13

    Also declared: ComparatorChallenges/StandardMapComponents.lean:13 (same declaration text), ComparatorChallenges/StandardMapEntropy.lean:13 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:13 (same declaration text).

  4. def OAI.StandardMapEntropy.sine line 19

    Also declared: ComparatorChallenges/StandardMapComponents.lean:19 (same declaration text), ComparatorChallenges/StandardMapEntropy.lean:19 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:19 (same declaration text).

  5. def OAI.StandardMapEntropy.standardMap line 21

    Also declared: ComparatorChallenges/StandardMapComponents.lean:21 (same declaration text), ComparatorChallenges/StandardMapEntropy.lean:21 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:21 (same declaration text).

  6. def OAI.StandardMapEntropy.area line 24

    Distinct definitions of this name: ComparatorChallenges/StandardMapComponents.lean:24 (same statement text; different proof or body), ComparatorChallenges/StandardMapEntropy.lean:24 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:24 (same declaration text). Qualify references as OAI.StandardMapEntropy.area@path.

  7. def OAI.StandardMapEntropy.FinitePartition line 27

    Also declared: ComparatorChallenges/StandardMapEntropy.lean:27 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:27 (same declaration text).

  8. def OAI.StandardMapEntropy.blockAtom line 29

    Also declared: ComparatorChallenges/StandardMapEntropy.lean:29 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:29 (same declaration text).

  9. def OAI.StandardMapEntropy.blockEntropy line 33

    Also declared: ComparatorChallenges/StandardMapEntropy.lean:33 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:33 (same declaration text).

  10. def OAI.StandardMapEntropy.partitionEntropy line 38

    Also declared: ComparatorChallenges/StandardMapEntropy.lean:38 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:38 (same declaration text).

  11. def OAI.StandardMapEntropy.metricEntropy line 42

    Distinct definitions of this name: ComparatorChallenges/StandardMapEntropy.lean:42 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:42 (same statement text; different proof or body). Qualify references as OAI.StandardMapEntropy.metricEntropy@path.

  12. def OAI.StandardMapEntropy.MainObligation line 45

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

  13. lemma OAI.StandardMapEntropy.sine_coe line 48
  14. lemma OAI.StandardMapEntropy.continuous_sine line 51
  15. instance OAI.StandardMapEntropy.circleVolumeProbability line 57
  16. instance OAI.StandardMapEntropy.areaProbability line 62
  17. def OAI.StandardMapEntropy.kick line 66
  18. lemma OAI.StandardMapEntropy.continuous_kick line 68
  19. lemma OAI.StandardMapEntropy.continuous_standardMap line 71
  20. theorem OAI.StandardMapEntropy.measurePreserving_standardMap line 76
  21. def OAI.StandardMapEntropy.inverseMap line 91
  22. lemma OAI.StandardMapEntropy.standardMap_inverseMap line 94
  23. lemma OAI.StandardMapEntropy.inverseMap_standardMap line 100
  24. def OAI.StandardMapEntropy.recurrenceCoordinates line 112
  25. lemma OAI.StandardMapEntropy.recurrenceCoordinates_involutive line 114
  26. def OAI.StandardMapEntropy.recurrenceMap line 118
  27. lemma OAI.StandardMapEntropy.standardMap_conjugacy line 121
  28. def OAI.StandardMapEntropy.phi line 128
  29. def OAI.StandardMapEntropy.potential line 130
  30. lemma OAI.StandardMapEntropy.hasDerivAt_phi line 132
  31. def OAI.StandardMapEntropy.linearSolution line 142
  32. lemma OAI.StandardMapEntropy.linearSolution_zero line 147
  33. lemma OAI.StandardMapEntropy.linearSolution_one line 150
  34. lemma OAI.StandardMapEntropy.linearSolution_step line 153
  35. def OAI.StandardMapEntropy.tSolution line 157
  36. def OAI.StandardMapEntropy.sSolution line 159
  37. lemma OAI.StandardMapEntropy.linearSolution_decomposition line 161
  38. theorem OAI.StandardMapEntropy.solution_wronskian line 172
  39. def OAI.StandardMapEntropy.boundaryValue line 183
  40. lemma OAI.StandardMapEntropy.boundaryValue_vanishes line 186
  41. lemma OAI.StandardMapEntropy.boundaryValue_unique line 191
  42. lemma OAI.StandardMapEntropy.boundaryValue_increment line 197
  43. lemma OAI.StandardMapEntropy.initial_from_boundary line 208
  44. theorem OAI.StandardMapEntropy.boundary_expansion_exact line 216
  45. lemma OAI.StandardMapEntropy.boundary_denominator line 223
  46. def OAI.StandardMapEntropy.liftedOrbit line 231
  47. lemma OAI.StandardMapEntropy.liftedOrbit_zero line 236
  48. lemma OAI.StandardMapEntropy.liftedOrbit_one line 237
  49. lemma OAI.StandardMapEntropy.liftedOrbit_step line 238
  50. def OAI.StandardMapEntropy.orbitCoefficient line 242
  51. theorem OAI.StandardMapEntropy.hasDerivAt_liftedOrbit line 245
  52. lemma OAI.StandardMapEntropy.continuous_liftedOrbit line 256
  53. theorem OAI.StandardMapEntropy.hasDerivAt_plusOrbit line 260
  54. def OAI.StandardMapEntropy.dirichletSolution line 268
  55. def OAI.StandardMapEntropy.greenKernel line 271
  56. lemma OAI.StandardMapEntropy.dirichletSolution_zero line 274
  57. lemma OAI.StandardMapEntropy.dirichletSolution_boundary line 277
  58. lemma OAI.StandardMapEntropy.dirichletSolution_step line 280
  59. lemma OAI.StandardMapEntropy.dirichletSolution_right line 284
  60. lemma OAI.StandardMapEntropy.greenKernel_symm line 292
  61. lemma OAI.StandardMapEntropy.greenKernel_zero line 296
  62. lemma OAI.StandardMapEntropy.greenKernel_boundary line 299
  63. theorem OAI.StandardMapEntropy.greenKernel_jump line 303
  64. lemma OAI.StandardMapEntropy.quadratic_alternating_four line 337
  65. lemma OAI.StandardMapEntropy.affine_cosine_zeros line 362
  66. theorem OAI.StandardMapEntropy.alternating_cosine_obstruction line 373
  67. def OAI.StandardMapEntropy.drawdown line 400
  68. lemma OAI.StandardMapEntropy.drawdown_nonneg line 404
  69. lemma OAI.StandardMapEntropy.drawdown_ge_drop line 409
  70. lemma OAI.StandardMapEntropy.drawdown_pos_of_bad line 425
  71. lemma OAI.StandardMapEntropy.drawdown_step_account line 432
  72. lemma OAI.StandardMapEntropy.drawdown_account_sum line 451
  73. lemma OAI.StandardMapEntropy.drawdown_count line 462
  74. theorem OAI.StandardMapEntropy.shortfall_count line 478
  75. def OAI.StandardMapEntropy.goodExponent line 499
  76. def OAI.StandardMapEntropy.growthBase line 500
  77. def OAI.StandardMapEntropy.pairMagnitude line 501
  78. def OAI.StandardMapEntropy.pairLog line 503
  79. def OAI.StandardMapEntropy.GoodIndex line 506
  80. def OAI.StandardMapEntropy.CommonGood line 517
  81. def OAI.StandardMapEntropy.matchedScale line 523
  82. def OAI.StandardMapEntropy.MatchedLogs line 527
  83. def OAI.StandardMapEntropy.localSuccessfulSet line 531
  84. def OAI.StandardMapEntropy.LocalScarcityObligation line 535
  85. lemma OAI.StandardMapEntropy.goodExponent_pos line 542
  86. lemma OAI.StandardMapEntropy.goodExponent_lt_one line 543
  87. lemma OAI.StandardMapEntropy.pairMagnitude_nonneg line 545
  88. lemma OAI.StandardMapEntropy.pairMagnitude_zero line 548
  89. lemma OAI.StandardMapEntropy.pairMagnitude_normalized_pos line 556
  90. lemma OAI.StandardMapEntropy.pairMagnitude_t_pos line 566
  91. lemma OAI.StandardMapEntropy.logb_growth line 576
  92. lemma OAI.StandardMapEntropy.pairMagnitude_eq_abs_of_growth line 582
  93. lemma OAI.StandardMapEntropy.GoodIndex.t_dominant line 595
  94. lemma OAI.StandardMapEntropy.GoodIndex.t_ne_zero line 611
  95. lemma OAI.StandardMapEntropy.GoodIndex.t_next_dominant line 617
  96. lemma OAI.StandardMapEntropy.GoodIndex.t_growth line 627
  97. lemma OAI.StandardMapEntropy.GoodIndex.t_next_ne_zero line 635
  98. lemma OAI.StandardMapEntropy.GoodIndex.t_earlier line 641
  99. lemma OAI.StandardMapEntropy.pairMagnitude_eq_prev_of_decrease line 659
  100. lemma OAI.StandardMapEntropy.GoodIndex.u_dominant line 673
  101. lemma OAI.StandardMapEntropy.GoodIndex.u_next_dominant line 682
  102. lemma OAI.StandardMapEntropy.GoodIndex.u_decay line 692
  103. lemma OAI.StandardMapEntropy.GoodIndex.t_previous_growth line 713
  104. lemma OAI.StandardMapEntropy.goodScale_square line 730
  105. lemma OAI.StandardMapEntropy.GoodIndex.u_wronskian_bound line 737
  106. lemma OAI.StandardMapEntropy.GoodIndex.u_bound line 764
  107. theorem OAI.StandardMapEntropy.GoodIndex.boundary_expansion_error line 770
  108. lemma OAI.StandardMapEntropy.growthBase_ge_four line 801
  109. lemma OAI.StandardMapEntropy.potential_bound line 806
  110. lemma OAI.StandardMapEntropy.potential_lipschitz line 821
  111. lemma OAI.StandardMapEntropy.abs_sub_left_of_mem_uIcc line 843
  112. theorem OAI.StandardMapEntropy.phi_quadratic_error line 852
  113. def OAI.StandardMapEntropy.forcingResponse line 879
  114. def OAI.StandardMapEntropy.forcingBudget line 884
  115. lemma OAI.StandardMapEntropy.forcingBudget_nonneg line 888
  116. lemma OAI.StandardMapEntropy.forcingResponse_bound line 894
  117. lemma OAI.StandardMapEntropy.forcingBudget_sum line 928
  118. def OAI.StandardMapEntropy.orbitDisplacement line 943
  119. def OAI.StandardMapEntropy.orbitForcing line 946
  120. lemma OAI.StandardMapEntropy.orbitDisplacement_step line 950
  121. lemma OAI.StandardMapEntropy.orbitDisplacement_representation line 957
  122. lemma OAI.StandardMapEntropy.orbitForcing_bound line 968
  123. lemma OAI.StandardMapEntropy.orbitDisplacement_comparison line 973
  124. lemma OAI.StandardMapEntropy.forcing_bootstrap line 989
  125. lemma OAI.StandardMapEntropy.power_backward_weight line 1028
  126. lemma OAI.StandardMapEntropy.negative_power_good line 1033
  127. lemma OAI.StandardMapEntropy.GoodIndex.rescaled_linear_bound line 1042
  128. theorem OAI.StandardMapEntropy.GoodIndex.rescaled_displacement line 1066
  129. lemma OAI.StandardMapEntropy.tSolution_comparison line 1114
  130. theorem OAI.StandardMapEntropy.GoodIndex.rescaled_derivative line 1128
  131. lemma OAI.StandardMapEntropy.forcingBudget_weighted line 1189
  132. lemma OAI.StandardMapEntropy.eventually_rescaling_small line 1213
  133. lemma OAI.StandardMapEntropy.tSolution_comparison_error line 1232
  134. lemma OAI.StandardMapEntropy.GoodIndex.rescaled_variation_force_bound line 1242
  135. theorem OAI.StandardMapEntropy.GoodIndex.varied_t_lower line 1262
  136. def OAI.StandardMapEntropy.phiSecond line 1303
  137. lemma OAI.StandardMapEntropy.hasDerivAt_potential line 1305
  138. lemma OAI.StandardMapEntropy.phiSecond_bound line 1313
  139. def OAI.StandardMapEntropy.rescaledOrbit line 1322
  140. def OAI.StandardMapEntropy.rescaledD₁ line 1325
  141. def OAI.StandardMapEntropy.rescaledD₂ line 1328
  142. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledOrbit line 1332
  143. lemma OAI.StandardMapEntropy.rescaledD₁_step line 1339
  144. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledD₁ line 1346
  145. lemma OAI.StandardMapEntropy.GoodIndex.rescaled_second_bound line 1361
  146. lemma OAI.StandardMapEntropy.forcingBudget_weighted_pow line 1408
  147. def OAI.StandardMapEntropy.phiThird line 1431
  148. def OAI.StandardMapEntropy.phiFourth line 1432
  149. def OAI.StandardMapEntropy.phiFifth line 1433
  150. lemma OAI.StandardMapEntropy.hasDerivAt_phiSecond line 1435
  151. lemma OAI.StandardMapEntropy.hasDerivAt_phiThird line 1441
  152. lemma OAI.StandardMapEntropy.hasDerivAt_phiFourth line 1447
  153. def OAI.StandardMapEntropy.rescaledF₃ line 1453
  154. def OAI.StandardMapEntropy.rescaledD₃ line 1456
  155. lemma OAI.StandardMapEntropy.rescaledD₂_step line 1459
  156. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledD₂ line 1465
  157. def OAI.StandardMapEntropy.rescaledF₄ line 1482
  158. def OAI.StandardMapEntropy.rescaledD₄ line 1487
  159. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledD₃ line 1490
  160. def OAI.StandardMapEntropy.rescaledF₅ line 1510
  161. def OAI.StandardMapEntropy.rescaledD₅ line 1517
  162. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledD₄ line 1520
  163. def OAI.StandardMapEntropy.derivativeMajorant line 1543
  164. lemma OAI.StandardMapEntropy.derivativeMajorant_pos line 1545
  165. lemma OAI.StandardMapEntropy.trig_amplitude_bound line 1547
  166. lemma OAI.StandardMapEntropy.uniform_phiSecond_bound line 1564
  167. lemma OAI.StandardMapEntropy.uniform_phiThird_bound line 1568
  168. lemma OAI.StandardMapEntropy.uniform_phiFourth_bound line 1572
  169. lemma OAI.StandardMapEntropy.uniform_phiFifth_bound line 1576
  170. lemma OAI.StandardMapEntropy.bell₃_bound line 1581
  171. lemma OAI.StandardMapEntropy.bell₄_bound line 1592
  172. lemma OAI.StandardMapEntropy.bell₅_bound line 1606
  173. lemma OAI.StandardMapEntropy.forcingResponse_fixed_order line 1624
  174. lemma OAI.StandardMapEntropy.fixed_order_coarse line 1648
  175. lemma OAI.StandardMapEntropy.rescaling_ratio_bounds line 1652
  176. def OAI.StandardMapEntropy.HigherControl line 1658
  177. lemma OAI.StandardMapEntropy.HigherControl.base_small line 1662
  178. lemma OAI.StandardMapEntropy.eventually_scalar_rescaling_small line 1668
  179. lemma OAI.StandardMapEntropy.tendsto_growthBase line 1683
  180. lemma OAI.StandardMapEntropy.eventually_HigherControl line 1688
  181. theorem OAI.StandardMapEntropy.GoodIndex.rescaled_high_bounds line 1698
  182. lemma OAI.StandardMapEntropy.recurrence_pair_backward_step line 1781
  183. lemma OAI.StandardMapEntropy.recurrence_pair_backward line 1799
  184. lemma OAI.StandardMapEntropy.dirichletSolution_backward_bound line 1817
  185. lemma OAI.StandardMapEntropy.GoodIndex.varied_dirichlet_bound line 1832
  186. lemma OAI.StandardMapEntropy.GoodIndex.varied_green_bound line 1851
  187. lemma OAI.StandardMapEntropy.hasDerivAt_ringInverse_comp line 1881
  188. def OAI.StandardMapEntropy.inverseJet₁ line 1891
  189. def OAI.StandardMapEntropy.inverseJet₂ line 1892
  190. def OAI.StandardMapEntropy.inverseJet₃ line 1895
  191. def OAI.StandardMapEntropy.inverseJet₄ line 1899
  192. lemma OAI.StandardMapEntropy.hasDerivAt_inverseJet₁ line 1908
  193. lemma OAI.StandardMapEntropy.hasDerivAt_inverseJet₂ line 1918
  194. lemma OAI.StandardMapEntropy.hasDerivAt_inverseJet₃ line 1929
  195. lemma OAI.StandardMapEntropy.path_variation_lower line 1944
  196. lemma OAI.StandardMapEntropy.path_max_sum_bound line 1964
  197. lemma OAI.StandardMapEntropy.inverse_chain_exponent line 1979
  198. def OAI.StandardMapEntropy.dirichletMatrix line 2018
  199. def OAI.StandardMapEntropy.greenMatrix line 2022
  200. lemma OAI.StandardMapEntropy.sum_fin_predecessor line 2025
  201. lemma OAI.StandardMapEntropy.sum_fin_successor line 2043
  202. theorem OAI.StandardMapEntropy.dirichletMatrix_mul_greenMatrix line 2063
  203. lemma OAI.StandardMapEntropy.dirichletMatrix_isUnit line 2076
  204. theorem OAI.StandardMapEntropy.dirichletMatrix_inverse line 2080
  205. def OAI.StandardMapEntropy.rescaledV₁ line 2085
  206. def OAI.StandardMapEntropy.rescaledV₂ line 2087
  207. def OAI.StandardMapEntropy.rescaledV₃ line 2090
  208. def OAI.StandardMapEntropy.rescaledV₄ line 2094
  209. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledPotential line 2101
  210. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledV₁ line 2105
  211. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledV₂ line 2112
  212. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledV₃ line 2123
  213. lemma OAI.StandardMapEntropy.GoodIndex.rescaled_coarse_high_bounds line 2137
  214. lemma OAI.StandardMapEntropy.potential_bell_bounds line 2160
  215. theorem OAI.StandardMapEntropy.GoodIndex.rescaled_potential_bounds line 2192
  216. def OAI.StandardMapEntropy.matrixEntryCLM line 2220
  217. lemma OAI.StandardMapEntropy.hasDerivAt_matrix_diagonal line 2227
  218. lemma OAI.StandardMapEntropy.hasDerivAt_dirichletMatrix line 2238
  219. def OAI.StandardMapEntropy.rescaledMatrix line 2249
  220. def OAI.StandardMapEntropy.rescaledDiagonal line 2252
  221. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledMatrix line 2256
  222. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledDiagonal₁ line 2263
  223. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledDiagonal₂ line 2270
  224. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledDiagonal₃ line 2277
  225. def OAI.StandardMapEntropy.rescaledInverse line 2285
  226. def OAI.StandardMapEntropy.rescaledInverse₁ line 2287
  227. def OAI.StandardMapEntropy.rescaledInverse₂ line 2289
  228. def OAI.StandardMapEntropy.rescaledInverse₃ line 2292
  229. def OAI.StandardMapEntropy.rescaledInverse₄ line 2295
  230. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledInverse line 2300
  231. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledInverse₁ line 2306
  232. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledInverse₂ line 2315
  233. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledInverse₃ line 2325
  234. theorem OAI.StandardMapEntropy.rescaledInverse_eq_greenMatrix line 2338
  235. lemma OAI.StandardMapEntropy.geometric_positive_tail line 2343
  236. lemma OAI.StandardMapEntropy.weighted_geometric_sites line 2351
  237. lemma OAI.StandardMapEntropy.inverse_chain_site_sum line 2372
  238. lemma OAI.StandardMapEntropy.prod_const_rpow line 2383
  239. lemma OAI.StandardMapEntropy.scalar_inverse_chain_bound line 2388
  240. def OAI.StandardMapEntropy.finTotal line 2453
  241. lemma OAI.StandardMapEntropy.finTotal_coe line 2455
  242. lemma OAI.StandardMapEntropy.finTotal_sum line 2457
  243. lemma OAI.StandardMapEntropy.finTotal_prod line 2461
  244. lemma OAI.StandardMapEntropy.finite_inverse_chain_bound line 2466
  245. lemma OAI.StandardMapEntropy.inverse_chain_rpow_factor line 2492
  246. def OAI.StandardMapEntropy.boundaryChain line 2508
  247. lemma OAI.StandardMapEntropy.fourth_chain_sum_bound line 2514
  248. lemma OAI.StandardMapEntropy.sum_fin_functions_cons line 2573
  249. def OAI.StandardMapEntropy.matrixChain line 2580
  250. def OAI.StandardMapEntropy.matrixPath line 2585
  251. lemma OAI.StandardMapEntropy.matrixPath_cons line 2591
  252. lemma OAI.StandardMapEntropy.matrixChain_entry line 2614
  253. lemma OAI.StandardMapEntropy.matrixChain_boundary line 2636
  254. lemma OAI.StandardMapEntropy.fourth_chain_entry_bound line 2645
  255. lemma OAI.StandardMapEntropy.inverseJet₄_chains line 2661
  256. def OAI.StandardMapEntropy.inverseFourthMajorant line 2674
  257. lemma OAI.StandardMapEntropy.absolute_polynomial_bound line 2677
  258. lemma OAI.StandardMapEntropy.inverseJet₄_boundary_bound line 2701
  259. lemma OAI.StandardMapEntropy.decay_nat_power line 2747
  260. lemma OAI.StandardMapEntropy.potential_power_identity line 2752
  261. lemma OAI.StandardMapEntropy.natural_distance_power line 2757
  262. lemma OAI.StandardMapEntropy.successive_distance_power line 2761
  263. lemma OAI.StandardMapEntropy.green_power_identity line 2765
  264. lemma OAI.StandardMapEntropy.GoodIndex.varied_dirichlet_real_bound line 2788
  265. lemma OAI.StandardMapEntropy.GoodIndex.varied_green_real_bound line 2800
  266. def OAI.StandardMapEntropy.rescaledPotentialJets line 2815
  267. lemma OAI.StandardMapEntropy.inflate_potential_bound line 2821
  268. lemma OAI.StandardMapEntropy.GoodIndex.rescaled_potential_real_bound line 2830
  269. lemma OAI.StandardMapEntropy.greenMatrix_first_row line 2857
  270. lemma OAI.StandardMapEntropy.greenMatrix_first_col line 2863
  271. theorem OAI.StandardMapEntropy.GoodIndex.rescaled_inverse_fourth_bound line 2869
  272. lemma OAI.StandardMapEntropy.continuous_linearSolution line 2894
  273. lemma OAI.StandardMapEntropy.continuous_orbitCoefficient line 2901
  274. lemma OAI.StandardMapEntropy.continuous_rescaled_tSolution line 2906
  275. lemma OAI.StandardMapEntropy.iteratedDeriv_of_jets line 2911
  276. lemma OAI.StandardMapEntropy.hasDerivAt_matrix_entry line 2926
  277. lemma OAI.StandardMapEntropy.iteratedDeriv_rescaledInverse_entry line 2931
  278. lemma OAI.StandardMapEntropy.rescaledInverse_boundary line 2952
  279. lemma OAI.StandardMapEntropy.iteratedDeriv_boundaryValue line 2959
  280. theorem OAI.StandardMapEntropy.GoodIndex.boundary_fourth_bound line 2971
  281. lemma OAI.StandardMapEntropy.eventually_chain_ratio_small line 2998
  282. theorem OAI.StandardMapEntropy.eventually_boundary_fourth_bound line 3003
  283. def OAI.StandardMapEntropy.scalarReciprocalJet line 3017
  284. def OAI.StandardMapEntropy.scalarProductJet line 3024
  285. lemma OAI.StandardMapEntropy.hasDerivAt_scalarReciprocalJet line 3031
  286. lemma OAI.StandardMapEntropy.hasDerivAt_scalarProductJet line 3046
  287. lemma OAI.StandardMapEntropy.scalarReciprocalJet_bound line 3070
  288. lemma OAI.StandardMapEntropy.scalarProductJet_bound line 3123
  289. def OAI.StandardMapEntropy.rescaledTJet line 3156
  290. lemma OAI.StandardMapEntropy.hasDerivAt_rescaledTJet line 3163
  291. lemma OAI.StandardMapEntropy.GoodIndex.rescaledTJet_bound line 3171
  292. lemma OAI.StandardMapEntropy.GoodIndex.rescaledD₁_terminal_lower line 3202
  293. def OAI.StandardMapEntropy.terminalQuotient line 3212
  294. lemma OAI.StandardMapEntropy.terminalQuotient_eq line 3216
  295. lemma OAI.StandardMapEntropy.iteratedDeriv_terminalQuotient line 3222
  296. theorem OAI.StandardMapEntropy.GoodIndex.quotient_derivatives line 3244
  297. lemma OAI.StandardMapEntropy.analytic_zeros_finite line 3271
  298. lemma OAI.StandardMapEntropy.analytic_eq_of_positive_measure line 3283
  299. lemma OAI.StandardMapEntropy.analytic_affine_cosine line 3296
  300. lemma OAI.StandardMapEntropy.analytic_affine_sine line 3302
  301. lemma OAI.StandardMapEntropy.polynomial_secant_obstruction line 3308
  302. lemma OAI.StandardMapEntropy.polynomial_secant_equality_null line 3318
  303. lemma OAI.StandardMapEntropy.polynomial_reciprocal_affine_obstruction line 3327
  304. lemma OAI.StandardMapEntropy.cosine_zero_sine_nonzero line 3335
  305. lemma OAI.StandardMapEntropy.cosine_root_spacing line 3342
  306. lemma OAI.StandardMapEntropy.cosine_roots_same_frequency line 3362
  307. lemma OAI.StandardMapEntropy.two_secants_polynomial_limit line 3388
  308. def OAI.StandardMapEntropy.oppositeLimitDifference line 3438
  309. lemma OAI.StandardMapEntropy.oppositeLimitDifference_analytic line 3443
  310. lemma OAI.StandardMapEntropy.opposite_limit_obstruction line 3455
  311. theorem OAI.StandardMapEntropy.opposite_limit_equality_null line 3471
  312. lemma OAI.StandardMapEntropy.polynomial_quartic_obstruction line 3477
  313. lemma OAI.StandardMapEntropy.polynomial_quartic_equality_null line 3484
  314. def OAI.StandardMapEntropy.taylorPolynomialAtZero line 3492
  315. lemma OAI.StandardMapEntropy.taylorPolynomialAtZero_eval line 3495
  316. lemma OAI.StandardMapEntropy.taylorPolynomialAtZero_degree line 3500
  317. lemma OAI.StandardMapEntropy.taylorPolynomialAtZero_eval_eq line 3506
  318. lemma OAI.StandardMapEntropy.taylorPolynomialAtZero_eval_zero line 3518
  319. lemma OAI.StandardMapEntropy.analytic_taylor_remainder_bound line 3526
  320. lemma OAI.StandardMapEntropy.analytic_liftedOrbit line 3548
  321. lemma OAI.StandardMapEntropy.analytic_orbitCoefficient line 3559
  322. lemma OAI.StandardMapEntropy.analytic_linearSolution line 3565
  323. lemma OAI.StandardMapEntropy.analytic_rescaledOrbit line 3573
  324. lemma OAI.StandardMapEntropy.analyticAt_boundaryValue line 3579
  325. lemma OAI.StandardMapEntropy.iteratedDeriv_rescaledOrbit line 3589
  326. lemma OAI.StandardMapEntropy.GoodIndex.boundary_taylor_bound line 3604
  327. lemma OAI.StandardMapEntropy.vandermonde_continuous line 3649
  328. lemma OAI.StandardMapEntropy.coefficients_tendsto_of_values line 3654
  329. def OAI.StandardMapEntropy.coefficientPolynomial line 3682
  330. lemma OAI.StandardMapEntropy.coefficientPolynomial_eval line 3685
  331. lemma OAI.StandardMapEntropy.coefficientPolynomial_reconstruct line 3689
  332. lemma OAI.StandardMapEntropy.coefficientPolynomial_degree line 3697
  333. lemma OAI.StandardMapEntropy.coefficientPolynomial_vandermonde line 3703
  334. lemma OAI.StandardMapEntropy.continuous_coefficientPolynomial_eval line 3709
  335. lemma OAI.StandardMapEntropy.polynomial_extraction line 3714
  336. lemma OAI.StandardMapEntropy.compact_sets_subsequence line 3753
  337. lemma OAI.StandardMapEntropy.neighborhoods_null_limit line 3760
  338. lemma OAI.StandardMapEntropy.successful_points_approximation line 3784
  339. lemma OAI.StandardMapEntropy.CommonGood.scale_pos line 3814
  340. lemma OAI.StandardMapEntropy.CommonGood.boundary_sum_error line 3821
  341. lemma OAI.StandardMapEntropy.matched_log_ratio line 3847
  342. lemma OAI.StandardMapEntropy.CommonGood.scale_ratio line 3857
  343. lemma OAI.StandardMapEntropy.cubic_scale_remainder line 3870
  344. def OAI.StandardMapEntropy.scaledTaylorPolynomial line 3889
  345. lemma OAI.StandardMapEntropy.scaledTaylorPolynomial_degree line 3892
  346. lemma OAI.StandardMapEntropy.scaledTaylorPolynomial_eval line 3899
  347. lemma OAI.StandardMapEntropy.GoodIndex.scaled_boundary_taylor_bound line 3903
  348. lemma OAI.StandardMapEntropy.potential_reciprocal_identity line 3923
  349. lemma OAI.StandardMapEntropy.CommonGood.cubic_boundary_bound line 3937
  350. lemma OAI.StandardMapEntropy.scaled_positive_reciprocal_bound line 4004
  351. lemma OAI.StandardMapEntropy.fourth_error_power line 4020
  352. lemma OAI.StandardMapEntropy.matched_error_power line 4025
  353. lemma OAI.StandardMapEntropy.CommonGood.cubic_successful_bound line 4034
  354. def OAI.StandardMapEntropy.localReciprocalTerm line 4150
  355. lemma OAI.StandardMapEntropy.localReciprocalTerm_eq line 4155
  356. theorem OAI.StandardMapEntropy.CommonGood.cubic_reciprocal_relation line 4168
  357. lemma OAI.StandardMapEntropy.tendsto_cubic_relation_error line 4192
  358. theorem OAI.StandardMapEntropy.eventually_cubic_reciprocal_relation line 4200
  359. lemma OAI.StandardMapEntropy.HasStrictDerivAt.moving_quotient_limit line 4213
  360. lemma OAI.StandardMapEntropy.tendsto_product_difference_quotient line 4234
  361. lemma OAI.StandardMapEntropy.opposite_reciprocal_limit line 4245
  362. lemma OAI.StandardMapEntropy.analytic_quartic_remainder_bound line 4314
  363. lemma OAI.StandardMapEntropy.tendsto_quartic_remainder_ratio line 4340
  364. lemma OAI.StandardMapEntropy.reciprocal_fourth_normalized line 4370
  365. lemma OAI.StandardMapEntropy.tendsto_reciprocal_fourth_normalized line 4382
  366. lemma OAI.StandardMapEntropy.rescaledOrbit_change_scale line 4402
  367. lemma OAI.StandardMapEntropy.iteratedDeriv_rescaledOrbit_change_scale line 4408
  368. lemma OAI.StandardMapEntropy.GoodIndex.terminal_derivative_bound line 4418
  369. lemma OAI.StandardMapEntropy.scaled_rpow_bound line 4435
  370. lemma OAI.StandardMapEntropy.GoodIndex.matched_phase_derivative_bound line 4445
  371. lemma OAI.StandardMapEntropy.taylorPolynomialAtZero_two_eval line 4469
  372. lemma OAI.StandardMapEntropy.taylorPolynomialAtZero_one_eval line 4475
  373. lemma OAI.StandardMapEntropy.analytic_quadratic_taylor_C1 line 4480
  374. lemma OAI.StandardMapEntropy.GoodIndex.matched_phase_quadratic_C1 line 4500
  375. lemma OAI.StandardMapEntropy.GoodIndex.matched_phase_initial_derivative line 4521
  376. lemma OAI.StandardMapEntropy.GoodIndex.matched_phase_curvature_bound line 4527
  377. lemma OAI.StandardMapEntropy.iteratedDeriv_comp_scale line 4535
  378. lemma OAI.StandardMapEntropy.terminalQuotient_change_scale line 4547
  379. lemma OAI.StandardMapEntropy.iteratedDeriv_terminalQuotient_change_scale line 4553
  380. lemma OAI.StandardMapEntropy.GoodIndex.matched_quotient_derivative_bound line 4564
  381. lemma OAI.StandardMapEntropy.analyticAt_terminalQuotient line 4586
  382. lemma OAI.StandardMapEntropy.GoodIndex.analytic_matched_quotient line 4596
  383. lemma OAI.StandardMapEntropy.CommonGood.cubic_successful_bound_ratio line 4614
  384. theorem OAI.StandardMapEntropy.CommonGood.cubic_reciprocal_relation_ratio line 4737
  385. lemma OAI.StandardMapEntropy.polynomial_extraction_analytic_ratio line 4764
  386. lemma OAI.StandardMapEntropy.successful_polynomial_values_tendsto line 4798
  387. lemma OAI.StandardMapEntropy.secant_quartic_limit_null line 4811
  388. lemma OAI.StandardMapEntropy.affine_reciprocal_limit_null line 4846
  389. lemma OAI.StandardMapEntropy.quartic_limit_null line 4866
  390. lemma OAI.StandardMapEntropy.iteratedDeriv_product_bound line 4882
  391. lemma OAI.StandardMapEntropy.iteratedDeriv_product_bound_four line 4909
  392. lemma OAI.StandardMapEntropy.GoodIndex.terminal_coarse_derivative_bound line 4922
  393. lemma OAI.StandardMapEntropy.GoodIndex.matched_phase_coarse_derivative_bound line 4934
  394. def OAI.StandardMapEntropy.rescaledPotentialJet line 4961
  395. lemma OAI.StandardMapEntropy.iteratedDeriv_rescaledPotential line 4968
  396. lemma OAI.StandardMapEntropy.analytic_rescaledPotential line 4979
  397. lemma OAI.StandardMapEntropy.GoodIndex.terminal_potential_derivative_bound line 4986
  398. lemma OAI.StandardMapEntropy.GoodIndex.matched_potential_derivative_bound line 5009
  399. def OAI.StandardMapEntropy.normalizedSlope line 5036
  400. def OAI.StandardMapEntropy.shiftedCosine line 5039
  401. def OAI.StandardMapEntropy.slowDenominator line 5042
  402. lemma OAI.StandardMapEntropy.shiftedCosine_eq line 5045
  403. lemma OAI.StandardMapEntropy.analytic_normalizedSlope line 5052
  404. lemma OAI.StandardMapEntropy.GoodIndex.normalizedSlope_derivative_bound line 5056
  405. lemma OAI.StandardMapEntropy.GoodIndex.analytic_shiftedCosine line 5073
  406. lemma OAI.StandardMapEntropy.GoodIndex.shiftedCosine_derivative_bound line 5080
  407. lemma OAI.StandardMapEntropy.GoodIndex.slowDenominator_derivative_bound line 5118
  408. def OAI.StandardMapEntropy.slowDenominatorModel line 5147
  409. lemma OAI.StandardMapEntropy.hasDerivAt_slowDenominatorModel line 5150
  410. lemma OAI.StandardMapEntropy.slowDenominatorModel_value line 5160
  411. lemma OAI.StandardMapEntropy.abs_sin_close_one line 5168
  412. lemma OAI.StandardMapEntropy.slowDenominatorModel_slope_bound line 5174
  413. lemma OAI.StandardMapEntropy.tendsto_slow_nonzero_slope line 5222
  414. lemma OAI.StandardMapEntropy.coefficients_tendsto_of_values_filter line 5259
  415. lemma OAI.StandardMapEntropy.polynomial_extraction_filter line 5287
  416. lemma OAI.StandardMapEntropy.HasStrictDerivAt.moving_quotient_limit_filter line 5327
  417. lemma OAI.StandardMapEntropy.tendsto_product_difference_quotient_filter line 5349
  418. lemma OAI.StandardMapEntropy.opposite_reciprocal_limit_filter line 5361
  419. lemma OAI.StandardMapEntropy.tendsto_quartic_remainder_ratio_filter line 5431
  420. lemma OAI.StandardMapEntropy.tendsto_reciprocal_fourth_normalized_filter line 5462
  421. lemma OAI.StandardMapEntropy.polynomial_extraction_analytic_ratio_filter line 5482
  422. lemma OAI.StandardMapEntropy.successful_polynomial_values_tendsto_filter line 5517
  423. lemma OAI.StandardMapEntropy.secant_quartic_limit_null_filter line 5530
  424. lemma OAI.StandardMapEntropy.affine_reciprocal_limit_null_filter line 5565
  425. lemma OAI.StandardMapEntropy.quartic_limit_null_filter line 5585
  426. lemma OAI.StandardMapEntropy.analyticAt_iteratedDeriv line 5601
  427. lemma OAI.StandardMapEntropy.analytic_derivative_variation line 5607
  428. lemma OAI.StandardMapEntropy.analytic_cubic_lagrange line 5620
  429. lemma OAI.StandardMapEntropy.tendsto_cubic_remainder_of_fourth line 5639
  430. lemma OAI.StandardMapEntropy.analytic_iteratedDeriv_inverse line 5671
  431. lemma OAI.StandardMapEntropy.analytic_reciprocal_fourth line 5690
  432. lemma OAI.StandardMapEntropy.ultrafilter_bounded_limit line 5705
  433. lemma OAI.StandardMapEntropy.polynomial_extraction_analytic_ratio_avoiding line 5714
  434. lemma OAI.StandardMapEntropy.affine_reciprocal_limit_null_avoiding line 5757
  435. lemma OAI.StandardMapEntropy.quartic_limit_null_avoiding line 5778
  436. lemma OAI.StandardMapEntropy.ultrafilter_scaled_limit line 5795
  437. lemma OAI.StandardMapEntropy.ultrafilter_real_alternative line 5805
  438. lemma OAI.StandardMapEntropy.reciprocal_fourth_scaled_identity line 5825
  439. lemma OAI.StandardMapEntropy.slow_reciprocal_fourth_vanishes line 5836
  440. lemma OAI.StandardMapEntropy.slow_no_zeros line 5872
  441. lemma OAI.StandardMapEntropy.slow_relative_value line 5892
  442. lemma OAI.StandardMapEntropy.slow_relative_fourth line 5917
  443. lemma OAI.StandardMapEntropy.analytic_affine_cosine_nonzero line 5994
  444. lemma OAI.StandardMapEntropy.cubic_fast_quartic_null line 6000
  445. lemma OAI.StandardMapEntropy.cubic_pure_quartic_null line 6028
  446. lemma OAI.StandardMapEntropy.slow_almost_constant_scarcity line 6073
  447. lemma OAI.StandardMapEntropy.analytic_linear_remainder_bound line 6158
  448. lemma OAI.StandardMapEntropy.slow_affine_limit line 6176
  449. lemma OAI.StandardMapEntropy.slow_affine_scarcity line 6238
  450. lemma OAI.StandardMapEntropy.vanishing_slope_scarcity line 6287
  451. lemma OAI.StandardMapEntropy.two_secants_affine_polynomial_limit line 6344
  452. lemma OAI.StandardMapEntropy.analytic_cosine_product_nonzero line 6381
  453. lemma OAI.StandardMapEntropy.two_secants_limit_classification line 6407
  454. lemma OAI.StandardMapEntropy.opposite_cubic_scarcity line 6444
  455. def OAI.StandardMapEntropy.coefficientScale line 6515
  456. lemma OAI.StandardMapEntropy.coefficientScale_bounds line 6518
  457. lemma OAI.StandardMapEntropy.coefficientScale_tendsto line 6527
  458. lemma OAI.StandardMapEntropy.coefficientScale_extract line 6534
  459. lemma OAI.StandardMapEntropy.error_tendsto_div_larger line 6568
  460. lemma OAI.StandardMapEntropy.quadratic_normalization_limit line 6577
  461. lemma OAI.StandardMapEntropy.phase_moving_limit line 6636
  462. def OAI.StandardMapEntropy.centerPhase line 6660
  463. lemma OAI.StandardMapEntropy.centerPhase_zero_bounds line 6662
  464. lemma OAI.StandardMapEntropy.centerPhase_cos line 6667
  465. lemma OAI.StandardMapEntropy.analytic_centerPhase line 6673
  466. lemma OAI.StandardMapEntropy.centerPhase_iteratedDeriv line 6676
  467. lemma OAI.StandardMapEntropy.opposite_phase_change line 6685
  468. def OAI.StandardMapEntropy.phaseReciprocal line 6698
  469. lemma OAI.StandardMapEntropy.phaseReciprocal_tendsto line 6701
  470. lemma OAI.StandardMapEntropy.positive_slope_scarcity line 6716
  471. structure OAI.StandardMapEntropy.RescaledPath line 6846
  472. def OAI.StandardMapEntropy.RescaledPath.size line 6855
  473. def OAI.StandardMapEntropy.RescaledPath.ratio line 6856
  474. def OAI.StandardMapEntropy.RescaledPath.phase line 6857
  475. def OAI.StandardMapEntropy.RescaledPath.quotient line 6859
  476. def OAI.StandardMapEntropy.RescaledPath.denominator line 6861
  477. def OAI.StandardMapEntropy.RescaledPath.Admissible line 6864
  478. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.size_pos line 6868
  479. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.scale_pos line 6871
  480. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.ratio_bounds line 6872
  481. lemma OAI.StandardMapEntropy.RescaledPath.phase_iteratedDeriv line 6874
  482. lemma OAI.StandardMapEntropy.RescaledPath.analytic_phase line 6879
  483. lemma OAI.StandardMapEntropy.RescaledPath.phase_zero_bounds line 6882
  484. lemma OAI.StandardMapEntropy.RescaledPath.phase_deriv_zero line 6883
  485. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.abs_phase_deriv_zero line 6888
  486. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.phase_derivative_bound line 6892
  487. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.phase_derivative_bound_coarse line 6900
  488. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.analytic_quotient line 6912
  489. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.quotient_derivative_bound line 6919
  490. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.denominator_model line 6927
  491. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.analytic_denominator line 6938
  492. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.denominator_derivative_bound line 6945
  493. lemma OAI.StandardMapEntropy.power_times_parameter_tendsto line 6956
  494. lemma OAI.StandardMapEntropy.RescaledPath.parameter_inverse_tendsto line 6975
  495. lemma OAI.StandardMapEntropy.RescaledPath.curvature_bound_tendsto line 6978
  496. lemma OAI.StandardMapEntropy.RescaledPath.quotient_bound_tendsto line 6984
  497. lemma OAI.StandardMapEntropy.RescaledPath.quotient_moving_tendsto line 6987
  498. lemma OAI.StandardMapEntropy.RescaledPath.phase_moving_tendsto line 6994
  499. lemma OAI.StandardMapEntropy.RescaledPath.curvature_tendsto line 7009
  500. lemma OAI.StandardMapEntropy.RescaledPath.scaled_curvature_tendsto line 7015
  501. lemma OAI.StandardMapEntropy.RescaledPath.scaled_quotient_derivative_tendsto line 7026
  502. lemma OAI.StandardMapEntropy.RescaledPath.shifted_tendsto line 7045
  503. lemma OAI.StandardMapEntropy.RescaledPath.denominator_nonzero_slope line 7053
  504. def OAI.StandardMapEntropy.cubicError line 7069
  505. def OAI.StandardMapEntropy.cubicFineError line 7072
  506. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.reciprocal_denominator line 7076
  507. lemma OAI.StandardMapEntropy.RescaledPath.Admissible.reciprocal_eq line 7085
  508. lemma OAI.StandardMapEntropy.fine_cubic_error_tendsto line 7099
  509. lemma OAI.StandardMapEntropy.paired_paths_scarcity line 7113
  510. structure OAI.StandardMapEntropy.LocalConfiguration line 7191
  511. def OAI.StandardMapEntropy.LocalConfiguration.scale line 7198
  512. def OAI.StandardMapEntropy.LocalConfiguration.left line 7199
  513. def OAI.StandardMapEntropy.LocalConfiguration.right line 7200
  514. def OAI.StandardMapEntropy.LocalConfiguration.fast line 7201
  515. def OAI.StandardMapEntropy.LocalConfiguration.slow line 7203
  516. def OAI.StandardMapEntropy.LocalConfiguration.successful line 7205
  517. def OAI.StandardMapEntropy.LocalConfiguration.reciprocalSum line 7206
  518. def OAI.StandardMapEntropy.LocalConfiguration.Valid line 7209
  519. lemma OAI.StandardMapEntropy.LocalConfiguration.Valid.left_admissible line 7212
  520. lemma OAI.StandardMapEntropy.LocalConfiguration.Valid.right_admissible line 7217
  521. lemma OAI.StandardMapEntropy.LocalConfiguration.Valid.fast_admissible line 7222
  522. lemma OAI.StandardMapEntropy.LocalConfiguration.Valid.slow_admissible line 7224
  523. lemma OAI.StandardMapEntropy.LocalConfiguration.fast_parameter line 7226
  524. lemma OAI.StandardMapEntropy.LocalConfiguration.slow_parameter line 7227
  525. lemma OAI.StandardMapEntropy.LocalConfiguration.Valid.scale_pos line 7228
  526. lemma OAI.StandardMapEntropy.LocalConfiguration.Valid.fast_ratio line 7229
  527. lemma OAI.StandardMapEntropy.LocalConfiguration.Valid.slow_min line 7239
  528. lemma OAI.StandardMapEntropy.LocalConfiguration.Valid.reciprocalSum line 7249
  529. lemma OAI.StandardMapEntropy.LocalConfiguration.Valid.cubic_relation line 7259
  530. lemma OAI.StandardMapEntropy.LocalConfiguration.Valid.fine_cubic_relation line 7263
  531. lemma OAI.StandardMapEntropy.LocalConfiguration.successful_subset line 7268
  532. lemma OAI.StandardMapEntropy.LocalConfiguration.successful_nonempty line 7269
  533. lemma OAI.StandardMapEntropy.LocalConfiguration.limit_null line 7272
  534. lemma OAI.StandardMapEntropy.LocalConfiguration.uniform_thick_scarcity line 7295
  535. theorem OAI.StandardMapEntropy.local_scarcity line 7332