MovingFrames.lean

1 module
2 public import Mathlib.Analysis.Calculus.Deriv.Mul
3 public import Mathlib.Analysis.Calculus.Deriv.Star
4 public import Mathlib.Analysis.Calculus.Deriv.Add
5 public import Mathlib.LinearAlgebra.Matrix.ConjTranspose
6 public import Mathlib.Analysis.Complex.Basic
7 public import Mathlib.Tactic.Abel
8 /-! Author: Komorebi P. Paper VII second block, Theorem 6.1.
9 Actual differentiated coordinates y = U* psi and the corrected Hamiltonian. -/
10 public section
11 set_option autoImplicit false
12 namespace KomorebiPaperVII.MovingFrames
13 open scoped BigOperators Matrix
14 variable {n : Type*} [Fintype n]
15 theorem matrix_product_derivative (A B : ℝ → Matrix n n ℂ)
16     (dA dB : Matrix n n ℂ) (t : ℝ)
17     (ha : ∀ i j, HasDerivAt (fun s => A s i j) (dA i j) t)
18     (hb : ∀ i j, HasDerivAt (fun s => B s i j) (dB i j) t) (i j : n) :
19     HasDerivAt (fun s => (A s * B s) i j) ((dA * B t + A t * dB) i j) t := by
20   simpa only [Matrix.mul_apply, Matrix.add_apply, Pi.mul_apply, Finset.sum_add_distrib] using
21     HasDerivAt.fun_sum (u := Finset.univ) (fun k _ => (ha i k).mul (hb k j))
22 
23 theorem matrix_vector_derivative (A : ℝ → Matrix n n ℂ) (y : ℝ → n → ℂ)
24     (dA : Matrix n n ℂ) (dy : n → ℂ) (t : ℝ)
25     (ha : ∀ i j, HasDerivAt (fun s => A s i j) (dA i j) t)
26     (hy : ∀ i, HasDerivAt (fun s => y s i) (dy i) t) (i : n) :
27     HasDerivAt (fun s => (A s *ᵥ y s) i) ((dA *ᵥ y t + A t *ᵥ dy) i) t := by
28   simpa only [Matrix.mulVec, dotProduct, Pi.add_apply, Pi.mul_apply, Finset.sum_add_distrib] using
29     HasDerivAt.fun_sum (u := Finset.univ) (fun j _ => (ha i j).mul (hy j))
30 
31 omit [Fintype n] in
32 theorem adjoint_derivative (U : ℝ → Matrix n n ℂ) (dU : Matrix n n ℂ) (t : ℝ)
33     (hu : ∀ i j, HasDerivAt (fun s => U s i j) (dU i j) t) (i j : n) :
34     HasDerivAt (fun s => (U s).conjTranspose i j) (dU.conjTranspose i j) t := by
35   exact (hu j i).star
36 
37 theorem differentiated_unitarity [DecidableEq n]
38     (U : ℝ → Matrix n n ℂ) (dU : Matrix n n ℂ) (t : ℝ)
39     (hu : ∀ i j, HasDerivAt (fun s => U s i j) (dU i j) t)
40     (hunit : ∀ s, (U s).conjTranspose * U s = 1) :
41     dU.conjTranspose * U t + (U t).conjTranspose * dU = 0 := by
42   ext i j
43   have h := matrix_product_derivative (fun s => (U s).conjTranspose) U
44     dU.conjTranspose dU t (adjoint_derivative U dU t hu) hu i j
45   have heq : (fun s => ((U s).conjTranspose * U s) i j) =
46       fun _ => (1 : Matrix n n ℂ) i j := by
47     funext s
48     rw [hunit]
49   rw [heq] at h
50   exact h.unique (hasDerivAt_const t ((1 : Matrix n n ℂ) i j))
51 
52 theorem frame_velocity_skew [DecidableEq n]
53     (U : ℝ → Matrix n n ℂ) (dU : Matrix n n ℂ) (t : ℝ)
54     (hu : ∀ i j, HasDerivAt (fun s => U s i j) (dU i j) t)
55     (hunit : ∀ s, (U s).conjTranspose * U s = 1) :
56     ((U t).conjTranspose * dU).conjTranspose = -((U t).conjTranspose * dU) := by
57   rw [Matrix.conjTranspose_mul, Matrix.conjTranspose_conjTranspose]
58   exact (add_eq_zero_iff_eq_neg).mp (differentiated_unitarity U dU t hu hunit)
59 
60 theorem connection_hermitian [DecidableEq n]
61     (U : ℝ → Matrix n n ℂ) (dU : Matrix n n ℂ) (t : ℝ)
62     (hu : ∀ i j, HasDerivAt (fun s => U s i j) (dU i j) t)
63     (hunit : ∀ s, (U s).conjTranspose * U s = 1) :
64     ((-Complex.I) • ((U t).conjTranspose * dU)).conjTranspose =
65       (-Complex.I) • ((U t).conjTranspose * dU) := by
66   rw [Matrix.conjTranspose_smul, frame_velocity_skew U dU t hu hunit]
67   simp
68 
69 def effectiveHamiltonian (U H dU : Matrix n n ℂ) : Matrix n n ℂ :=
70   U.conjTranspose * H * U + (-Complex.I) • (U.conjTranspose * dU)
71 
72 theorem effective_hamiltonian_hermitian [DecidableEq n]
73     (U : ℝ → Matrix n n ℂ) (H dU : Matrix n n ℂ) (t : ℝ)
74     (hu : ∀ i j, HasDerivAt (fun s => U s i j) (dU i j) t)
75     (hunit : ∀ s, (U s).conjTranspose * U s = 1)
76     (hH : H.conjTranspose = H) :
77     (effectiveHamiltonian (U t) H dU).conjTranspose =
78       effectiveHamiltonian (U t) H dU := by
79   simp only [effectiveHamiltonian, Matrix.conjTranspose_add,
80     connection_hermitian U dU t hu hunit, Matrix.conjTranspose_mul,
81     Matrix.conjTranspose_conjTranspose, hH, Matrix.mul_assoc]
82 
83 theorem moving_frame_equation [DecidableEq n]
84     (U : ℝ → Matrix n n ℂ) (psi y : ℝ → n → ℂ)
85     (H dU : Matrix n n ℂ) (dpsi dy : n → ℂ) (t : ℝ)
86     (hu : ∀ i j, HasDerivAt (fun s => U s i j) (dU i j) t)
87     (hp : ∀ i, HasDerivAt (fun s => psi s i) (dpsi i) t)
88     (hy : ∀ i, HasDerivAt (fun s => y s i) (dy i) t)
89     (hunit : (U t).conjTranspose * U t = 1)
90     (hcoord : ∀ s, psi s = U s *ᵥ y s)
91     (hsch : Complex.I • dpsi = H *ᵥ psi t) :
92     Complex.I • dy = effectiveHamiltonian (U t) H dU *ᵥ y t := by
93   have hdiff : dpsi = dU *ᵥ y t + U t *ᵥ dy := by
94     funext i
95     have h := matrix_vector_derivative U y dU dy t hu hy i
96     have heq : (fun s => (U s *ᵥ y s) i) = fun s => psi s i := by
97       funext s
98       rw [hcoord]
99     rw [heq] at h
100     exact (h.unique (hp i)).symm
101   rw [hdiff, smul_add, hcoord t] at hsch
102   have he := congrArg (fun v => (U t).conjTranspose *ᵥ v) hsch
103   simp only [Matrix.mulVec_add, Matrix.mulVec_smul, Matrix.mulVec_mulVec,
104     hunit, Matrix.one_mulVec] at he
105   simp only [effectiveHamiltonian, Matrix.add_mulVec, neg_smul, Matrix.neg_mulVec, Matrix.smul_mulVec]
106   rw [← sub_eq_add_neg]
107   apply eq_sub_iff_add_eq.mpr
108   simpa only [add_comm, Matrix.mul_assoc] using he
109 
110 theorem moving_frame_coordinates [DecidableEq n]
111     (U : ℝ → Matrix n n ℂ) (psi : ℝ → n → ℂ)
112     (H dU : Matrix n n ℂ) (dpsi : n → ℂ) (t : ℝ)
113     (hu : ∀ i j, HasDerivAt (fun s => U s i j) (dU i j) t)
114     (hp : ∀ i, HasDerivAt (fun s => psi s i) (dpsi i) t)
115     (hleft : ∀ s, (U s).conjTranspose * U s = 1)
116     (hright : ∀ s, U s * (U s).conjTranspose = 1)
117     (hsch : Complex.I • dpsi = H *ᵥ psi t)
118     (hH : H.conjTranspose = H) :
119     let y := fun s => (U s).conjTranspose *ᵥ psi s
120     let dy := dU.conjTranspose *ᵥ psi t + (U t).conjTranspose *ᵥ dpsi
121     (∀ i, HasDerivAt (fun s => y s i) (dy i) t) ∧
122       Complex.I • dy = effectiveHamiltonian (U t) H dU *ᵥ y t ∧
123       (effectiveHamiltonian (U t) H dU).conjTranspose =
124         effectiveHamiltonian (U t) H dU := by
125   dsimp only
126   have hy := matrix_vector_derivative (fun s => (U s).conjTranspose) psi
127     dU.conjTranspose dpsi t (adjoint_derivative U dU t hu) hp
128   refine ⟨hy, ?_, effective_hamiltonian_hermitian U H dU t hu hleft hH⟩
129   apply moving_frame_equation U psi (fun s => (U s).conjTranspose *ᵥ psi s)
130     H dU dpsi _ t hu hp hy (hleft t) _ hsch
131   intro s
132   rw [Matrix.mulVec_mulVec, hright, Matrix.one_mulVec]
133 end KomorebiPaperVII.MovingFrames
134 
135 #print axioms KomorebiPaperVII.MovingFrames.matrix_product_derivative
136 #print axioms KomorebiPaperVII.MovingFrames.matrix_vector_derivative
137 #print axioms KomorebiPaperVII.MovingFrames.adjoint_derivative
138 #print axioms KomorebiPaperVII.MovingFrames.differentiated_unitarity
139 #print axioms KomorebiPaperVII.MovingFrames.frame_velocity_skew
140 #print axioms KomorebiPaperVII.MovingFrames.connection_hermitian
141 #print axioms KomorebiPaperVII.MovingFrames.effective_hamiltonian_hermitian
142 #print axioms KomorebiPaperVII.MovingFrames.moving_frame_equation
143 #print axioms KomorebiPaperVII.MovingFrames.moving_frame_coordinates

Back to source controls