shiftInvOp_single

formal source

 145def shiftInvOp (p : Nat.Primes) : StateSpace →ₗ[ℝ] StateSpace :=
 146  Finsupp.lmapDomain ℝ ℝ (fun v => v - Finsupp.single p 1)
 147
 148@[simp] theorem shiftInvOp_single (p : Nat.Primes) (v : MultIndex) (c : ℝ) :
 149    shiftInvOp p (Finsupp.single v c)
 150      = Finsupp.single (v - Finsupp.single p 1) c := by
 151  simp [shiftInvOp, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
 152
 153/-- The reciprocal involution operator `U`: maps `e_v` to `e_{-v}`,
 154    corresponding to the multiplicative inversion `q ↦ 1/q`. -/
 155def involutionOp : StateSpace →ₗ[ℝ] StateSpace :=
 156  Finsupp.lmapDomain ℝ ℝ (fun v => -v)
 157
 158@[simp] theorem involutionOp_single (v : MultIndex) (c : ℝ) :
 159    involutionOp (Finsupp.single v c) = Finsupp.single (-v) c := by
 160  simp [involutionOp, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
 161
 162/-! ## Structural theorems -/
 163
 164/-- The reciprocal involution is involutive: `U ∘ U = id`. -/
 165theorem involutionOp_involutive : involutionOp ∘ₗ involutionOp = LinearMap.id := by
 166  ext v
 167  simp
 168
 169/-- The reciprocal involution commutes with the diagonal cost operator
 170    (consequence of `J(1/q) = J(q)`). -/
 171theorem involutionOp_diagOp_comm :
 172    involutionOp ∘ₗ diagOp = diagOp ∘ₗ involutionOp := by
 173  ext v
 174  simp [costAt_neg_eq]
 175
 176/-- The reciprocal involution intertwines the prime-shift with its
 177    inverse: `U ∘ V_p = V_p^{-1} ∘ U`.
 178