OAI/Probability/Honeycomb/TriangleVisits.lean

GitHub source file

150 declarations, 0 contain sorry, 0 declared as axioms

Honeycomb triangle chords, visit sums and positive finite means.

  1. structure OAI.DiskBoundary.Vertex line 14
  2. structure OAI.DiskBoundary.Port line 20
  3. def OAI.DiskBoundary.direction line 26
  4. def OAI.DiskBoundary.U line 31
  5. def OAI.DiskBoundary.V line 33
  6. def OAI.DiskBoundary.position line 35
  7. def OAI.DiskBoundary.edgeA line 38
  8. def OAI.DiskBoundary.edgeB line 40
  9. def OAI.DiskBoundary.portPosition line 46
  10. def OAI.DiskBoundary.Incident line 48
  11. def OAI.DiskBoundary.Adj line 50
  12. def OAI.DiskBoundary.BoundaryPort line 53
  13. structure OAI.DiskBoundary.PortPath line 56
  14. def OAI.DiskBoundary.PortPath.length line 69
  15. def OAI.DiskBoundary.PortPath.joints line 71
  16. def OAI.DiskBoundary.PortPath.trace line 74
  17. def OAI.DiskBoundary.PortPath.diameter line 78
  18. def OAI.DiskBoundary.PortPath.height line 80
  19. instance OAI.DiskBoundary.(instance at line 85) line 85
  20. instance OAI.DiskBoundary.(instance at line 86) line 86
  21. def OAI.DiskBoundary.IsChord line 88
  22. abbrev OAI.DiskBoundary.Chord line 91
  23. def OAI.DiskBoundary.criticalPoint line 93
  24. def OAI.DiskBoundary.weight line 95
  25. def OAI.DiskBoundary.pathMeasure line 97
  26. def OAI.DiskBoundary.Normalizable line 100
  27. def OAI.DiskBoundary.normalize line 103
  28. def OAI.DiskBoundary.dot line 106
  29. def OAI.DiskBoundary.halfPlane line 108
  30. def OAI.DiskBoundary.wallPort line 110
  31. abbrev OAI.DiskBoundary.Arch line 112
  32. def OAI.DiskBoundary.Arch.path line 115
  33. def OAI.DiskBoundary.μ line 117
  34. def OAI.DiskBoundary.archKernel line 119
  35. def OAI.DiskBoundary.heightTail line 122
  36. def OAI.DiskBoundary.diameterTail line 124
  37. def OAI.DiskBoundary.diameterWindow line 126
  38. def OAI.DiskBoundary.heightWindow line 129
  39. def OAI.DiskBoundary.archMean line 132
  40. def OAI.DiskBoundary.triangle line 135
  41. def OAI.DiskBoundary.triangleVertices line 137
  42. def OAI.DiskBoundary.innerVertices line 139
  43. def OAI.DiskBoundary.triangleMeasure line 141
  44. def OAI.DiskBoundary.hitsInner line 144
  45. def OAI.DiskBoundary.triangleLaw line 147
  46. def OAI.DiskBoundary.visitProbability line 150
  47. def OAI.DiskBoundary.triangleMean line 153
  48. def OAI.DiskBoundary.innerCount line 156
  49. def OAI.DiskBoundary.triangleInnerMean line 160
  50. def OAI.DiskBoundary.admissibleLevels line 163
  51. def OAI.DiskBoundary.wallFilter line 165
  52. def OAI.DiskBoundary.ComparablePower line 167
  53. def OAI.DiskBoundary.HasExponent line 173
  54. def OAI.DiskBoundary.UniformVisitExponent line 178
  55. def OAI.DiskBoundary.SharpBoundaryMassAndAnnealedChordLaws line 183
  56. theorem OAI.DiskBoundary.Vertex.ext line 200
  57. theorem OAI.DiskBoundary.PortPath.ext line 210
  58. instance OAI.DiskBoundary.(instance at line 219) line 219
  59. theorem OAI.DiskBoundary.PortPath.length_pos line 226
  60. theorem OAI.DiskBoundary.criticalPoint_pos line 229
  61. theorem OAI.DiskBoundary.criticalPoint_lt_one line 233
  62. theorem OAI.DiskBoundary.weight_pos line 241
  63. theorem OAI.DiskBoundary.weight_lt_top line 244
  64. theorem OAI.DiskBoundary.weight_le_one line 246
  65. theorem OAI.DiskBoundary.pathMeasure_apply line 251
  66. theorem OAI.DiskBoundary.pathMeasure_singleton line 260
  67. theorem OAI.DiskBoundary.lintegral_pathMeasure line 267
  68. theorem OAI.DiskBoundary.normalize_apply line 272
  69. theorem OAI.DiskBoundary.normalize_univ line 277
  70. theorem OAI.DiskBoundary.normalize_isProbabilityMeasure line 283
  71. theorem OAI.DiskBoundary.normalized_atom line 287
  72. theorem OAI.DiskBoundary.position_re line 295
  73. theorem OAI.DiskBoundary.position_im line 302
  74. theorem OAI.DiskBoundary.edge_displacement line 308
  75. theorem OAI.DiskBoundary.direction_normSq line 313
  76. theorem OAI.DiskBoundary.direction_norm line 317
  77. theorem OAI.DiskBoundary.edge_length line 323
  78. theorem OAI.DiskBoundary.position_injective line 326
  79. theorem OAI.DiskBoundary.mem_halfPlane_iff line 355
  80. theorem OAI.DiskBoundary.wallPort_position line 360
  81. theorem OAI.DiskBoundary.wallPort_boundary line 366
  82. theorem OAI.DiskBoundary.PortPath.source_mem_trace line 370
  83. theorem OAI.DiskBoundary.PortPath.target_mem_trace line 374
  84. theorem OAI.DiskBoundary.PortPath.vertex_mem_trace line 378
  85. theorem OAI.DiskBoundary.PortPath.trace_isCompact line 384
  86. theorem OAI.DiskBoundary.PortPath.trace_nonempty line 394
  87. theorem OAI.DiskBoundary.Arch.height_le_diameter line 397
  88. theorem OAI.DiskBoundary.heightTail_le_diameterTail line 412
  89. theorem OAI.DiskBoundary.heightTail_antitone line 417
  90. theorem OAI.DiskBoundary.diameterTail_antitone line 421
  91. theorem OAI.DiskBoundary.dot_zero_position line 425
  92. theorem OAI.DiskBoundary.dot_one_position line 433
  93. theorem OAI.DiskBoundary.dot_two_position line 441
  94. theorem OAI.DiskBoundary.triangle_coordinate_bounds line 446
  95. theorem OAI.DiskBoundary.triangleVertices_finite line 468
  96. def OAI.DiskBoundary.incidentPorts line 483
  97. theorem OAI.DiskBoundary.incident_iff_mem line 487
  98. theorem OAI.DiskBoundary.boundaryPorts_finite line 494
  99. def OAI.DiskBoundary.Chord.domainList line 504
  100. theorem OAI.DiskBoundary.Chord.domainList_map_val line 507
  101. theorem OAI.DiskBoundary.Chord.domainList_nodup line 511
  102. theorem OAI.DiskBoundary.finite_chord line 517
  103. theorem OAI.DiskBoundary.Chord.length_le_card line 533
  104. theorem OAI.DiskBoundary.finite_pathMeasure line 540
  105. theorem OAI.DiskBoundary.triangleMeasure_finite line 550
  106. theorem OAI.DiskBoundary.admissibleLevels_tendsto line 554
  107. instance OAI.DiskBoundary.(instance at line 564) line 564
  108. theorem OAI.DiskBoundary.PortPath.length_eq_tsum_visits line 566
  109. theorem OAI.DiskBoundary.innerCount_eq_tsum_visits line 578
  110. theorem OAI.DiskBoundary.lintegral_length_eq_tsum_visits line 600
  111. theorem OAI.DiskBoundary.lintegral_innerCount_eq_tsum_visits line 618
  112. theorem OAI.DiskBoundary.triangleMean_eq_sum_visitProbability line 642
  113. theorem OAI.DiskBoundary.triangleInnerMean_eq_sum_visitProbability line 646
  114. theorem OAI.DiskBoundary.innerCount_le_length line 651
  115. theorem OAI.DiskBoundary.triangleInnerMean_le_triangleMean line 657
  116. theorem OAI.DiskBoundary.finite_chord_event_normalizable line 663
  117. theorem OAI.DiskBoundary.triangleMean_le_card line 675
  118. theorem OAI.DiskBoundary.triangleMean_lt_top line 686
  119. theorem OAI.DiskBoundary.mem_halfPlane_iff_k_nonneg line 691
  120. theorem OAI.DiskBoundary.boundaryPort_halfPlane_coords line 707
  121. theorem OAI.DiskBoundary.boundaryPort_halfPlane_iff line 713
  122. theorem OAI.DiskBoundary.lintegral_normalized_pathMeasure line 724
  123. theorem OAI.DiskBoundary.archMean_eq_weighted_ratio line 738
  124. theorem OAI.DiskBoundary.triangleMean_eq_weighted_ratio line 743
  125. def OAI.DiskBoundary.row line 749
  126. theorem OAI.DiskBoundary.row_ne_nil line 753
  127. theorem OAI.DiskBoundary.row_head line 756
  128. theorem OAI.DiskBoundary.row_head? line 760
  129. theorem OAI.DiskBoundary.row_last line 764
  130. theorem OAI.DiskBoundary.mem_row line 774
  131. theorem OAI.DiskBoundary.row_nodup line 782
  132. theorem OAI.DiskBoundary.row_chain line 787
  133. def OAI.DiskBoundary.rowPath line 802
  134. theorem OAI.DiskBoundary.a_mem_triangle_level line 813
  135. theorem OAI.DiskBoundary.b_mem_triangle_level line 845
  136. theorem OAI.DiskBoundary.mem_triangle_level line 878
  137. def OAI.DiskBoundary.triangleRow line 887
  138. theorem OAI.DiskBoundary.exists_chord_through line 911
  139. theorem OAI.DiskBoundary.origin_mem_triangle line 927
  140. theorem OAI.DiskBoundary.innerVertices_subset line 932
  141. theorem OAI.DiskBoundary.hitsInner_nonempty line 937
  142. theorem OAI.DiskBoundary.triangle_normalizable line 944
  143. theorem OAI.DiskBoundary.eventually_triangle_normalizable line 949
  144. theorem OAI.DiskBoundary.triangleLaw_isProbabilityMeasure line 955
  145. theorem OAI.DiskBoundary.visitProbability_pos line 959
  146. theorem OAI.DiskBoundary.visitProbability_le_one line 971
  147. theorem OAI.DiskBoundary.triangleMean_pos line 976
  148. theorem OAI.DiskBoundary.eventually_triangleMean_pos_finite line 990
  149. theorem OAI.DiskBoundary.triangleInnerMean_pos line 997
  150. theorem OAI.DiskBoundary.eventually_triangleInnerMean_pos_finite line 1009