SchrodingerUnitary.lean

1 import PaperXI.SchrodingerOperator
2 import Mathlib.NumberTheory.GaussSum
3 import Mathlib.Analysis.Complex.Basic
4 import Mathlib.Tactic
5 
6 /-! The literal Schrödinger operators preserve the usual finite sum Hermitian pairing. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.SchrodingerUnitary
10 open scoped Classical
11 
12 variable {K : Type*} [Field K] [Fintype K]
13 
14 /-- Finite-field additive characters take values on the unit circle. -/
15 theorem conjugate_character (ψ : AddChar K ℂ) (a : K) :
16     star (ψ a) = ψ (-a) := by
17   simpa only [AddChar.inv_apply, starRingEnd_apply] using
18     AddChar.starComp_apply (Nat.pos_of_ne_zero (CharP.ringChar_ne_zero_of_finite K)) a
19 
20 /-- The phase factor contributes one to the Hermitian pairing. -/
21 theorem conjugate_mul_character (ψ : AddChar K ℂ) (a : K) :
22     star (ψ a) * ψ a = 1 := by
23   rw [conjugate_character, ← ψ.map_add_eq_mul]
24   simp
25 
26 variable {X : Type*} [AddCommGroup X] [Module K X] [Fintype X]
27 
28 /-- Every literal Schrödinger operator preserves the finite sum Hermitian pairing. -/
29 theorem pairing_invariant (ψ : AddChar K ℂ) (x : X) (ξ : X →ₗ[K] K)
30     (z : K) (f g : X → ℂ) :
31     (∑ u : X, star (Schrodinger.operator ψ x ξ z f u) *
32       Schrodinger.operator ψ x ξ z g u) = ∑ u : X, star (f u) * g u := by
33   calc
34     _ = ∑ u : X, star (f (u + x)) * g (u + x) := by
35       apply Finset.sum_congr rfl
36       intro u _
37       simp only [Schrodinger.operator_apply, star_mul]
38       calc
39         _ = (star (ψ (z + ξ u + (2 : K)⁻¹ * ξ x)) *
40           ψ (z + ξ u + (2 : K)⁻¹ * ξ x)) *
41           (star (f (u + x)) * g (u + x)) := by ring
42         _ = _ := by rw [conjugate_mul_character, one_mul]
43     _ = _ := Fintype.sum_bijective _ (AddGroup.addRight_bijective x) _ _ (fun _ => rfl)
44 
45 end PaperXI.SchrodingerUnitary

Back to source controls