pith. machine review for the scientific record. sign in
abbrev definition def or abbrev

StateSpace

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)

 110abbrev StateSpace : Type := MultIndex →₀ ℝ

proof body

Definition body.

 111
 112/-! ## The three operators
 113
 114We use `Finsupp.lsum` and similar mathlib constructions to define
 115linear endomorphisms of `StateSpace`.  The "basis vector" `e_v` is
 116`Finsupp.single v 1`. -/
 117
 118/-- The diagonal cost operator `D`: maps `e_v` to `J(toRat v) · e_v`.
 119
 120    Defined as the linear map sending each basis element `e_v` to
 121    `costAt v • e_v`. -/

used by (9)

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

depends on (18)

Lean names referenced from this declaration's body.