StateSpace

formal source

 107/-! ## The state space: free ℝ-module on `MultIndex` -/
 108
 109/-- The pre-Hilbert space: free `ℝ`-module on `MultIndex`. -/
 110abbrev StateSpace : Type := MultIndex →₀ ℝ
 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`. -/
 122def diagOp : StateSpace →ₗ[ℝ] StateSpace :=
 123  Finsupp.lsum ℝ (fun v => costAt v • Finsupp.lsingle v)
 124
 125/-- Action of `diagOp` on a basis element: `D(e_v) = costAt v · e_v`. -/
 126@[simp] theorem diagOp_single (v : MultIndex) (c : ℝ) :
 127    diagOp (Finsupp.single v c) = Finsupp.single v (costAt v * c) := by
 128  simp [diagOp, mul_comm]
 129
 130/-- The prime-shift operator `V_p`: maps `e_v` to `e_{v + δ_p}`,
 131    i.e., multiplication of the underlying rational by `p`.
 132
 133    Defined via `Finsupp.lmapDomain` shifting the index by `δ_p`. -/
 134def shiftOp (p : Nat.Primes) : StateSpace →ₗ[ℝ] StateSpace :=
 135  Finsupp.lmapDomain ℝ ℝ (fun v => v + Finsupp.single p 1)
 136
 137/-- Action of `shiftOp p` on a basis element. -/
 138@[simp] theorem shiftOp_single (p : Nat.Primes) (v : MultIndex) (c : ℝ) :
 139    shiftOp p (Finsupp.single v c)
 140      = Finsupp.single (v + Finsupp.single p 1) c := by