theorem
proved
involutionOp_shiftInvOp
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.HilbertPolyaCandidate on GitHub at line 191.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
comp_apply -
of -
compose -
of -
identity -
of -
of -
of -
and -
Primes -
involutionOp -
involutionOp_single -
shiftInvOp -
shiftInvOp_single -
shiftOp -
shiftOp_single -
identity
used by
formal source
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) :
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