theorem
proved
shiftOp_shiftInvOp
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.HilbertPolyaCandidate on GitHub at line 202.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
199
200/-- The shift and inverse-shift compose to the identity (formal unitarity
201 of `V_p`). -/
202theorem shiftOp_shiftInvOp (p : Nat.Primes) :
203 shiftOp p ∘ₗ shiftInvOp p = LinearMap.id := by
204 ext v
205 simp only [LinearMap.coe_comp, Function.comp_apply,
206 shiftInvOp_single, shiftOp_single, Finsupp.lsingle_apply,
207 LinearMap.id_apply]
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]