`involutionOp_shiftOp`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
domain: NumberTheory
line: 181 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.HilbertPolyaCandidate on GitHub at line 181.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 178
 179    This is the operator-level analog of the zeta functional equation's
 180    involution `s ↔ 1-s`. -/
 181theorem involutionOp_shiftOp (p : Nat.Primes) :
 182    involutionOp ∘ₗ shiftOp p = shiftInvOp p ∘ₗ involutionOp := by
 183  ext v
 184  simp only [LinearMap.coe_comp, Function.comp_apply,
 185             shiftOp_single, involutionOp_single, shiftInvOp_single,
 186             Finsupp.lsingle_apply]
 187  congr 1
 188  abel
 189
 190/-- Symmetric form of the previous: `U ∘ V_p^{-1} = V_p ∘ U`. -/
 191theorem involutionOp_shiftInvOp (p : Nat.Primes) :
 192    involutionOp ∘ₗ shiftInvOp p = shiftOp p ∘ₗ involutionOp := by
 193  ext v
 194  simp only [LinearMap.coe_comp, Function.comp_apply,
 195             shiftInvOp_single, involutionOp_single, shiftOp_single,
 196             Finsupp.lsingle_apply]
 197  congr 1
 198  abel
 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) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.