def
definition
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 145.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
142
143/-- The inverse prime-shift operator `V_p^{-1}`: maps `e_v` to
144 `e_{v - δ_p}` (division of the underlying rational by `p`). -/
145def shiftInvOp (p : Nat.Primes) : StateSpace →ₗ[ℝ] StateSpace :=
146 Finsupp.lmapDomain ℝ ℝ (fun v => v - Finsupp.single p 1)
147
148@[simp] theorem shiftInvOp_single (p : Nat.Primes) (v : MultIndex) (c : ℝ) :
149 shiftInvOp p (Finsupp.single v c)
150 = Finsupp.single (v - Finsupp.single p 1) c := by
151 simp [shiftInvOp, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
152
153/-- The reciprocal involution operator `U`: maps `e_v` to `e_{-v}`,
154 corresponding to the multiplicative inversion `q ↦ 1/q`. -/
155def involutionOp : StateSpace →ₗ[ℝ] StateSpace :=
156 Finsupp.lmapDomain ℝ ℝ (fun v => -v)
157
158@[simp] theorem involutionOp_single (v : MultIndex) (c : ℝ) :
159 involutionOp (Finsupp.single v c) = Finsupp.single (-v) c := by
160 simp [involutionOp, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
161
162/-! ## Structural theorems -/
163
164/-- The reciprocal involution is involutive: `U ∘ U = id`. -/
165theorem involutionOp_involutive : involutionOp ∘ₗ involutionOp = LinearMap.id := by
166 ext v
167 simp
168
169/-- The reciprocal involution commutes with the diagonal cost operator
170 (consequence of `J(1/q) = J(q)`). -/
171theorem involutionOp_diagOp_comm :
172 involutionOp ∘ₗ diagOp = diagOp ∘ₗ involutionOp := by
173 ext v
174 simp [costAt_neg_eq]
175