def
definition
def or abbrev
cachedAccessCost
show as:
view Lean formalization →
formal statement (Lean)
31noncomputable def cachedAccessCost (n : ℕ) (freq : Fin n → ℝ) (dist : Fin n → ℝ)
32 (cached : Fin n → Prop) [DecidablePred cached]
33 (ε α : ℝ) (K : ℕ) : ℝ :=
proof body
Definition body.
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*) - ε) -/