totalAccessCost

formal source

  23/-! ## §1  Local Cache Theorem (Theorem 3.1) -/
  24
  25/-- Total access cost without cache: weighted sum of access frequencies × distances. -/
  26noncomputable def totalAccessCost (n : ℕ) (freq : Fin n → ℝ) (dist : Fin n → ℝ) : ℝ :=
  27  ∑ i : Fin n, freq i * dist i
  28
  29/-- Cached access cost: cached items accessed at distance ε, uncached at full distance,
  30    plus maintenance overhead α per cached item. -/
  31noncomputable def cachedAccessCost (n : ℕ) (freq : Fin n → ℝ) (dist : Fin n → ℝ)
  32    (cached : Fin n → Prop) [DecidablePred cached]
  33    (ε α : ℝ) (K : ℕ) : ℝ :=
  34  (∑ i : Fin n, if cached i then freq i * ε else freq i * dist i) + α * K
  35
  36/-- **LOCAL CACHE THEOREM (Theorem 3.1)**
  37
  38If there exists a frequently-accessed distant item v* such that
  39caching it saves more than the maintenance cost, then caching
  40strictly reduces total cost.
  41
  42Conditions:
  43  (A1) Non-uniformity: freq(v*) · dist(v*) is the dominant cost term
  44  (A2) Distance spread: dist(v*) > ε
  45  (A3) Positive maintenance: 0 < α < freq(v*) · (dist(v*) - ε) -/
  46theorem local_cache_benefit
  47    (freq_star dist_star ε α : ℝ)
  48    (_hε_pos : 0 < ε)
  49    (_hdist : ε < dist_star)
  50    (_hα_pos : 0 < α)
  51    (hα_lt : α < freq_star * (dist_star - ε))
  52    (_hfreq_pos : 0 < freq_star) :
  53    -- The cost reduction from caching v* is strictly positive
  54    freq_star * dist_star - (freq_star * ε + α) > 0 := by
  55  have h1 : freq_star * dist_star - freq_star * ε = freq_star * (dist_star - ε) := by ring
  56  linarith [hα_lt]