involutionOp_primeHop

formal source

 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
 242    with a finite truncation. -/
 243def candidateOp (S : Finset Nat.Primes) (lam : Nat.Primes → ℝ) :
 244    StateSpace →ₗ[ℝ] StateSpace :=
 245  diagOp + S.sum (fun p => lam p • primeHop p)
 246
 247/-- Auxiliary: involution commutes with weighted sum of `primeHop` over a finset.
 248    Proved by induction on the finset. -/
 249private theorem involutionOp_sum_primeHop
 250    (S : Finset Nat.Primes) (lam : Nat.Primes → ℝ) :
 251    involutionOp ∘ₗ S.sum (fun p => lam p • primeHop p)
 252      = S.sum (fun p => lam p • primeHop p) ∘ₗ involutionOp := by
 253  classical
 254  refine Finset.induction_on S ?_ ?_
 255  · simp
 256  · intro p S hp ih
 257    rw [Finset.sum_insert hp]
 258    rw [LinearMap.comp_add, LinearMap.add_comp, ih]
 259    congr 1