SchrodingerTrace.lean

1 import PaperXI.SchrodingerOperator
2 import Mathlib.LinearAlgebra.Trace
3 import Mathlib.NumberTheory.GaussSum
4 import Mathlib.Analysis.Complex.Basic
5 import Mathlib.Tactic
6 
7 /-! Character support for the literal finite function-space Schrödinger operators. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.SchrodingerTrace
11 open scoped Classical
12 
13 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
14 
15 /-- A nonzero linear functional onto the scalar field is surjective. -/
16 theorem functional_surjective {ξ : X →ₗ[K] K} (hξ : ξ ≠ 0) :
17     Function.Surjective ξ := by
18   obtain ⟨u, hu⟩ := DFunLike.ne_iff.mp hξ
19   change ξ u ≠ 0 at hu
20   intro a
21   refine ⟨(a / ξ u) • u, ?_⟩
22   simp [map_smul, smul_eq_mul, hu]
23 
24 /-- A nontrivial character remains nontrivial after a nonzero functional. -/
25 theorem functional_character_ne_one {ψ : AddChar K ℂ} (hψ : ψ ≠ 1)
26     {ξ : X →ₗ[K] K} (hξ : ξ ≠ 0) :
27     ψ.compAddMonoidHom ξ.toAddMonoidHom ≠ 1 := by
28   intro h
29   apply hψ
30   ext a
31   obtain ⟨u, rfl⟩ := functional_surjective hξ a
32   have hu := congrArg (fun χ : AddChar X ℂ => χ u) h
33   simpa using hu
34 
35 variable [Fintype X]
36 
37 /-- Exact finite Fourier cancellation for every nonzero scalar functional. -/
38 theorem sum_functional_character {ψ : AddChar K ℂ} (hψ : ψ ≠ 1)
39     {ξ : X →ₗ[K] K} (hξ : ξ ≠ 0) : (∑ u : X, ψ (ξ u)) = 0 := by
40   exact AddChar.sum_eq_zero_of_ne_one (functional_character_ne_one hψ hξ)
41 
42 /-- The diagonal matrix entries are computed in the actual delta-function basis. -/
43 theorem operator_diagonal (ψ : AddChar K ℂ) (x : X) (ξ : X →ₗ[K] K)
44     (z : K) (u : X) :
45     LinearMap.toMatrix (Pi.basisFun ℂ X) (Pi.basisFun ℂ X)
46       (Schrodinger.operator ψ x ξ z) u u =
47       if x = 0 then ψ (z + ξ u) else 0 := by
48   classical
49   rw [LinearMap.toMatrix_apply, Pi.basisFun_repr, Schrodinger.operator_apply,
50     Pi.basisFun_apply]
51   by_cases hx : x = 0
52   · subst x
53     simp
54   · have hux : u + x ≠ u := by simpa using hx
55     simp [hx, hux]
56 
57 /-- Translation by a nonzero vector has no diagonal contribution. -/
58 theorem trace_of_translation_ne_zero (ψ : AddChar K ℂ) {x : X} (hx : x ≠ 0)
59     (ξ : X →ₗ[K] K) (z : K) :
60     LinearMap.trace ℂ (X → ℂ) (Schrodinger.operator ψ x ξ z) = 0 := by
61   classical
62   rw [LinearMap.trace_eq_matrix_trace ℂ (Pi.basisFun ℂ X)]
63   simp [Matrix.trace, hx]
64 
65 /-- Pure modulation has trace equal to its literal finite character sum. -/
66 theorem trace_of_translation_zero (ψ : AddChar K ℂ) (ξ : X →ₗ[K] K) (z : K) :
67     LinearMap.trace ℂ (X → ℂ) (Schrodinger.operator ψ 0 ξ z) =
68       ψ z * ∑ u : X, ψ (ξ u) := by
69   classical
70   rw [LinearMap.trace_eq_matrix_trace ℂ (Pi.basisFun ℂ X)]
71   simp [Matrix.trace, ψ.map_add_eq_mul, Finset.mul_sum]
72 
73 /-- Proposition 7.3: exact character support, without assuming the trace formula. -/
74 theorem character_support {ψ : AddChar K ℂ} (hψ : ψ ≠ 1)
75     (x : X) (ξ : X →ₗ[K] K) (z : K) :
76     LinearMap.trace ℂ (X → ℂ) (Schrodinger.operator ψ x ξ z) =
77       if x = 0 ∧ ξ = 0 then (Fintype.card X : ℂ) * ψ z else 0 := by
78   classical
79   by_cases hx : x = 0
80   · subst x
81     rw [trace_of_translation_zero]
82     by_cases hξ : ξ = 0
83     · subst ξ
84       simp [mul_comm]
85     · simp [hξ, sum_functional_character hψ hξ]
86   · simp [hx, trace_of_translation_ne_zero ψ hx]
87 
88 end PaperXI.SchrodingerTrace

Back to source controls