def definition def or abbrev

`totalAccessCost`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  26noncomputable def totalAccessCost (n : ℕ) (freq : Fin n → ℝ) (dist : Fin n → ℝ) : ℝ :=

proof body

Definition body.

  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. -/

depends on (2)

Lean names referenced from this declaration's body.

cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use