shiftOp_single

formal source

 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
 141  simp [shiftOp, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
 142
 143/-- The inverse prime-shift operator `V_p^{-1}`: maps `e_v` to
 144    `e_{v - δ_p}` (division of the underlying rational by `p`). -/
 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