OAI/Combinatorics/KServer/AnchorTravel.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

The actual retained heavy label, not an assumed anchor motion rule.

  1. lemma OAI.KServer.HeavyAnchorDynamics.key_iff line 15
  2. lemma OAI.KServer.HeavyAnchorDynamics.anchor_eq line 33
  3. lemma OAI.KServer.HeavyAnchorDynamics.common_centers line 44
  4. def OAI.KServer.HeavyAnchorDynamics.slot line 85
  5. lemma OAI.KServer.HeavyAnchorDynamics.level_heavy line 87
  6. lemma OAI.KServer.HeavyAnchorDynamics.region_ball line 122
  7. lemma OAI.KServer.HeavyAnchorDynamics.heavy_mass_comparison line 138
  8. def OAI.KServer.AnchorTravel.ramp line 173
  9. lemma OAI.KServer.AnchorTravel.ramp_nonneg line 175
  10. lemma OAI.KServer.AnchorTravel.ramp_le_one line 176
  11. lemma OAI.KServer.AnchorTravel.ramp_zero line 177
  12. lemma OAI.KServer.AnchorTravel.ramp_one line 180
  13. lemma OAI.KServer.AnchorTravel.ramp_lipschitz line 184
  14. theorem OAI.KServer.AnchorTravel.ramp_motion line 194

    Source documentation

    Actual pointwise metric motion inequality, including the saturation cutoff. No independence between the old point and an updated history is required.

    theorem ramp_motion {a y z : Y} {r c : ℝ} (hr : 0 < r) (hc : 0 ≤ c) :
    r*c*max 0 (ramp (dist a z/r)-ramp (dist a y/r)) ≤
      if dist a y < 7*r then dist y z/3*c else 0 := by
…

    Mentions: OAI.KServer.AnchorTravel.ramp

  15. lemma OAI.KServer.AnchorTravel.inner_ramp line 219

    Source documentation

    On the heavy inner ball the new ramp vanishes and the old ramp is one.

    lemma inner_ramp {a x z : Y} {r γ : ℝ} (hr : 0 < r) (hγ : γ < 1/100)
    (hax : 8*r < dist a x) (hxz : dist x z ≤ γ*r) :
    ramp (dist x z/r)=0 ∧ ramp (dist a z/r)=1 := by
…

    Mentions: OAI.KServer.AnchorTravel.ramp

  16. def OAI.KServer.AnchorTravel.integral line 234
  17. def OAI.KServer.AnchorTravel.mass line 237
  18. lemma OAI.KServer.AnchorTravel.integral_bounds line 240
  19. theorem OAI.KServer.AnchorTravel.heavy_integral_drop line 250

    Source documentation

    The heavy condition gives the actual unnormalized potential drop on a retained reuse, with C the new heavy key's entire ball and S its inner ball.

    theorem heavy_integral_drop {w : Y → ℝ} {C S : Finset Y} {a x : Y} {r γ δ : ℝ}
    (hw : ∀ z ∈ C, 0 ≤ w z) (hSC : S ⊆ C)
    (hr : 0 < r) (hγ : γ < 1/100) (hax : 8*r < dist a x)
    (hS : ∀ z ∈ S, dist x z ≤ γ*r)
    (hheavy : mass w C ≤ (1+δ)*mass w S) :
    integral w C x r-integral w C a r ≤ -(1-δ)*mass w S := by
…

    Mentions: OAI.KServer.AnchorTravel.mass, OAI.KServer.AnchorTravel.integral

  20. theorem OAI.KServer.AnchorTravel.retained_anchor_payment line 277

    Source documentation

    Exact rho=6/5 normalization. H≥1 is used in the held-size comparison.

    theorem retained_anchor_payment {w : Y → ℝ} {C S : Finset Y} {a x : Y}
    {r γ δ u b : ℝ} (hw : ∀ z ∈ C, 0 ≤ w z) (hSC : S ⊆ C)
    (hr : 0 < r) (hγ : γ < 1/100) (hδ : δ ≤ 1/100)
    (hax : 8*r < dist a x) (hS : ∀ z ∈ S, dist x z ≤ γ*r)
    (hheavy : mass w C ≤ (1+δ)*mass w S) (hH : 1 ≤ mass w S)
    (hu : 0 < u) (href : u ≤ (6/5)*(1+mass w C)) (hb : 0 ≤ b) :
    r*b/u*(integral w C x r-integral w C a r) ≤ -r*b/4 := by
