OAI/Combinatorics/ThinTrees/Metric/AssignedCharging.lean

GitHub source file

153 declarations, 0 contain sorry, 0 declared as axioms

Metric assigned charging.

  1. structure OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record line 20
  2. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.excluded line 31
  3. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.conflict line 34
  4. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.leafSet line 35
  5. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.routing line 36
  6. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.Shape line 38
  7. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.Protected line 41
  8. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.RoutingCertificate line 46
  9. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.Valid line 51
  10. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.root_mem line 54
  11. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.mem_leafSet line 57
  12. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.mem_routing line 60
  13. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.protected_routing_edges line 65
  14. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.variation_lower line 95
  15. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.restrict_valid line 104
  16. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.LabeledArrangement line 129
  17. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.labeled_energy line 135
  18. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.parentBoundary line 183
  19. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.LocallyConnectedReal line 186
  20. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.parent_boundary_lower line 188
  21. structure OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag line 194
  22. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.input line 210
  23. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.input_leaf line 213
  24. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.input_valid line 245
  25. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.predecessor_dichotomy line 281
  26. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.domain_descendant_partition line 294
  27. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.domain_avoid_partition line 312
  28. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.innerRecord line 325
  29. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.outsideRecord line 327
  30. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.central_conflict line 330
  31. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.central_domain_disjoint line 343
  32. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.protected_same_side line 352
  33. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.central_valid line 370
  34. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.Compatible line 477
  35. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.compatible_symm line 480
  36. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.compatible_self_iff line 483
  37. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.compatible_heredity line 491
  38. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.candidate_ancestor line 498
  39. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.insert_compatible line 511
  40. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.Interior line 530
  41. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.interior_restriction line 536
  42. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.not_interior_ball line 547
  43. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.labeled_empty line 556
  44. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.labeled_subset line 558
  45. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.labeled_pair line 563
  46. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.labeled_union line 570
  47. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.labeled_sets_disjoint line 584
  48. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.restriction line 605
  49. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.Refines line 608
  50. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.restriction_refines line 611
  51. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.compatible_refinements line 616
  52. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.labeled_replace line 625
  53. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.replacement_credit line 631
  54. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.compatible_ne line 656
  55. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.phaseToken line 661
  56. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.restriction_not_fresh line 665
  57. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.restriction_token line 672
  58. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.interior_width line 680
  59. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.interior_ball_subset line 685
  60. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.labeled_singleton line 695
  61. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.labeled_insert line 703
  62. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.avoiding_operation line 712
  63. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.restrictionSet line 827
  64. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.mem_restrictionSet line 830
  65. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.restrictionSet_valid line 834
  66. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.restrictionSet_refines line 843
  67. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.restrictionSet_token line 849
  68. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.restrictions_compatible line 858
  69. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.dense_operation line 867
  70. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.central_refines line 976
  71. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.hollow_token line 985
  72. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.sparse_operation line 995
  73. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.neighbor_exists line 1126
  74. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.neighbor line 1147
  75. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.neighbor_spec line 1150
  76. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.input_injective line 1157
  77. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.input_arrangement line 1162
  78. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.unique_interior line 1179
  79. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.strict_owner_of_interior line 1194
  80. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.large_component line 1224
  81. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.selected_interior line 1256
  82. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.radial_group line 1293
  83. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.RadialRefines line 1370
  84. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.radialRefines_refl line 1374
  85. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.restriction_radialRefines line 1377
  86. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.central_radialRefines line 1381
  87. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.InteriorTo line 1392
  88. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Evolution line 1397
  89. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.OwnerEvolution line 1400
  90. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.evolution_interior line 1404
  91. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.ownerEvolution_order line 1414
  92. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.SameOwnerSeparated line 1426
  93. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.metadata_evolution line 1432
  94. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.metadata_owners line 1443
  95. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.metadata_separation line 1454
  96. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.metadata_fresh line 1486
  97. structure OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.InteriorMove line 1499
  98. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.avoiding_move line 1516
  99. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.dense_move line 1574
  100. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.sparse_move line 1634
  101. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.interior_move line 1729
  102. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.ownerEvolution_refl line 1808
  103. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.ownerEvolution_trans line 1812
  104. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.interior_loop line 1823
  105. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.baseToken line 1907
  106. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.shrinkRecord line 1910
  107. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.shrinkValue line 1913
  108. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.fresh_base line 1917
  109. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.shrink_refines line 1924
  110. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.shrink_valid line 1933
  111. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.shrink_base line 1942
  112. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.shrink_cost line 1953
  113. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.shrink_discard line 1966
  114. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.Record.border_shrink_compatible line 1979
  115. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.shrinkFamily line 2004
  116. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.shrinkFamily_valid line 2007
  117. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.shrinkFamily_sum line 2022
  118. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.border_transition line 2057
  119. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.loop_with_border_debt line 2130
  120. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.phase_loops line 2203
  121. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.assigned_phase line 2327
  122. structure OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily line 2409
  123. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.owners line 2423
  124. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.mass line 2424
  125. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.predecessors line 2425
  126. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.ProtectedFrom line 2428
  127. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.owner_mem line 2431
  128. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.owners_nodes line 2432
  129. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.input_valid line 2437
  130. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.phase line 2454
  131. abbrev OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.Family line 2489
  132. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.initialRadius line 2491
  133. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.mass line 2495
  134. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.Geometric line 2499
  135. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.Ready line 2503
  136. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.radius_nonneg line 2507
  137. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.construct line 2513
  138. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.insertable_bound line 2542
  139. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.goodCenters line 2571
  140. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.badCenters line 2574
  141. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.badCount line 2577
  142. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.boundaryCount line 2579
  143. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.bad_witness line 2582
  144. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.badCount_le line 2598
  145. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.prune line 2641
  146. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.BoundaryRatio line 2742
  147. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.boundary_mass line 2745
  148. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.Fresh line 2769
  149. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.Ratios line 2773
  150. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.GeometricAt line 2777
  151. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.geometric_of line 2781
  152. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.prune_sequence line 2790
  153. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.assigned_bound line 2834