OAI/Combinatorics/KServer/JointTravel.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Literal retained-heavy anchor data and chronological payment on the one joint request/tape experiment.

  1. abbrev OAI.KServer.JointHeavy.J line 18
  2. def OAI.KServer.JointHeavy.key line 21
  3. def OAI.KServer.JointHeavy.anchor line 24
  4. def OAI.KServer.JointHeavy.b line 27
  5. def OAI.KServer.JointHeavy.u line 30
  6. def OAI.KServer.JointHeavy.c line 33
  7. def OAI.KServer.JointHeavy.present line 36
  8. lemma OAI.KServer.JointHeavy.cell_eq line 39
  9. lemma OAI.KServer.JointHeavy.mass_eq line 47
  10. lemma OAI.KServer.JointHeavy.b_nonneg line 57
  11. lemma OAI.KServer.JointHeavy.u_pos line 59
  12. lemma OAI.KServer.JointHeavy.c_bounds line 61
  13. lemma OAI.KServer.JointHeavy.absent_band line 65
  14. lemma OAI.KServer.JointHeavy.integral_eq line 72
  15. lemma OAI.KServer.JointHeavy.slot_payment line 78
  16. lemma OAI.KServer.JointHeavy.key_adapted line 151
  17. lemma OAI.KServer.JointHeavy.anchor_adapted line 159
  18. lemma OAI.KServer.JointHeavy.c_adapted line 167
  19. lemma OAI.KServer.JointHeavy.prepared_adapted line 173
  20. lemma OAI.KServer.JointHeavy.current_adapted line 179
  21. def OAI.KServer.JointHeavy.travel line 184
  22. def OAI.KServer.JointHeavy.charge line 188
  23. def OAI.KServer.JointHeavy.potential line 192
  24. lemma OAI.KServer.JointHeavy.stage_payment line 195
  25. lemma OAI.KServer.JointHeavy.expected_payment line 209
  26. def OAI.KServer.JointHeavy.selected line 241
  27. lemma OAI.KServer.JointHeavy.selected_term line 244
  28. lemma OAI.KServer.JointHeavy.cutoff_sum line 266
  29. lemma OAI.KServer.KeyReferences.refresh_nonneg line 325
  30. lemma OAI.KServer.KeyReferences.count_variation line 334
  31. lemma OAI.KServer.KeyReferences.refresh_all line 342
  32. lemma OAI.KServer.KeyReferences.refresh_subset line 365
  33. lemma OAI.KServer.PrefixTree.disjoint_variation line 388
  34. lemma OAI.KServer.PrefixTree.bands_disjoint line 405
  35. lemma OAI.KServer.PrefixTree.band_variation line 416
  36. lemma OAI.KServer.JointHeavy.potential_bounds line 442
  37. lemma OAI.KServer.JointHeavy.heavy_eq_of_map_eq line 446
  38. lemma OAI.KServer.JointHeavy.heavy_cross_le line 465
  39. lemma OAI.KServer.JointHeavy.travel_raw line 483
  40. lemma OAI.KServer.JointHeavy.slot_injective line 534
  41. lemma OAI.KServer.JointHeavy.refresh_bound line 538
  42. lemma OAI.KServer.JointHeavy.band_variation_bound line 567
  43. lemma OAI.KServer.JointHeavy.charge_bound line 575
  44. lemma OAI.KServer.JointHistory.prefix_of_take_eq line 618
  45. def OAI.KServer.JointHistory.Observed line 628
  46. lemma OAI.KServer.JointHistory.observed_true line 632
  47. lemma OAI.KServer.JointHistory.observed_history line 638
  48. def OAI.KServer.JointHistory.q line 644
  49. lemma OAI.KServer.JointHistory.q_eq line 649
  50. lemma OAI.KServer.JointHistory.q_nonneg line 656
  51. lemma OAI.KServer.JointHistory.q_park_nonneg line 663
  52. lemma OAI.KServer.JointHistory.q_root line 671
  53. def OAI.KServer.JointHistory.anchors line 677
  54. lemma OAI.KServer.JointHistory.anchors_adapted line 680
  55. def OAI.KServer.JointHistory.a line 691
  56. lemma OAI.KServer.JointHistory.a_eq line 694