pith. machine review for the scientific record. sign in
theorem proved term proof

denseDomain_mem

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  57theorem denseDomain_mem (f : StateSpace) : f ∈ denseDomain := trivial

proof body

Term-mode proof.

  58
  59/-! ## Cost potential growth bound
  60
  61For the cost operator to have a discrete spectrum, the diagonal cost
  62potential `D(v) = J(toRat v)` must grow as `|v| → ∞`.  Since `J(p) ~ p/2`
  63and `c(v) = Σ_p v_p J(p)`, the growth rate depends on the multiplicative
  64index norm.
  65-/
  66
  67/-- A growth bound for the cost potential at a multiplicative index `v`
  68    with respect to a chosen norm `‖v‖`.  We state the abstract bound
  69    rather than fixing a specific norm. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.