involutionOp_diagOp_comm

formal source

 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
 189
 190/-- Symmetric form of the previous: `U ∘ V_p^{-1} = V_p ∘ U`. -/
 191theorem involutionOp_shiftInvOp (p : Nat.Primes) :
 192    involutionOp ∘ₗ shiftInvOp p = shiftOp p ∘ₗ involutionOp := by
 193  ext v
 194  simp only [LinearMap.coe_comp, Function.comp_apply,
 195             shiftInvOp_single, involutionOp_single, shiftOp_single,
 196             Finsupp.lsingle_apply]
 197  congr 1
 198  abel
 199
 200/-- The shift and inverse-shift compose to the identity (formal unitarity
 201    of `V_p`). -/