229theorem involutionOp_primeHop (p : Nat.Primes) : 230 involutionOp ∘ₗ primeHop p = primeHop p ∘ₗ involutionOp := by
proof body
Term-mode proof.
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 242 with a finite truncation. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.