involutionOp_single

formal source

 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
 179    This is the operator-level analog of the zeta functional equation's
 180    involution `s ↔ 1-s`. -/
 181theorem involutionOp_shiftOp (p : Nat.Primes) :
 182    involutionOp ∘ₗ shiftOp p = shiftInvOp p ∘ₗ involutionOp := by
 183  ext v
 184  simp only [LinearMap.coe_comp, Function.comp_apply,
 185             shiftOp_single, involutionOp_single, shiftInvOp_single,
 186             Finsupp.lsingle_apply]
 187  congr 1
 188  abel