pith. machine review for the scientific record. sign in
theorem proved term proof

involutionOp_sum_primeHop

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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
 260    rw [LinearMap.comp_smul, LinearMap.smul_comp]
 261    congr 1
 262    exact involutionOp_primeHop p
 263
 264/-- The candidate operator commutes with the reciprocal involution.
 265    This is the Hilbert--Pólya-style structural symmetry: any spectrum
 266    of the (closure of the) operator decomposes into eigenspaces of
 267    the involution, mirroring `s ↔ 1-s`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.