OAI/Combinatorics/KServer/JointBudget.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Geometric absorption on the same numbered tree used for metric rounding.

  1. abbrev OAI.KServer.JointBudget.Node line 17
  2. def OAI.KServer.JointBudget.stepQuota line 19
  3. def OAI.KServer.JointBudget.stepKey line 23
  4. lemma OAI.KServer.JointBudget.stepQuota_nonneg line 26
  5. lemma OAI.KServer.JointBudget.stepKey_nonneg line 30
  6. lemma OAI.KServer.JointBudget.quota_tree line 34
  7. lemma OAI.KServer.JointBudget.geo_half line 80
  8. lemma OAI.KServer.JointBudget.key_tree line 85
  9. lemma OAI.KServer.JointBudget.quota_bound line 98
  10. lemma OAI.KServer.JointBudget.park_bound line 117
  11. lemma OAI.KServer.EmbeddedCost.exchange line 140
  12. def OAI.KServer.EmbeddedCost.opt line 154
  13. def OAI.KServer.EmbeddedCost.inventory line 156
  14. def OAI.KServer.EmbeddedCost.tierMove line 157
  15. def OAI.KServer.EmbeddedCost.tierCoefficient line 163
  16. lemma OAI.KServer.EmbeddedCost.tier_all line 166
  17. def OAI.KServer.EmbeddedCost.heavyDrift line 199
  18. def OAI.KServer.EmbeddedCost.heavyMove line 201
  19. def OAI.KServer.EmbeddedCost.heavyCoefficient line 207
  20. lemma OAI.KServer.EmbeddedCost.movement_average line 210
  21. lemma OAI.KServer.EmbeddedCost.far_scales_general line 221
  22. lemma OAI.KServer.EmbeddedCost.nonheavy_scales line 233
  23. lemma OAI.KServer.EmbeddedCost.heavy_far_all line 251
  24. lemma OAI.KServer.EmbeddedCost.heavy_nonheavy_all line 260
  25. lemma OAI.KServer.EmbeddedCost.heavy_annulus_all line 276
  26. lemma OAI.KServer.EmbeddedCost.heavy_all line 299
  27. lemma OAI.KServer.PriorityKeys.indicator_triangle line 334
  28. lemma OAI.KServer.PriorityKeys.indicator_chain line 344
  29. lemma OAI.KServer.PriorityKeys.stages_total line 354
  30. lemma OAI.KServer.EmbeddedCost.indicator_ne_comm line 399
  31. lemma OAI.KServer.EmbeddedCost.map_edit line 402
  32. def OAI.KServer.EmbeddedCost.mappedCross line 416
  33. lemma OAI.KServer.EmbeddedCost.physical_cross line 421
  34. lemma OAI.KServer.EmbeddedCost.mapped_step line 435
  35. lemma OAI.KServer.EmbeddedCost.mapped_step_mean line 451
  36. def OAI.KServer.EmbeddedCost.spatialCoefficient line 485
  37. def OAI.KServer.EmbeddedCost.spatialMove line 487
  38. lemma OAI.KServer.EmbeddedCost.spatial_all line 493
  39. def OAI.KServer.EmbeddedCost.keyMove line 508
  40. lemma OAI.KServer.EmbeddedCost.key_move_decompose line 514
  41. lemma OAI.KServer.EmbeddedCost.embedding_all line 534
  42. def OAI.KServer.JointEmbedding.scaleCost line 562
  43. lemma OAI.KServer.JointEmbedding.cross_mean line 566
  44. lemma OAI.KServer.JointEmbedding.total_key line 582
  45. lemma OAI.KServer.JointEmbedding.hidden_cost line 594
  46. lemma OAI.KServer.JointEmbedding.radius_reverse line 604
  47. lemma OAI.KServer.JointEmbedding.key_bound line 611