ReleaseCanonicalNaturality.lean

1 import KomorebiVerification.PaperII.ReleaseCanonicalHFC
2 
3 set_option autoImplicit false
4 set_option backward.isDefEq.respectTransparency false
5 set_option maxHeartbeats 1000000
6 noncomputable section
7 namespace Komorebi.PaperII.ReleaseCanonicalNaturality
8 open Set Filter
9 open scoped Topology Classical
10 open Komorebi.PaperII.TypedLinearDefects
11 open Komorebi.PaperII.ReleaseAnalyticContour
12 open Komorebi.PaperII.ReleaseCycleWinding
13 open Komorebi.PaperII.ReleaseCycleCauchy
14 open Komorebi.PaperII.ReleaseCanonicalHFC
15 
16 variable {Ef Ec : Type*}
17 variable [NormedAddCommGroup Ef] [NormedAddCommGroup Ec]
18 variable [NormedSpace ℂ Ef] [NormedSpace ℂ Ec]
19 variable [NormedSpace ℝ Ef] [NormedSpace ℝ Ec]
20 variable [IsScalarTower ℝ ℂ Ef] [IsScalarTower ℝ ℂ Ec]
21 variable [CompleteSpace Ef] [CompleteSpace Ec]
22 
23 omit [NormedSpace ℝ Ef] [NormedSpace ℝ Ec]
24   [IsScalarTower ℝ ℂ Ef] [IsScalarTower ℝ ℂ Ec]
25   [CompleteSpace Ef] [CompleteSpace Ec] in
26 theorem resolvent_natural_of_defect_zero
27     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
28     (hdef : continuousDefect C Tf Tc = 0) {z : ℂ}
29     (hf : z ∈ resolventSet ℂ Tf) (hc : z ∈ resolventSet ℂ Tc) :
30     C.comp (resolvent Tf z) = (resolvent Tc z).comp C := by
31   apply sub_eq_zero.mp
32   rw [resolvent_defect_actual C Tf Tc z hf hc,hdef]
33   simp
34 
35 omit [NormedSpace ℝ Ef] [NormedSpace ℝ Ec]
36   [IsScalarTower ℝ ℂ Ef] [IsScalarTower ℝ ℂ Ec]
37   [CompleteSpace Ef] [CompleteSpace Ec] in
38 /-- The intertwining resolvents agree on their overlap, so they define one
39 holomorphic map on the union of the two resolvent sets. -/
40 def gluedResolvent (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
41     (z : ℂ) : Ef →L[ℂ] Ec :=
42   if z ∈ resolventSet ℂ Tf then C.comp (resolvent Tf z) else (resolvent Tc z).comp C
43 
44 omit [NormedSpace ℝ Ef] [NormedSpace ℝ Ec]
45   [IsScalarTower ℝ ℂ Ef] [IsScalarTower ℝ ℂ Ec]
46   [CompleteSpace Ef] [CompleteSpace Ec] in
47 theorem gluedResolvent_eq_left
48     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec) {z : ℂ}
49     (hz : z ∈ resolventSet ℂ Tf) :
50     gluedResolvent C Tf Tc z = C.comp (resolvent Tf z) := by
51   simp [gluedResolvent,hz]
52 
53 omit [NormedSpace ℝ Ef] [NormedSpace ℝ Ec]
54   [IsScalarTower ℝ ℂ Ef] [IsScalarTower ℝ ℂ Ec]
55   [CompleteSpace Ef] [CompleteSpace Ec] in
56 theorem gluedResolvent_eq_right
57     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
58     (hdef : continuousDefect C Tf Tc = 0) {z : ℂ}
59     (hz : z ∈ resolventSet ℂ Tc) :
60     gluedResolvent C Tf Tc z = (resolvent Tc z).comp C := by
61   unfold gluedResolvent
62   split_ifs with hf
63   · exact resolvent_natural_of_defect_zero C Tf Tc hdef hf hz
64   · rfl
65 
66 omit [NormedSpace ℝ Ef] [NormedSpace ℝ Ec]
67   [IsScalarTower ℝ ℂ Ef] [IsScalarTower ℝ ℂ Ec] in
68 theorem differentiableOn_gluedResolvent
69     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
70     (hdef : continuousDefect C Tf Tc = 0) :
71     DifferentiableOn ℂ (gluedResolvent C Tf Tc)
72       (resolventSet ℂ Tf ∪ resolventSet ℂ Tc) := by
73   let post : (Ef →L[ℂ] Ef) →L[ℂ] (Ef →L[ℂ] Ec) :=
74     ContinuousLinearMap.compL ℂ Ef Ef Ec C
75   let pre : (Ec →L[ℂ] Ec) →L[ℂ] (Ef →L[ℂ] Ec) :=
76     (ContinuousLinearMap.compL ℂ Ef Ec Ec).flip C
77   intro z hz
78   rcases hz with hf | hc
79   · have hd := post.hasFDerivAt.comp_hasDerivAt z
80       (spectrum.hasDerivAt_resolvent_const_left hf)
81     apply DifferentiableAt.differentiableWithinAt
82     apply hd.differentiableAt.congr_of_eventuallyEq
83     filter_upwards [(spectrum.isOpen_resolventSet Tf).mem_nhds hf] with w hw
84     exact gluedResolvent_eq_left C Tf Tc hw
85   · have hd := pre.hasFDerivAt.comp_hasDerivAt z
86       (spectrum.hasDerivAt_resolvent_const_left hc)
87     apply DifferentiableAt.differentiableWithinAt
88     apply hd.differentiableAt.congr_of_eventuallyEq
89     filter_upwards [(spectrum.isOpen_resolventSet Tc).mem_nhds hc] with w hw
90     exact gluedResolvent_eq_right C Tf Tc hdef hw
91 
92 /-- Canonical intertwining uses independently admissible cycles and domains.
93 No contour common to the two operator spaces is required. -/
94 theorem dunfordIntegral_natural_of_admissible
95     (h : ℂ → ℂ) (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
96     (Af : AdmissibleCycle h Tf) (Ac : AdmissibleCycle h Tc)
97     (hdef : continuousDefect C Tf Tc = 0) :
98     C.comp (dunfordIntegral Af.cycle h Tf) =
99       (dunfordIntegral Ac.cycle h Tc).comp C := by
100   let V : Set ℂ := (Af.domain ∪ Ac.domain) ∩
101     (resolventSet ℂ Tf ∪ resolventSet ℂ Tc)
102   have hV : IsOpen V := (Af.isOpen_domain.union Ac.isOpen_domain).inter
103     ((spectrum.isOpen_resolventSet Tf).union (spectrum.isOpen_resolventSet Tc))
104   have hh : DifferentiableOn ℂ h (Af.domain ∪ Ac.domain) := by
105     intro z hz
106     rcases hz with hf | hc
107     · exact ((Af.holomorphic z hf).differentiableAt
108         (Af.isOpen_domain.mem_nhds hf)).differentiableWithinAt
109     · exact ((Ac.holomorphic z hc).differentiableAt
110         (Ac.isOpen_domain.mem_nhds hc)).differentiableWithinAt
111   have hdensity : DifferentiableOn ℂ (fun z => h z • gluedResolvent C Tf Tc z) V := by
112     intro z hz
113     have hhz := (hh z hz.1).differentiableAt
114       ((Af.isOpen_domain.union Ac.isOpen_domain).mem_nhds hz.1)
115     have hrz := (differentiableOn_gluedResolvent C Tf Tc hdef z hz.2).differentiableAt
116       (((spectrum.isOpen_resolventSet Tf).union
117         (spectrum.isOpen_resolventSet Tc)).mem_nhds hz.2)
118     exact (hhz.smul hrz).differentiableWithinAt
119   have htracef : Af.cycle.trace ⊆ V :=
120     fun z hz => ⟨Or.inl (Af.trace_domain hz),Or.inl (Af.trace_resolvent hz)⟩
121   have htracec : Ac.cycle.trace ⊆ V :=
122     fun z hz => ⟨Or.inr (Ac.trace_domain hz),Or.inr (Ac.trace_resolvent hz)⟩
123   have hwind : ∀ w ∉ V, winding Af.cycle w = winding Ac.cycle w := by
124     intro w hw
125     by_cases hr : w ∈ resolventSet ℂ Tf ∪ resolventSet ℂ Tc
126     · have ho : w ∉ Af.domain ∪ Ac.domain := fun hu => hw ⟨hu,hr⟩
127       rw [Af.winding_complement w (fun ha => ho (Or.inl ha)),
128         Ac.winding_complement w (fun ha => ho (Or.inr ha))]
129     · have hsf : w ∈ spectrum ℂ Tf := by
130         simpa only [spectrum,mem_compl_iff] using (fun hf => hr (Or.inl hf))
131       have hsc : w ∈ spectrum ℂ Tc := by
132         simpa only [spectrum,mem_compl_iff] using (fun hc => hr (Or.inr hc))
133       rw [Af.winding_spectrum w hsf,Ac.winding_spectrum w hsc]
134   have hcompare := lineIntegral_eq_of_winding Af.cycle Ac.cycle hV hdensity htracef htracec hwind
135   let post : (Ef →L[ℂ] Ef) →L[ℂ] (Ef →L[ℂ] Ec) :=
136     ContinuousLinearMap.compL ℂ Ef Ef Ec C
137   let pre : (Ec →L[ℂ] Ec) →L[ℂ] (Ef →L[ℂ] Ec) :=
138     (ContinuousLinearMap.compL ℂ Ef Ec Ec).flip C
139   have hff : ContinuousOn (fun z => h z • resolvent Tf z) Af.cycle.trace :=
140     (Af.holomorphic.continuousOn.mono Af.trace_domain).smul
141       (continuousOn_resolvent_trace Af.cycle Tf Af.trace_resolvent)
142   have hcc : ContinuousOn (fun z => h z • resolvent Tc z) Ac.cycle.trace :=
143     (Ac.holomorphic.continuousOn.mono Ac.trace_domain).smul
144       (continuousOn_resolvent_trace Ac.cycle Tc Ac.trace_resolvent)
145   have hleft : Af.cycle.lineIntegral (fun z => h z • gluedResolvent C Tf Tc z) =
146       post (Af.cycle.lineIntegral (fun z => h z • resolvent Tf z)) := by
147     rw [← Af.cycle.lineIntegral_map post hff]
148     apply lineIntegral_congr_on_trace Af.cycle
149     intro z hz
150     change h z • gluedResolvent C Tf Tc z = post (h z • resolvent Tf z)
151     rw [gluedResolvent_eq_left C Tf Tc (Af.trace_resolvent hz)]
152     simp only [map_smul]
153     rfl
154   have hright : Ac.cycle.lineIntegral (fun z => h z • gluedResolvent C Tf Tc z) =
155       pre (Ac.cycle.lineIntegral (fun z => h z • resolvent Tc z)) := by
156     rw [← Ac.cycle.lineIntegral_map pre hcc]
157     apply lineIntegral_congr_on_trace Ac.cycle
158     intro z hz
159     change h z • gluedResolvent C Tf Tc z = pre (h z • resolvent Tc z)
160     rw [gluedResolvent_eq_right C Tf Tc hdef (Ac.trace_resolvent hz)]
161     simp only [map_smul]
162     rfl
163   rw [hleft,hright] at hcompare
164   change post ((2 * (Real.pi : ℂ) * Complex.I)⁻¹ •
165       Af.cycle.lineIntegral (fun z => h z • resolvent Tf z)) =
166     pre ((2 * (Real.pi : ℂ) * Complex.I)⁻¹ •
167       Ac.cycle.lineIntegral (fun z => h z • resolvent Tc z))
168   rw [map_smul,map_smul,hcompare]
169 
170 /-- Naturality of the canonical holomorphic functional calculus for zero
171 defect, with separate admissibility witnesses for the two operators. -/
172 theorem canonicalValue_natural_of_defect_zero
173     (h : ℂ → ℂ) (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
174     (Hf : Nonempty (AdmissibleCycle h Tf)) (Hc : Nonempty (AdmissibleCycle h Tc))
175     (hdef : continuousDefect C Tf Tc = 0) :
176     C.comp (canonicalValue h Tf Hf) = (canonicalValue h Tc Hc).comp C := by
177   exact dunfordIntegral_natural_of_admissible h C Tf Tc
178     (Classical.choice Hf) (Classical.choice Hc) hdef
179 
180 theorem canonicalValue_compatible_of_defect_eq_zero
181     (h : ℂ → ℂ) (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
182     (Hf : Nonempty (AdmissibleCycle h Tf)) (Hc : Nonempty (AdmissibleCycle h Tc))
183     (hdef : continuousDefect C Tf Tc = 0) :
184     C.comp (canonicalValue h Tf Hf) = (canonicalValue h Tc Hc).comp C :=
185   canonicalValue_natural_of_defect_zero h C Tf Tc Hf Hc hdef
186 
187 end Komorebi.PaperII.ReleaseCanonicalNaturality

Back to source controls