OAI/Probability/FKPressure/Basic.lean

GitHub source file

315 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BelowOne.Time line 19
2. abbrev OAI.BelowOne.Curve line 20
3. abbrev OAI.BelowOne.GridPoint line 21
4. instance OAI.BelowOne.(instance at line 23) line 23
5. instance OAI.BelowOne.(instance at line 24) line 24
6. structure OAI.BelowOne.IncreasingReparam line 27
7. instance OAI.BelowOne.(instance at line 31) line 31
8. def OAI.BelowOne.curveDistance line 35
9. def OAI.BelowOne.IsCurveTest line 41
10. def OAI.BelowOne.gridEmbed line 45
11. def OAI.BelowOne.gridNeighbor line 48
12. def OAI.BelowOne.interpolate line 53
13. def OAI.BelowOne.cycleNext line 60
14. def OAI.BelowOne.cyclePrev line 63
15. structure OAI.BelowOne.SmoothMarkedJordan line 68
16. def OAI.BelowOne.SmoothMarkedJordan.a line 87
17. def OAI.BelowOne.SmoothMarkedJordan.b line 88
18. structure OAI.BelowOne.LatticePolygon line 92
19. abbrev OAI.BelowOne.LatticePolygon.Vertex line 136
20. def OAI.BelowOne.LatticePolygon.position line 138
21. def OAI.BelowOne.LatticePolygon.graph line 140
22. def OAI.BelowOne.LatticePolygon.edges line 145
23. def OAI.BelowOne.LatticePolygon.first line 147
24. def OAI.BelowOne.LatticePolygon.aVertex line 149
25. def OAI.BelowOne.LatticePolygon.bVertex line 150
26. def OAI.BelowOne.LatticePolygon.wiredVertices line 152
27. def OAI.BelowOne.LatticePolygon.wiredEdges line 160
28. def OAI.BelowOne.LatticePolygon.wiredConfiguration line 168
29. def OAI.BelowOne.LatticePolygon.componentCount line 172
30. def OAI.BelowOne.LatticePolygon.configurationWeight line 176
31. def OAI.BelowOne.LatticePolygon.partitionFunction line 180
32. structure OAI.BelowOne.LatticePolygon.Dart line 184
33. instance OAI.BelowOne.LatticePolygon.(instance at line 189) line 189
34. instance OAI.BelowOne.LatticePolygon.(instance at line 195) line 195
35. instance OAI.BelowOne.LatticePolygon.(instance at line 196) line 196
36. def OAI.BelowOne.LatticePolygon.Dart.reverse line 198
37. def OAI.BelowOne.LatticePolygon.dartPosition line 201
38. def OAI.BelowOne.LatticePolygon.dartDirection line 205
39. def OAI.BelowOne.LatticePolygon.angularSteps line 210
40. def OAI.BelowOne.LatticePolygon.IsNextDart line 217
41. def OAI.BelowOne.LatticePolygon.IsSwitched line 223
42. def OAI.BelowOne.LatticePolygon.IsContourSuccessor line 226
43. def OAI.BelowOne.LatticePolygon.IsInitialDart line 231
44. def OAI.BelowOne.LatticePolygon.IsFinalDart line 239
45. def OAI.BelowOne.LatticePolygon.IsInterface line 249
46. structure OAI.BelowOne.MarkedApproximation line 262
47. def OAI.BelowOne.interfaceExpectation line 288
48. def OAI.BelowOne.kappa line 295
49. def OAI.BelowOne.upperHalfPlane line 297
50. def OAI.BelowOne.pastTrace line 299
51. def OAI.BelowOne.loewnerDomain line 302
52. def OAI.BelowOne.inverseOn line 308
53. def OAI.BelowOne.IsLoewnerTrace line 314
54. def OAI.BelowOne.cayley line 335
55. def OAI.BelowOne.IsDomainCoordinate line 339
56. abbrev OAI.BelowOne.BrownianSample line 347
57. instance OAI.BelowOne.(instance at line 349) line 349
58. instance OAI.BelowOne.(instance at line 350) line 350
59. def OAI.BelowOne.IsChordalSLE line 354
60. lemma OAI.BelowOne.FKComponents.eq_of_walk line 380
61. lemma OAI.BelowOne.FKComponents.component_card_sup_edge_of_reachable line 387
62. lemma OAI.BelowOne.FKComponents.component_card_sup_edge_of_not_reachable line 410
63. lemma OAI.BelowOne.FKComponents.component_card_sup_edge line 470
64. def OAI.BelowOne.FKFinite.configuration line 485
65. def OAI.BelowOne.FKFinite.count line 488
66. def OAI.BelowOne.FKFinite.weight line 491
67. def OAI.BelowOne.FKFinite.partition line 494
68. lemma OAI.BelowOne.FKFinite.weight_pos line 497
69. lemma OAI.BelowOne.FKFinite.partition_pos line 501
70. lemma OAI.BelowOne.FKFinite.configuration_insert line 508
71. lemma OAI.BelowOne.FKFinite.configuration_union line 516
72. lemma OAI.BelowOne.FKFinite.weight_union line 523
73. theorem OAI.BelowOne.FKFinite.domain_markov line 532
74. lemma OAI.BelowOne.FKFinite.weight_insert_connected line 557
75. lemma OAI.BelowOne.FKFinite.weight_insert_separated line 566
76. theorem OAI.BelowOne.FKFinite.edge_conditional_probability line 577
77. def OAI.BelowOne.LatticePolygon.wireGraph line 601
78. lemma OAI.BelowOne.LatticePolygon.wiredConfiguration_eq line 604
79. lemma OAI.BelowOne.LatticePolygon.componentCount_eq line 612
80. lemma OAI.BelowOne.LatticePolygon.configurationWeight_odds line 617
81. lemma OAI.BelowOne.LatticePolygon.partitionFunction_odds line 635
82. theorem OAI.BelowOne.LatticePolygon.normalized_configurationWeight_odds line 645
83. def OAI.BelowOne.FKPressure.graph line 672
84. def OAI.BelowOne.FKPressure.components line 675
85. def OAI.BelowOne.FKPressure.partition line 679
86. lemma OAI.BelowOne.FKPressure.graph_empty line 684
87. lemma OAI.BelowOne.FKPressure.graph_mono line 688
88. lemma OAI.BelowOne.FKPressure.graph_insert line 693
89. lemma OAI.BelowOne.FKPressure.graph_contracted line 699
90. lemma OAI.BelowOne.FKPressure.partition_empty line 705
91. lemma OAI.BelowOne.FKPressure.deletion_contraction line 711
92. lemma OAI.BelowOne.FKPressure.separating_edge_count line 727
93. lemma OAI.BelowOne.FKPressure.separating_edge_partition line 737
94. theorem OAI.BelowOne.FKPressure.negative_partition line 751
95. theorem OAI.BelowOne.FKPressure.signed_partition_pos line 783
96. def OAI.BelowOne.FKPressure.hardSum line 817
97. lemma OAI.BelowOne.FKPressure.components_contracted_of_reachable line 820
98. lemma OAI.BelowOne.FKPressure.hardSum_deletion_contraction line 828
99. lemma OAI.BelowOne.FKPressure.hardSum_eq_zero_of_reachable line 842
100. theorem OAI.BelowOne.FKPressure.hardSum_sign line 855
101. lemma OAI.BelowOne.FKPressure.union_constrained_sum line 879
102. lemma OAI.BelowOne.FKPressure.fixed_union line 946
103. theorem OAI.BelowOne.FKPressure.fixed_union_hard_nonpos line 965
104. lemma OAI.BelowOne.FKPressure.regroup_union line 999
105. def OAI.BelowOne.FKPressure.connectedSum line 1028
106. lemma OAI.BelowOne.FKPressure.connectedSum_grouped line 1036
107. theorem OAI.BelowOne.FKPressure.connectedSum_nonpos line 1059
108. instance OAI.BelowOne.PartitionCumulant.finiteSetoid line 1084
109. instance OAI.BelowOne.PartitionCumulant.fintypeSetoid line 1087
110. def OAI.BelowOne.PartitionCumulant.extendMap line 1091
111. def OAI.BelowOne.PartitionCumulant.extend line 1095
112. lemma OAI.BelowOne.PartitionCumulant.extend_some line 1098
113. lemma OAI.BelowOne.PartitionCumulant.extend_none_some line 1103
114. lemma OAI.BelowOne.PartitionCumulant.restrict_extend line 1106
115. lemma OAI.BelowOne.PartitionCumulant.extend_injective line 1111
116. lemma OAI.BelowOne.PartitionCumulant.extend_bijective line 1126
117. def OAI.BelowOne.PartitionCumulant.extensionEquiv line 1176
118. lemma OAI.BelowOne.PartitionCumulant.card_extend_none line 1179
119. lemma OAI.BelowOne.PartitionCumulant.card_extend_some line 1193
120. theorem OAI.BelowOne.PartitionCumulant.sum_option line 1210
121. def OAI.BelowOne.PartitionCumulant.coefficient line 1227
122. lemma OAI.BelowOne.PartitionCumulant.coefficient_recurrence line 1229
123. theorem OAI.BelowOne.PartitionCumulant.sum_coefficient_option line 1243
124. def OAI.BelowOne.PartitionCumulant.setoidEquiv line 1252
125. lemma OAI.BelowOne.PartitionCumulant.card_relabel line 1266
126. lemma OAI.BelowOne.PartitionCumulant.sum_relabel line 1271
127. lemma OAI.BelowOne.PartitionCumulant.sum_coefficient_nontrivial line 1276
128. lemma OAI.BelowOne.PartitionCumulant.sum_coefficient_subsingleton line 1284
129. lemma OAI.BelowOne.PartitionCumulant.sum_coefficient line 1302
130. def OAI.BelowOne.PartitionCumulant.coarseningQuotientEquiv line 1317
131. theorem OAI.BelowOne.PartitionCumulant.sum_coarsenings line 1329
132. theorem OAI.BelowOne.PartitionCumulant.connected_cancellation line 1342
133. def OAI.BelowOne.FKPressure.blockStructureSum line 1381
134. theorem OAI.BelowOne.FKPressure.exponential_cancellation line 1391
135. theorem OAI.BelowOne.FKPressure.logarithmic_structure_nonpos line 1432
136. lemma OAI.BelowOne.FKPressure.component_card_block_sum line 1456
137. lemma OAI.BelowOne.FKPressure.reachable_induce_block line 1468
138. lemma OAI.BelowOne.FKPressure.components_induce_block_sum line 1483
139. lemma OAI.BelowOne.FKPressure.component_weight_block_prod line 1499
140. lemma OAI.BelowOne.FKPressure.graph_adj_iff line 1509
141. lemma OAI.BelowOne.FKPressure.endpoints_reachable line 1519
142. lemma OAI.BelowOne.FKPressure.graph_reachable_le_iff line 1528
143. def OAI.BelowOne.FKPressure.edgeBlock line 1545
144. lemma OAI.BelowOne.FKPressure.graph_induce_filter line 1548
145. abbrev OAI.BelowOne.SubsetSplitting.Selection line 1584
146. def OAI.BelowOne.SubsetSplitting.fiber line 1586
147. def OAI.BelowOne.SubsetSplitting.split line 1588
148. def OAI.BelowOne.SubsetSplitting.join line 1594
149. lemma OAI.BelowOne.SubsetSplitting.join_split line 1600
150. lemma OAI.BelowOne.SubsetSplitting.split_join line 1612
151. def OAI.BelowOne.SubsetSplitting.selectionEquiv line 1628
152. lemma OAI.BelowOne.SubsetSplitting.sum_factorization line 1634
153. def OAI.BelowOne.SubsetSplitting.piTripleEquiv line 1647
154. lemma OAI.BelowOne.SubsetSplitting.sum_triple_coe line 1654
155. lemma OAI.BelowOne.SubsetSplitting.sum_factorization_three line 1667
156. lemma OAI.BelowOne.FKPressure.filter_classical line 1711
157. lemma OAI.BelowOne.FKPressure.powerset_filter_eq line 1715
158. lemma OAI.BelowOne.FKPressure.sum_powerset_filter line 1726
159. lemma OAI.BelowOne.FKPressure.confinement_iff line 1732
160. lemma OAI.BelowOne.FKPressure.blockStructureSum_restrict line 1743
161. def OAI.BelowOne.FKPressure.inducedBlockMoment line 1771
162. lemma OAI.BelowOne.FKPressure.structure_weight_factor line 1780
163. lemma OAI.BelowOne.FKPressure.blockStructureSum_factorization line 1799
164. abbrev OAI.BelowOne.MultiaffineDerivative.coordinate line 1833
165. def OAI.BelowOne.MultiaffineDerivative.restrict line 1835
166. lemma OAI.BelowOne.MultiaffineDerivative.restrict_apply line 1839
167. def OAI.BelowOne.MultiaffineDerivative.Matches line 1841
168. lemma OAI.BelowOne.MultiaffineDerivative.matches_iff line 1845
169. lemma OAI.BelowOne.MultiaffineDerivative.matches_data line 1862
170. lemma OAI.BelowOne.MultiaffineDerivative.matches_unique line 1881
171. def OAI.BelowOne.MultiaffineDerivative.matchingEmbedding line 1886
172. lemma OAI.BelowOne.MultiaffineDerivative.matchingEmbedding_matches line 1892
173. lemma OAI.BelowOne.MultiaffineDerivative.sum_matches line 1901
174. lemma OAI.BelowOne.MultiaffineDerivative.factor_indicator line 1918
175. lemma OAI.BelowOne.MultiaffineDerivative.prod_indicator line 1933
176. lemma OAI.BelowOne.MultiaffineDerivative.ite_classical line 1941
177. lemma OAI.BelowOne.MultiaffineDerivative.dite_classical line 1945
178. lemma OAI.BelowOne.MultiaffineDerivative.range_equiv_classical line 1949
179. lemma OAI.BelowOne.MultiaffineDerivative.monomial_derivative line 1955
180. lemma OAI.BelowOne.MultiaffineDerivative.contDiff_monomial line 2002
181. lemma OAI.BelowOne.MultiaffineDerivative.weighted_monomial_derivative line 2006
182. def OAI.BelowOne.MultiaffineDerivative.polynomial line 2014
183. lemma OAI.BelowOne.MultiaffineDerivative.contDiff_polynomial line 2017
184. lemma OAI.BelowOne.MultiaffineDerivative.polynomial_derivative line 2022
185. lemma OAI.BelowOne.MultiaffineDerivative.polynomial_zero line 2034
186. def OAI.BelowOne.OrderedPartitionBridge.partition line 2054
187. lemma OAI.BelowOne.OrderedPartitionBridge.index_emb line 2056
188. lemma OAI.BelowOne.OrderedPartitionBridge.index_surjective line 2060
189. lemma OAI.BelowOne.OrderedPartitionBridge.card_partition line 2064
190. def OAI.BelowOne.OrderedPartitionBridge.maximum line 2068
191. lemma OAI.BelowOne.OrderedPartitionBridge.index_maximum line 2071
192. lemma OAI.BelowOne.OrderedPartitionBridge.le_maximum line 2074
193. lemma OAI.BelowOne.OrderedPartitionBridge.relation_iff_range line 2079
194. lemma OAI.BelowOne.OrderedPartitionBridge.maximum_eq_of_partition_eq line 2088
195. lemma OAI.BelowOne.OrderedPartitionBridge.partition_injective line 2101
196. def OAI.BelowOne.OrderedPartitionBridge.block line 2147
197. lemma OAI.BelowOne.OrderedPartitionBridge.mem_block line 2151
198. lemma OAI.BelowOne.OrderedPartitionBridge.block_nonempty line 2155
199. lemma OAI.BelowOne.OrderedPartitionBridge.block_eq line 2158
200. def OAI.BelowOne.OrderedPartitionBridge.blockMax line 2163
201. lemma OAI.BelowOne.OrderedPartitionBridge.blockMax_related line 2166
202. lemma OAI.BelowOne.OrderedPartitionBridge.blockMax_eq line 2169
203. def OAI.BelowOne.OrderedPartitionBridge.maxima line 2172
204. lemma OAI.BelowOne.OrderedPartitionBridge.maximum_fixed line 2176
205. lemma OAI.BelowOne.OrderedPartitionBridge.blockMax_mem line 2181
206. def OAI.BelowOne.OrderedPartitionBridge.ofSetoid line 2185
207. lemma OAI.BelowOne.OrderedPartitionBridge.range_ofSetoid line 2224
208. lemma OAI.BelowOne.OrderedPartitionBridge.partition_ofSetoid line 2228
209. def OAI.BelowOne.OrderedPartitionBridge.partitionEquiv line 2246
210. lemma OAI.BelowOne.PartitionCumulant.iteratedDeriv_succ_log line 2262
211. lemma OAI.BelowOne.PartitionCumulant.iteratedDeriv_log_one line 2270
212. lemma OAI.BelowOne.PartitionCumulant.iteratedFDeriv_log_comp line 2277
213. def OAI.BelowOne.PartitionCumulant.blockDerivative line 2299
214. lemma OAI.BelowOne.PartitionCumulant.logarithmic_derivative_partition_sum line 2304
215. def OAI.BelowOne.FKPressure.siteMoment line 2338
216. lemma OAI.BelowOne.FKPressure.siteMoment_empty line 2347
217. lemma OAI.BelowOne.FKPressure.block_edge_iff line 2353
218. lemma OAI.BelowOne.FKPressure.inducedBlockMoment_eq_siteMoment line 2365
219. lemma OAI.BelowOne.FKPressure.bot_reachable_le line 2373
220. lemma OAI.BelowOne.FKPressure.blockStructureSum_siteMoment line 2378
221. def OAI.BelowOne.FKPressure.sitePolynomial line 2385
222. lemma OAI.BelowOne.FKPressure.sitePolynomial_zero line 2389
223. lemma OAI.BelowOne.FKPressure.coe_image_emb line 2395
224. lemma OAI.BelowOne.FKPressure.product_moments_partition line 2400
225. lemma OAI.BelowOne.FKPressure.blockDerivative_sitePolynomial line 2420
226. theorem OAI.BelowOne.FKPressure.sitePolynomial_log_derivative line 2443
227. theorem OAI.BelowOne.FKPressure.sitePolynomial_log_derivative_nonpos line 2456
228. def OAI.BelowOne.FKPressure.inducedPartition line 2480
229. lemma OAI.BelowOne.FKPressure.alternating_powerset line 2486
230. lemma OAI.BelowOne.FKPressure.siteMoment_separate line 2498
231. lemma OAI.BelowOne.FKPressure.siteMoment_squarefree line 2523
232. lemma OAI.BelowOne.FKPressure.siteMoment_collision_zero line 2533
233. def OAI.BelowOne.FKPressure.imageEquiv line 2555
234. lemma OAI.BelowOne.FKPressure.induced_graph_image_iso line 2564
235. lemma OAI.BelowOne.FKPressure.induced_component_image line 2597
236. lemma OAI.BelowOne.FKPressure.inducedPartition_reindex line 2607
237. def OAI.BelowOne.FKPressure.liftEdges line 2654
238. def OAI.BelowOne.FKPressure.hardEdges line 2657
239. def OAI.BelowOne.FKPressure.squarefreeMoment line 2660
240. lemma OAI.BelowOne.FKPressure.mem_liftEdges line 2666
241. lemma OAI.BelowOne.FKPressure.liftEdges_filter_image line 2671
242. lemma OAI.BelowOne.FKPressure.liftEdges_filter_inj line 2689
243. lemma OAI.BelowOne.FKPressure.hardEdges_filter_empty_iff line 2704
244. lemma OAI.BelowOne.FKPressure.inducedPartition_filter line 2718
245. lemma OAI.BelowOne.FKPressure.siteMoment_lift line 2727
246. def OAI.BelowOne.FKPressure.unscaledSitePolynomial line 2769
247. lemma OAI.BelowOne.FKPressure.unscaledSitePolynomial_zero line 2773
248. lemma OAI.BelowOne.FKPressure.injOn_range_iff line 2778
249. lemma OAI.BelowOne.FKPressure.lifted_derivative line 2788
250. lemma OAI.BelowOne.FKPressure.blockDerivative_lift line 2799
251. theorem OAI.BelowOne.FKPressure.unscaledSitePolynomial_log_derivative line 2819
252. theorem OAI.BelowOne.FKPressure.unscaledSitePolynomial_log_derivative_nonpos line 2836
253. def OAI.BelowOne.ComponentProduct.saturated line 2862
254. def OAI.BelowOne.ComponentProduct.preimage line 2865
255. lemma OAI.BelowOne.ComponentProduct.mem_preimage line 2868
256. lemma OAI.BelowOne.ComponentProduct.preimage_saturated line 2872
257. lemma OAI.BelowOne.ComponentProduct.image_preimage line 2877
258. lemma OAI.BelowOne.ComponentProduct.preimage_image line 2889
259. lemma OAI.BelowOne.ComponentProduct.selected_product line 2900
260. lemma OAI.BelowOne.ComponentProduct.expansion line 2907
261. lemma OAI.BelowOne.FKPressure.reachable_induce_saturated line 2943
262. lemma OAI.BelowOne.FKPressure.component_card_induce_saturated line 2957
263. lemma OAI.BelowOne.FKPressure.saturated_graph_iff line 2980
264. def OAI.BelowOne.FKPressure.componentProduct line 3002
265. lemma OAI.BelowOne.FKPressure.componentProduct_expansion line 3006
266. lemma OAI.BelowOne.SubsetSplitting.sum_factorization_binary line 3033
267. lemma OAI.BelowOne.FKPressure.graph_induce_inside_filter line 3063
268. lemma OAI.BelowOne.FKPressure.confined_edge_sum line 3081
269. def OAI.BelowOne.FKPressure.percolationSitePolynomial line 3121
270. def OAI.BelowOne.FKPressure.percolationCoefficient line 3126
271. lemma OAI.BelowOne.FKPressure.percolationSitePolynomial_eq line 3132
272. def OAI.BelowOne.FKPressure.incidentProduct line 3168
273. def OAI.BelowOne.FKPressure.incidentScale line 3172
274. lemma OAI.BelowOne.FKPressure.incidentProduct_pos line 3176
275. lemma OAI.BelowOne.FKPressure.incidentProduct_subprod line 3184
276. lemma OAI.BelowOne.FKPressure.incident_product_identity line 3197
277. lemma OAI.BelowOne.FKPressure.percolationCoefficient_rescale line 3211
278. lemma OAI.BelowOne.FKPressure.percolationSitePolynomial_rescale line 3225
279. def OAI.BelowOne.MultiaffineDerivative.diagonalEquiv line 3250
280. lemma OAI.BelowOne.MultiaffineDerivative.diagonalEquiv_coordinate line 3261
281. lemma OAI.BelowOne.MultiaffineDerivative.iteratedFDeriv_diagonal line 3268
282. lemma OAI.BelowOne.FKPressure.percolationSitePolynomial_zero line 3297
283. lemma OAI.BelowOne.FKPressure.percolationSitePolynomial_log_derivative_nonpos line 3304
284. lemma OAI.BelowOne.FKPressure.componentProduct_pos line 3321
285. lemma OAI.BelowOne.FKPressure.percolationSitePolynomial_pos line 3331
286. lemma OAI.BelowOne.PositiveMultilinear.sum_coordinates line 3361
287. lemma OAI.BelowOne.PositiveMultilinear.expansion line 3365
288. lemma OAI.BelowOne.PositiveMultilinear.nonneg line 3375
289. lemma OAI.BelowOne.PositiveMultilinear.ones_eq_sum line 3381
290. lemma OAI.BelowOne.PositiveMultilinear.norm_le_ones line 3386
291. lemma OAI.BelowOne.PositiveSeries.scalar_apply_nonneg line 3413
292. lemma OAI.BelowOne.PositiveSeries.summable_add_of_shift line 3422
293. lemma OAI.BelowOne.PositiveSeries.radius_add_le line 3461
294. theorem OAI.BelowOne.PositiveSeries.not_analytic_at_radius line 3474
295. theorem OAI.BelowOne.PositiveSeries.radius_gt_of_analytic_interval line 3526
296. def OAI.BelowOne.PositiveAnalyticCube.cube line 3572
297. def OAI.BelowOne.PositiveAnalyticCube.diagonal line 3573
298. def OAI.BelowOne.PositiveAnalyticCube.taylor line 3575
299. def OAI.BelowOne.PositiveAnalyticCube.diagonalCoefficient line 3578
300. lemma OAI.BelowOne.PositiveAnalyticCube.taylor_diagonal_eq line 3581
301. lemma OAI.BelowOne.PositiveAnalyticCube.diagonal_hasFPowerSeriesAt line 3589
302. lemma OAI.BelowOne.PositiveAnalyticCube.taylor_coordinate_nonneg line 3602
303. lemma OAI.BelowOne.PositiveAnalyticCube.diagonalCoefficient_nonneg line 3613
304. lemma OAI.BelowOne.PositiveAnalyticCube.radius_le_of_norm_le line 3619
305. lemma OAI.BelowOne.PositiveAnalyticCube.taylor_radius_gt_one line 3634
306. lemma OAI.BelowOne.PositiveAnalyticCube.hasFPowerSeriesAt_taylor line 3650
307. lemma OAI.BelowOne.PositiveAnalyticCube.cube_convex line 3661
308. lemma OAI.BelowOne.PositiveAnalyticCube.cube_subset_eball line 3669
309. lemma OAI.BelowOne.PositiveAnalyticCube.taylor_sum_eq_on_cube line 3680
310. def OAI.BelowOne.FKPressure.pressure line 3708
311. lemma OAI.BelowOne.FKPressure.analyticAt_percolationSitePolynomial line 3711
312. lemma OAI.BelowOne.FKPressure.pressure_zero line 3723
313. lemma OAI.BelowOne.FKPressure.pressure_derivative_nonneg line 3727
314. lemma OAI.BelowOne.FKPressure.pressure_analyticOn_cube line 3737
315. theorem OAI.BelowOne.FKPressure.pressure_expansion line 3744