ContourNaturality.lean

1 import KomorebiPaperVI.Algebra
2 import Mathlib.MeasureTheory.Integral.CircleIntegral
3 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
4 
5 /-! Author: Komorebi P. Actual finite contour integrals of matrix resolvents.
6 This module proves naturality for a supplied common contour representation. -/
7 namespace KomorebiPaperVI.ContourNaturality
8 open scoped BigOperators
9 open Complex
10 set_option backward.isDefEq.respectTransparency false
11 variable {I J K : Type*} [Fintype I] [Fintype J] [Fintype K] [DecidableEq I] [DecidableEq J]
12 
13 noncomputable def resolvent (A : Matrix I I ℂ) (z : ℂ) : Matrix I I ℂ :=
14   (Matrix.scalar I z-A)⁻¹
15 
16 noncomputable def circleMatrix (F : ℂ → Matrix I J ℂ) (c : ℂ) (r : ℝ) : Matrix I J ℂ :=
17   fun i j => ∮ z in C(c,r),F z i j
18 
19 omit [DecidableEq I] [DecidableEq J] [Fintype J] [Fintype K] in
20 theorem circle_mul_left (C : Matrix K I ℂ) (F : ℂ → Matrix I J ℂ) (c : ℂ) (r : ℝ)
21     (hF : ∀ i j,CircleIntegrable (fun z => F z i j) c r) :
22     C*circleMatrix F c r=circleMatrix (fun z => C*F z) c r := by
23   ext i j
24   simp only [Matrix.mul_apply,circleMatrix]
25   have hi (k : I) : CircleIntegrable (fun z => C i k*F z k j) c r := by
26     convert! (hF k j).const_smul (a := C i k) using 1
27   rw [circleIntegral.integral_fun_sum (fun k _ => hi k)]
28   simp only [circleIntegral.integral_const_mul]
29 
30 omit [DecidableEq I] [DecidableEq J] [Fintype I] [Fintype K] in
31 theorem circle_mul_right (C : Matrix J K ℂ) (F : ℂ → Matrix I J ℂ) (c : ℂ) (r : ℝ)
32     (hF : ∀ i j,CircleIntegrable (fun z => F z i j) c r) :
33     circleMatrix F c r*C=circleMatrix (fun z => F z*C) c r := by
34   ext i j
35   simp only [Matrix.mul_apply,circleMatrix]
36   have hi (k : J) : CircleIntegrable (fun z => F z i k*C k j) c r := by
37     have hc : CircleIntegrable (fun z => C k j*F z i k) c r := by
38       convert! (hF i k).const_smul (a := C k j) using 1
39     simpa only [mul_comm] using hc
40   rw [circleIntegral.integral_fun_sum (fun k _ => hi k)]
41   simp only [mul_comm,circleIntegral.integral_const_mul]
42 
43 omit [Fintype K] in
44 theorem resolvent_intertwines (C : Matrix J I ℂ) (A : Matrix I I ℂ) (B : Matrix J J ℂ)
45     (h : C*A=B*C) (z : ℂ) (hA : IsUnit (Matrix.scalar I z-A))
46     (hB : IsUnit (Matrix.scalar J z-B)) : C*resolvent A z=resolvent B z*C := by
47   have he := Algebra.rectangular_resolvent_identity C A B (resolvent A z) (resolvent B z) z
48     (fun i j => mul_comm _ _)
49     (Matrix.mul_nonsing_inv _ ((Matrix.isUnit_iff_isUnit_det _).mp hA))
50     (Matrix.nonsing_inv_mul _ ((Matrix.isUnit_iff_isUnit_det _).mp hB))
51   simpa only [h,sub_self,Matrix.mul_zero,Matrix.zero_mul,sub_eq_zero] using he
52 
53 noncomputable def calculus (A : Matrix I I ℂ) (f : ℂ → ℂ) (c : K → ℂ) (r : K → ℝ) :
54     Matrix I I ℂ := ((2*Real.pi:ℂ)*Complex.I)⁻¹ •
55       ∑ k,circleMatrix (fun z => f z • resolvent A z) (c k) (r k)
56 
57 theorem common_contour_naturality (C : Matrix J I ℂ) (A : Matrix I I ℂ) (B : Matrix J J ℂ)
58     (h : C*A=B*C) (f : ℂ → ℂ) (c : K → ℂ) (r : K → ℝ) (hr : ∀ k,0 ≤ r k)
59     (hA : ∀ k z,z∈Metric.sphere (c k) (r k) → IsUnit (Matrix.scalar I z-A))
60     (hB : ∀ k z,z∈Metric.sphere (c k) (r k) → IsUnit (Matrix.scalar J z-B))
61     (hiA : ∀ k i j,CircleIntegrable (fun z => f z*resolvent A z i j) (c k) (r k))
62     (hiB : ∀ k i j,CircleIntegrable (fun z => f z*resolvent B z i j) (c k) (r k)) :
63     C*calculus A f c r=calculus B f c r*C := by
64   unfold calculus
65   rw [Matrix.mul_smul,Matrix.smul_mul,Matrix.mul_sum,Matrix.sum_mul]
66   congr 1
67   apply Finset.sum_congr rfl
68   intro k _
69   have ha : ∀ i j,CircleIntegrable (fun z => (f z • resolvent A z) i j) (c k) (r k) := hiA k
70   have hb : ∀ i j,CircleIntegrable (fun z => (f z • resolvent B z) i j) (c k) (r k) := hiB k
71   rw [circle_mul_left C (fun z => f z • resolvent A z) _ _ ha,
72     circle_mul_right C (fun z => f z • resolvent B z) _ _ hb]
73   ext i j
74   apply circleIntegral.integral_congr (hr k)
75   intro z hz
76   have he := resolvent_intertwines C A B h z (hA k z hz) (hB k z hz)
77   change (C*(f z • resolvent A z)) i j=((f z • resolvent B z)*C) i j
78   rw [Matrix.mul_smul,Matrix.smul_mul,he]
79 
80 end KomorebiPaperVI.ContourNaturality

Back to source controls