HolomorphicFinite.lean

1 import KomorebiPaperVI.CanonicalJets
2 import Mathlib.Analysis.Complex.CauchyIntegral
3 import Mathlib.LinearAlgebra.Matrix.ToLin
4 
5 /-! Author: Komorebi P. Canonical holomorphic functions of finite complex matrices.
6 The definition uses the unique finite Taylor-jet action on generalized eigenspaces.
7 Cauchy's formula identifies each local coefficient with an actual circle integral. -/
8 namespace KomorebiPaperVI.HolomorphicFinite
9 open Module Complex Set
10 open scoped Topology
11 open KomorebiPaperVI.CanonicalJets
12 set_option backward.isDefEq.respectTransparency false
13 
14 section Linear
15 variable {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
16 
17 theorem canonical_unique (A : End ℂ V) (a : ℂ → ℕ → ℂ) (B : End ℂ V)
18     (hB : ∀ μ x,x∈A.maxGenEigenspace μ → B x=jet A a μ (finrank ℂ V) x) :
19     B=calculus A a := by
20   apply DirectSum.decompose_lhom_ext A.maxGenEigenspace
21   intro μ
22   ext x
23   exact (hB μ x x.property).trans (calculus_on_component A a μ x x.property).symm
24 
25 theorem holomorphic_on_component (A : End ℂ V) (f : ℂ → ℂ) (μ : ℂ)
26     (x : V) (hx : x∈A.maxGenEigenspace μ) :
27     holomorphic A f x=∑ k ∈ Finset.range (finrank ℂ V),
28       (iteratedDeriv k f μ/(k.factorial:ℂ)) • (((A-μ • 1)^k) x) := by
29   rw [holomorphic,calculus_on_component A _ μ x hx]
30   simp [jet]
31 
32 omit [FiniteDimensional ℂ V] in
33 theorem component_mem_spectrum (A : End ℂ V) (μ : ℂ) (x : V)
34     (hx : x∈A.maxGenEigenspace μ) (hne : x≠0) : μ∈spectrum ℂ A := by
35   have hv : A.HasUnifEigenvector μ ⊤ x := ⟨hx,hne⟩
36   exact (hv.hasUnifEigenvalue.lt zero_lt_one).mem_spectrum
37 
38 theorem calculus_spectrum_congr (A : End ℂ V) (a b : ℂ → ℕ → ℂ)
39     (h : ∀ μ∈spectrum ℂ A,∀ k∈Finset.range (finrank ℂ V),a μ k=b μ k) :
40     calculus A a=calculus A b := by
41   apply DirectSum.decompose_lhom_ext A.maxGenEigenspace
42   intro μ
43   ext x
44   change calculus A a x=calculus A b x
45   by_cases hx : (x:V)=0
46   · simp [hx]
47   rw [calculus_on_component A a μ x x.property,calculus_on_component A b μ x x.property]
48   simp only [jet,LinearMap.sum_apply,LinearMap.smul_apply]
49   apply Finset.sum_congr rfl
50   intro k hk
51   rw [h μ (component_mem_spectrum A μ x x.property hx) k hk]
52 
53 end Linear
54 
55 noncomputable def cauchyCoefficient (f : ℂ → ℂ) (μ : ℂ) (r : ℝ) (k : ℕ) : ℂ :=
56   (2*Real.pi*I)⁻¹ * ∮ z in C(μ,r),f z/(z-μ)^(k+1)
57 
58 theorem cauchyCoefficient_eq (f : ℂ → ℂ) (μ : ℂ) (r : ℝ) (hr : 0 < r)
59     (hf : DifferentiableOn ℂ f (Metric.closedBall μ r)) (k : ℕ) :
60     cauchyCoefficient f μ r k=iteratedDeriv k f μ/(k.factorial:ℂ) := by
61   have hh := hf.circleIntegral_one_div_sub_center_pow_smul hr k
62   simp only [smul_eq_mul,one_div] at hh
63   unfold cauchyCoefficient
64   have he : (fun z => f z/(z-μ)^(k+1))=(fun z => ((z-μ)^(k+1))⁻¹*f z) := by
65     ext z
66     simp [div_eq_mul_inv,mul_comm]
67   rw [he,hh]
68   field_simp
69 
70 theorem cauchyCoefficient_independent (f : ℂ → ℂ) (μ : ℂ) (r s : ℝ)
71     (hr : 0 < r) (hs : 0 < s)
72     (hf : DifferentiableOn ℂ f (Metric.closedBall μ r))
73     (hg : DifferentiableOn ℂ f (Metric.closedBall μ s)) (k : ℕ) :
74     cauchyCoefficient f μ r k=cauchyCoefficient f μ s k := by
75   rw [cauchyCoefficient_eq f μ r hr hf,cauchyCoefficient_eq f μ s hs hg]
76 
77 theorem admissible_circle (f : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U)
78     (hf : AnalyticOnNhd ℂ f U) (μ : ℂ) (hμ : μ∈U) :
79     ∃ r : ℝ,0 < r ∧ Metric.closedBall μ r ⊆ U ∧
80       ∀ k,cauchyCoefficient f μ r k=iteratedDeriv k f μ/(k.factorial:ℂ) := by
81   obtain ⟨r,hr,hsub⟩ := Metric.nhds_basis_closedBall.mem_iff.mp (hU.mem_nhds hμ)
82   exact ⟨r,hr,hsub,fun k => cauchyCoefficient_eq f μ r hr
83     (fun z hz => (hf z (hsub hz)).differentiableAt.differentiableWithinAt) k⟩
84 
85 section LocalRepresentation
86 variable {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
87 
88 theorem canonical_cauchy_representation (A : End ℂ V) (f : ℂ → ℂ) (r : ℂ → ℝ)
89     (hr : ∀ μ∈spectrum ℂ A,0 < r μ)
90     (hf : ∀ μ∈spectrum ℂ A,DifferentiableOn ℂ f (Metric.closedBall μ (r μ))) :
91     calculus A (fun μ k => cauchyCoefficient f μ (r μ) k)=holomorphic A f := by
92   apply calculus_spectrum_congr
93   intro μ hμ k _
94   exact cauchyCoefficient_eq f μ (r μ) (hr μ hμ) (hf μ hμ) k
95 
96 theorem canonical_contours_exist (A : End ℂ V) (f : ℂ → ℂ) (U : Set ℂ)
97     (hU : IsOpen U) (hf : AnalyticOnNhd ℂ f U) (hA : spectrum ℂ A ⊆ U) :
98     ∃ r : ℂ → ℝ,(∀ μ∈spectrum ℂ A,0 < r μ ∧ Metric.closedBall μ (r μ) ⊆ U) ∧
99       calculus A (fun μ k => cauchyCoefficient f μ (r μ) k)=holomorphic A f := by
100   classical
101   have he (μ : ℂ) : ∃ r : ℝ,0 < r ∧
102       (μ∈spectrum ℂ A → Metric.closedBall μ r ⊆ U) := by
103     by_cases hm : μ∈spectrum ℂ A
104     · obtain ⟨r,hr,hsub,_⟩ := admissible_circle f U hU hf μ (hA hm)
105       exact ⟨r,hr,fun _ => hsub⟩
106     · exact ⟨1,zero_lt_one,fun h => (hm h).elim⟩
107   choose r hr hsub using he
108   refine ⟨r,fun μ hμ => ⟨hr μ,hsub μ hμ⟩,?_⟩
109   apply canonical_cauchy_representation A f r (fun μ _ => hr μ)
110   intro μ hμ z hz
111   exact (hf z (hsub μ hμ hz)).differentiableAt.differentiableWithinAt
112 
113 theorem canonical_contours_independent (A : End ℂ V) (f : ℂ → ℂ) (r s : ℂ → ℝ)
114     (hr : ∀ μ∈spectrum ℂ A,0 < r μ) (hs : ∀ μ∈spectrum ℂ A,0 < s μ)
115     (hf : ∀ μ∈spectrum ℂ A,DifferentiableOn ℂ f (Metric.closedBall μ (r μ)))
116     (hg : ∀ μ∈spectrum ℂ A,DifferentiableOn ℂ f (Metric.closedBall μ (s μ))) :
117     calculus A (fun μ k => cauchyCoefficient f μ (r μ) k)=
118       calculus A (fun μ k => cauchyCoefficient f μ (s μ) k) := by
119   rw [canonical_cauchy_representation A f r hr hf,canonical_cauchy_representation A f s hs hg]
120 
121 end LocalRepresentation
122 
123 section Matrix
124 variable {I J : Type*} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
125 
126 noncomputable def matrixFunction (A : Matrix I I ℂ) (f : ℂ → ℂ) : Matrix I I ℂ :=
127   LinearMap.toMatrix' (holomorphic A.toLin' f)
128 
129 theorem matrix_holomorphic_naturality (A : Matrix I I ℂ) (B : Matrix J J ℂ)
130     (C : Matrix J I ℂ) (h : C*A=B*C) (f : ℂ → ℂ) :
131     C*matrixFunction A f=matrixFunction B f*C := by
132   have hh : B.toLin'.comp C.toLin'=C.toLin'.comp A.toLin' := by
133     rw [← Matrix.toLin'_mul,← Matrix.toLin'_mul,h]
134   have hc := holomorphic_naturality A.toLin' B.toLin' C.toLin' hh f
135   have hm := congrArg LinearMap.toMatrix' hc
136   simpa only [LinearMap.toMatrix'_comp,LinearMap.toMatrix'_toLin',matrixFunction] using hm
137 
138 end Matrix
139 end KomorebiPaperVI.HolomorphicFinite

Back to source controls