shiftInvOp_shiftOp

formal source

 208  congr 1
 209  abel
 210
 211theorem shiftInvOp_shiftOp (p : Nat.Primes) :
 212    shiftInvOp p ∘ₗ shiftOp p = LinearMap.id := by
 213  ext v
 214  simp only [LinearMap.coe_comp, Function.comp_apply,
 215             shiftOp_single, shiftInvOp_single, Finsupp.lsingle_apply,
 216             LinearMap.id_apply]
 217  congr 1
 218  abel
 219
 220/-! ## The candidate Hilbert--Pólya operator (algebraic part) -/
 221
 222/-- The off-diagonal piece for a single prime: `V_p + V_p^{-1}`.
 223    This is the "hopping" term in the multiplicative direction `p`. -/
 224def primeHop (p : Nat.Primes) : StateSpace →ₗ[ℝ] StateSpace :=
 225  shiftOp p + shiftInvOp p
 226
 227/-- The reciprocal involution maps `V_p + V_p^{-1}` to itself
 228    (consequence of intertwining shift and inverse shift). -/
 229theorem involutionOp_primeHop (p : Nat.Primes) :
 230    involutionOp ∘ₗ primeHop p = primeHop p ∘ₗ involutionOp := by
 231  unfold primeHop
 232  rw [LinearMap.comp_add, LinearMap.add_comp]
 233  rw [involutionOp_shiftOp, involutionOp_shiftInvOp]
 234  rw [add_comm (shiftInvOp p ∘ₗ involutionOp) (shiftOp p ∘ₗ involutionOp)]
 235
 236/-- The candidate Hilbert--Pólya operator with weights `λ : Nat.Primes → ℝ`,
 237    defined on a finite set `S ⊆ Nat.Primes`:
 238    `T_S(λ) := D + ∑_{p ∈ S} λ p · (V_p + V_p^{-1})`.
 239
 240    The full operator (sum over all primes) requires choosing a Hilbert space
 241    closure and analyzing convergence; we work here at the algebraic level