…

    Mentions: OAI.KServer.AnchorTravel.mass, OAI.KServer.AnchorTravel.integral

  21. theorem OAI.KServer.AnchorTravel.normalization_refresh line 302

    Source documentation

    Positive normalization-refresh jumps are paid by the old-plus-new size charge; no invalid comparison of the new integral to the old reference is used.

    theorem normalization_refresh {r b I s u C : ℝ}
    (hr : 0 ≤ r) (hb : 0 ≤ b) (hI : 0 ≤ I) (hs : 0 < s) (hu : 0 < u)
    (hIs : I ≤ s) (hbu : b ≤ (6/5)*C*u) :
    r*b*I*(1/s-1/u) ≤ (6/5)*C*r*u := by
…
  22. def OAI.KServer.HeavyAnchorDynamics.present line 335
  23. def OAI.KServer.HeavyAnchorDynamics.cell line 340
  24. lemma OAI.KServer.HeavyAnchorDynamics.absent_cell line 344
  25. lemma OAI.KServer.HeavyAnchorDynamics.present_cell line 354
  26. lemma OAI.KServer.HeavyAnchorDynamics.moving_drop line 363
  27. def OAI.KServer.HeavyAnchorDynamics.selected line 409
  28. lemma OAI.KServer.HeavyAnchorDynamics.selected_data line 415
  29. lemma OAI.KServer.HeavyAnchorDynamics.selected_close line 432
  30. lemma OAI.KServer.HeavyAnchorDynamics.selected_contains line 447
  31. def OAI.KServer.AnchorTravel.term line 473
  32. def OAI.KServer.AnchorTravel.cutoff line 478
  33. lemma OAI.KServer.AnchorTravel.cutoff_nonneg line 483
  34. lemma OAI.KServer.AnchorTravel.term_bounds line 489
  35. lemma OAI.KServer.AnchorTravel.term_motion line 500
  36. theorem OAI.KServer.AnchorTravel.member_drift line 525
  37. lemma OAI.KServer.AnchorTravel.conditional_average line 555
  38. def OAI.KServer.AnchorTravel.slotIntegral line 566
  39. lemma OAI.KServer.AnchorTravel.integral_term line 569
  40. lemma OAI.KServer.AnchorTravel.slotIntegral_nonneg line 580
  41. lemma OAI.KServer.AnchorTravel.slotIntegral_bound line 585
  42. lemma OAI.KServer.AnchorTravel.expected_membership line 592
  43. lemma OAI.KServer.AnchorTravel.raw_bounds line 607
  44. lemma OAI.KServer.AnchorTravel.reference_step line 628
  45. lemma OAI.KServer.AnchorTravel.park_step line 644
  46. lemma OAI.KServer.AnchorTravel.anchor_step line 655
  47. lemma OAI.KServer.AnchorTravel.chronological_step line 683
  48. def OAI.KServer.AnchorTravel.familyTest line 707
  49. def OAI.KServer.AnchorTravel.familyIntegral line 710
  50. lemma OAI.KServer.AnchorTravel.familyIntegral_eq line 713
  51. lemma OAI.KServer.AnchorTravel.expected_step line 718
  52. lemma OAI.KServer.AnchorTravel.chronological_telescope line 749
  53. lemma OAI.KServer.AnchorTravel.slot_stage line 771
  54. lemma OAI.KServer.KeysAdapted.heavy_anchor_adapted line 812
  55. lemma OAI.KServer.KeysAdapted.tier_anchor_adapted line 821
  56. lemma OAI.KServer.KeysAdapted.anchor_adapted line 848