OAI/Combinatorics/KServer/Caps.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

The actual rankwise caps used by the star construction: core flags and both endpoint trackers run for the full history, not only at output times.

  1. def OAI.KServer.TrackedCaps.count line 16
  2. def OAI.KServer.TrackedCaps.core line 19
  3. def OAI.KServer.TrackedCaps.flex line 22
  4. def OAI.KServer.TrackedCaps.estimate line 25
  5. def OAI.KServer.TrackedCaps.cap line 28
  6. lemma OAI.KServer.TrackedCaps.cap_eq line 31
  7. lemma OAI.KServer.TrackedCaps.count_nonneg line 40
  8. lemma OAI.KServer.TrackedCaps.core_nonneg line 43
  9. lemma OAI.KServer.TrackedCaps.flex_nonneg line 46
  10. lemma OAI.KServer.TrackedCaps.decomposition line 50
  11. lemma OAI.KServer.TrackedCaps.domination line 63
  12. lemma OAI.KServer.TrackedCaps.flex_antitone line 80
  13. lemma OAI.KServer.TrackedCaps.flex_slack line 89
  14. lemma OAI.KServer.TrackedCaps.estimate_error line 109
  15. lemma OAI.KServer.TrackedCaps.scaled_bounds line 123
  16. lemma OAI.KServer.TrackedCaps.endpoint_adapted line 140
  17. lemma OAI.KServer.TrackedCaps.cap_adapted line 147
  18. def OAI.KServer.StarSide.mark line 172
  19. def OAI.KServer.StarSide.sides line 176
  20. def OAI.KServer.StarSide.coarseFlex line 182
  21. def OAI.KServer.StarSide.scale line 185
  22. def OAI.KServer.StarSide.sideFlags line 191
  23. def OAI.KServer.StarSide.logs line 195
  24. def OAI.KServer.StarSide.input line 199
  25. def OAI.KServer.StarSide.proportion line 208
  26. lemma OAI.KServer.StarSide.coarseFlex_nonneg line 212
  27. lemma OAI.KServer.StarSide.scale_nonneg line 221
  28. lemma OAI.KServer.StarSide.proportion_mem line 228
  29. lemma OAI.KServer.StarSide.logs_upper line 233
  30. lemma OAI.KServer.StarSide.feasible line 244
  31. lemma OAI.KServer.StarSide.coarseFlex_adapted line 280
  32. lemma OAI.KServer.StarSide.input_adapted line 288
  33. lemma OAI.KServer.StarSide.proportion_adapted line 320
  34. lemma OAI.KServer.CoarseFineBridge.base_compare line 345
  35. lemma OAI.KServer.CoarseFineBridge.estimate_compare line 367
  36. lemma OAI.KServer.CoarseFineBridge.compare line 384
  37. lemma OAI.KServer.CoarseFineBridge.zero_iff line 402
  38. def OAI.KServer.LocalConstants.cb line 419
  39. def OAI.KServer.LocalConstants.cg line 420
  40. def OAI.KServer.LocalConstants.ct line 421
  41. def OAI.KServer.LocalConstants.cw line 422
  42. def OAI.KServer.LocalConstants.C line 423
  43. def OAI.KServer.LocalConstants.eb line 424
  44. def OAI.KServer.LocalConstants.lb line 425
  45. def OAI.KServer.LocalConstants.rho line 426
  46. def OAI.KServer.LocalConstants.dp line 427
  47. def OAI.KServer.LocalConstants.ds line 428
  48. lemma OAI.KServer.LocalConstants.positive line 430
  49. lemma OAI.KServer.LocalConstants.small line 432
  50. def OAI.KServer.ActualCaps.ell line 453
  51. def OAI.KServer.ActualCaps.z line 454
  52. def OAI.KServer.ActualCaps.a line 455
  53. def OAI.KServer.ActualCaps.flexCap line 457
  54. def OAI.KServer.ActualCaps.cap line 460
  55. lemma OAI.KServer.ActualCaps.ell_ge_one line 463
  56. lemma OAI.KServer.ActualCaps.ell_pos line 466
  57. lemma OAI.KServer.ActualCaps.ranges line 468
  58. lemma OAI.KServer.ActualCaps.scalar_errors line 487
  59. lemma OAI.KServer.ActualCaps.regular_bounds line 507
  60. lemma OAI.KServer.ActualCaps.dominant_bounds line 520
  61. lemma OAI.KServer.ActualCaps.estimate_nonneg line 547
  62. lemma OAI.KServer.ActualCaps.flexCap_nonneg line 556
  63. lemma OAI.KServer.ActualCaps.flexCap_upper line 564
  64. lemma OAI.KServer.ActualCaps.cap_bounds line 585
  65. lemma OAI.KServer.ActualCaps.inactive_cap line 594
  66. lemma OAI.KServer.ActualCaps.held_beta_bounds line 614
  67. def OAI.KServer.ActualStar.key line 637
  68. def OAI.KServer.ActualStar.b line 639
  69. def OAI.KServer.ActualStar.β line 642
  70. def OAI.KServer.ActualStar.h line 644
  71. def OAI.KServer.ActualStar.active line 647
  72. def OAI.KServer.ActualStar.mark line 648
  73. def OAI.KServer.ActualStar.α line 651
  74. lemma OAI.KServer.ActualStar.h_nonneg line 654
  75. lemma OAI.KServer.ActualStar.h_one line 656
  76. lemma OAI.KServer.ActualStar.h_upper line 659
  77. lemma OAI.KServer.ActualStar.beta_range line 665
  78. lemma OAI.KServer.ActualStar.b_range line 670
  79. lemma OAI.KServer.ActualStar.b_error line 674
  80. lemma OAI.KServer.ActualStar.parameter_gap line 679
  81. lemma OAI.KServer.ActualStar.α_mem line 686
  82. lemma OAI.KServer.ActualStar.α_feasible line 689
  83. lemma OAI.KServer.OutputConstants.eta_nonneg line 707
  84. lemma OAI.KServer.OutputConstants.eta_upper line 709
  85. lemma OAI.KServer.OutputConstants.beta_eta line 714
  86. lemma OAI.KServer.OutputConstants.dominant_room line 723
  87. lemma OAI.KServer.OutputConstants.regular_error line 728
  88. lemma OAI.KServer.OutputConstants.regular_room line 739
  89. lemma OAI.KServer.OutputConstants.side_room line 745
  90. lemma OAI.KServer.OutputConstants.residual_room line 756
  91. def OAI.KServer.ActualOutput.B line 780
  92. def OAI.KServer.ActualOutput.n line 781
  93. def OAI.KServer.ActualOutput.S line 782
  94. def OAI.KServer.ActualOutput.f line 783
  95. def OAI.KServer.ActualOutput.fc line 785
  96. def OAI.KServer.ActualOutput.flexcap line 787
  97. def OAI.KServer.ActualOutput.d line 789
  98. def OAI.KServer.ActualOutput.lower line 791
  99. def OAI.KServer.ActualOutput.T line 793
  100. def OAI.KServer.ActualOutput.e line 795
  101. def OAI.KServer.ActualOutput.D line 797
  102. lemma OAI.KServer.ActualOutput.S_nonneg line 800
  103. lemma OAI.KServer.ActualOutput.D_nonneg line 802
  104. lemma OAI.KServer.ActualOutput.mark_active line 804
  105. lemma OAI.KServer.ActualOutput.inactive line 807
  106. lemma OAI.KServer.ActualOutput.inactive_lower line 810
  107. lemma OAI.KServer.ActualOutput.inactive_f line 813
  108. lemma OAI.KServer.ActualOutput.lower_decomposition line 821
  109. lemma OAI.KServer.ActualOutput.child_size line 824
  110. lemma OAI.KServer.ActualOutput.lower_nonneg line 827
  111. lemma OAI.KServer.ActualOutput.d_bounds line 829
  112. lemma OAI.KServer.ActualOutput.inactive_d line 832
  113. lemma OAI.KServer.ActualOutput.regular_caps line 836
  114. lemma OAI.KServer.ActualOutput.dominant_caps line 849
  115. lemma OAI.KServer.ActualOutput.T_nonneg line 854
  116. lemma OAI.KServer.ActualOutput.e_bounds line 860
  117. lemma OAI.KServer.ActualOutput.DT_compare line 868