ReleaseAnalyticContour.lean

1 import KomorebiVerification.PaperII.TypedLinearDefects
2 import Mathlib.Analysis.Normed.Algebra.GelfandFormula
3 import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
4 import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
5 import Mathlib.Tactic.GCongr
6 
7 set_option autoImplicit false
8 noncomputable section
9 namespace Komorebi.PaperII.ReleaseAnalyticContour
10 open scoped BigOperators Topology
11 open MeasureTheory Set
12 open TypedLinearDefects
13 universe u v
14 
15 /-- A finite family of oriented closed absolutely continuous curves, represented
16 by their actual integrable velocities. Repeated entries count multiplicity.
17 This is an analytic representation, not an assertion that all rectifiable
18 parameterizations already have this form. -/
19 structure IntegralCycle where
20   count : ℕ
21   base : Fin count → ℂ
22   velocity : Fin count → ℝ → ℂ
23   velocity_integrable : ∀ i, IntervalIntegrable (velocity i) volume 0 1
24   closed : ∀ i, (∫ s : ℝ in (0:ℝ)..1, velocity i s) = 0
25 
26 namespace IntegralCycle
27 
28 def curve (Γ : IntegralCycle) (i : Fin Γ.count) (s : ℝ) : ℂ :=
29   Γ.base i + ∫ r : ℝ in 0..s, Γ.velocity i r
30 
31 def trace (Γ : IntegralCycle) : Set ℂ :=
32   {z | ∃ i s, s ∈ uIcc (0:ℝ) 1 ∧ Γ.curve i s = z}
33 
34 /-- Velocity length counts each curve occurrence, hence multiplicity. Its
35 identification with geometric rectifiable length is a separate bridge. -/
36 def length (Γ : IntegralCycle) : ℝ :=
37   ∑ i : Fin Γ.count, ∫ s : ℝ in (0:ℝ)..1, ‖Γ.velocity i s‖
38 
39 @[simp] theorem curve_zero (Γ : IntegralCycle) (i : Fin Γ.count) :
40     Γ.curve i 0 = Γ.base i := by simp [curve]
41 
42 @[simp] theorem curve_one (Γ : IntegralCycle) (i : Fin Γ.count) :
43     Γ.curve i 1 = Γ.base i := by simp [curve, Γ.closed]
44 
45 theorem continuousOn_curve (Γ : IntegralCycle) (i : Fin Γ.count) :
46     ContinuousOn (Γ.curve i) (uIcc (0:ℝ) 1) := by
47   exact continuousOn_const.add
48     (intervalIntegral.continuousOn_primitive_interval' (Γ.velocity_integrable i) left_mem_uIcc)
49 
50 section Integral
51 variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E]
52 variable [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E]
53 
54 /-- Actual Bochner line integral over the represented finite cycle. -/
55 def lineIntegral (Γ : IntegralCycle) (f : ℂ → E) : E :=
56   ∑ i : Fin Γ.count, ∫ s : ℝ in (0:ℝ)..1, Γ.velocity i s • f (Γ.curve i s)
57 
58 omit [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
59 theorem integrable_lineIntegrand (Γ : IntegralCycle) {f : ℂ → E}
60     (hf : ContinuousOn f Γ.trace) (i : Fin Γ.count) :
61     IntervalIntegrable (fun s : ℝ => Γ.velocity i s • f (Γ.curve i s)) volume 0 1 := by
62   apply (Γ.velocity_integrable i).smul_continuousOn
63   exact hf.comp (Γ.continuousOn_curve i) (fun s hs => ⟨i,s,hs,rfl⟩)
64 
65 omit [IsScalarTower ℝ ℂ E] in
66 /-- No scalar surrogate is used: bounded linear maps commute with the actual
67 Banach-valued cycle integral. -/
68 theorem lineIntegral_map {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F]
69     [NormedSpace ℝ F] [IsScalarTower ℝ ℂ F] [CompleteSpace F]
70     (Γ : IntegralCycle) (L : E →L[ℂ] F) {f : ℂ → E} (hf : ContinuousOn f Γ.trace) :
71     Γ.lineIntegral (fun z => L (f z)) = L (Γ.lineIntegral f) := by
72   unfold lineIntegral
73   rw [map_sum]
74   apply Finset.sum_congr rfl
75   intro i hi
76   simpa only [map_smul] using
77     L.intervalIntegral_comp_comm (Γ.integrable_lineIntegrand hf i)
78 
79 omit [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
80 theorem lineIntegral_sub (Γ : IntegralCycle) {f g : ℂ → E}
81     (hf : ContinuousOn f Γ.trace) (hg : ContinuousOn g Γ.trace) :
82     Γ.lineIntegral (fun z => f z - g z) = Γ.lineIntegral f - Γ.lineIntegral g := by
83   unfold lineIntegral
84   simp_rw [smul_sub]
85   rw [← Finset.sum_sub_distrib]
86   apply Finset.sum_congr rfl
87   intro i hi
88   exact intervalIntegral.integral_sub (Γ.integrable_lineIntegrand hf i)
89     (Γ.integrable_lineIntegrand hg i)
90 
91 omit [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
92 /-- The exact length-times-uniform-bound estimate for the actual integral. -/
93 theorem norm_lineIntegral_le (Γ : IntegralCycle) {f : ℂ → E} (M : ℝ)
94     (hM : ∀ z ∈ Γ.trace, ‖f z‖ ≤ M) :
95     ‖Γ.lineIntegral f‖ ≤ Γ.length * M := by
96   unfold lineIntegral length
97   refine (norm_sum_le _ _).trans ?_
98   rw [Finset.sum_mul]
99   apply Finset.sum_le_sum
100   intro i hi
101   calc
102     _ ≤ ∫ s : ℝ in (0:ℝ)..1, ‖Γ.velocity i s‖ * M := by
103       apply intervalIntegral.norm_integral_le_of_norm_le (by norm_num)
104       · exact Filter.Eventually.of_forall fun s hs => by
105           rw [norm_smul]
106           exact mul_le_mul_of_nonneg_left
107             (hM (Γ.curve i s) ⟨i,s,by simpa using Ioc_subset_Icc_self hs,rfl⟩)
108             (norm_nonneg _)
109       · exact (Γ.velocity_integrable i).norm.mul_const M
110     _ = _ := intervalIntegral.integral_mul_const _ _
111 end Integral
112 end IntegralCycle
113 
114 section Resolvent
115 variable {Ef : Type u} {Ec : Type v}
116 variable [NormedAddCommGroup Ef] [NormedAddCommGroup Ec]
117 variable [NormedSpace ℂ Ef] [NormedSpace ℂ Ec]
118 variable [NormedSpace ℝ Ef] [NormedSpace ℝ Ec]
119 variable [IsScalarTower ℝ ℂ Ef] [IsScalarTower ℝ ℂ Ec]
120 variable [CompleteSpace Ef] [CompleteSpace Ec]
121 
122 /-- A chosen-cycle Dunford integral. This definition does not itself assert
123 independence of the admissible cycle. -/
124 def dunfordIntegral (Γ : IntegralCycle) (h : ℂ → ℂ)
125     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
126     [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E]
127     (T : E →L[ℂ] E) : E →L[ℂ] E :=
128   (2 * (Real.pi : ℂ) * Complex.I)⁻¹ •
129     Γ.lineIntegral (fun z => h z • resolvent T z)
130 
131 /-- Actual spectrum resolvents satisfy the typed inverse-witness equations. -/
132 theorem resolvent_inverse_witnesses
133     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
134     (T : E →L[ℂ] E) (z : ℂ) (hz : z ∈ resolventSet ℂ T) :
135     (continuousScalarShift z T).comp (resolvent T z) = 1 ∧
136       (resolvent T z).comp (continuousScalarShift z T) = 1 := by
137   rw [spectrum.resolvent_eq hz]
138   have hs : continuousScalarShift z T = (hz.unit : E →L[ℂ] E) := by
139     simp [continuousScalarShift, Algebra.algebraMap_eq_smul_one]
140   rw [hs]
141   constructor
142   · exact hz.unit.mul_inv
143   · exact hz.unit.inv_mul
144 
145 omit [NormedSpace ℝ Ef] [NormedSpace ℝ Ec]
146   [IsScalarTower ℝ ℂ Ef] [IsScalarTower ℝ ℂ Ec]
147   [CompleteSpace Ef] [CompleteSpace Ec] in
148 /-- The pointwise sandwich uses actual spectrum resolvents. -/
149 theorem resolvent_defect_actual
150     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
151     (z : ℂ) (hf : z ∈ resolventSet ℂ Tf) (hc : z ∈ resolventSet ℂ Tc) :
152     C.comp (resolvent Tf z) - (resolvent Tc z).comp C =
153       (resolvent Tc z).comp
154         ((continuousDefect C Tf Tc).comp (resolvent Tf z)) := by
155   simpa only [ContinuousLinearMap.comp_assoc] using
156     continuous_scalarShift_resolvent_identity z C Tf (resolvent Tf z)
157       Tc (resolvent Tc z)
158       (resolvent_inverse_witnesses Tf z hf).1
159       (resolvent_inverse_witnesses Tc z hc).2
160 
161 /-- Actual resolvent continuity on the trace follows from differentiability
162 on its resolvent set. -/
163 theorem continuousOn_resolvent_trace
164     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
165     (Γ : IntegralCycle) (T : E →L[ℂ] E)
166     (hT : Γ.trace ⊆ resolventSet ℂ T) :
167     ContinuousOn (resolvent T) Γ.trace := by
168   intro z hz
169   exact (spectrum.hasDerivAt_resolvent_const_left (hT hz)).continuousAt.continuousWithinAt
170 
171 /-- Integral defect for an actual finite absolutely continuous cycle. No
172 conclusion-valued functional-calculus certificate is a premise. -/
173 theorem dunfordIntegral_defect
174     (Γ : IntegralCycle) (h : ℂ → ℂ) (hh : ContinuousOn h Γ.trace)
175     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
176     (hf : Γ.trace ⊆ resolventSet ℂ Tf) (hc : Γ.trace ⊆ resolventSet ℂ Tc) :
177     C.comp (dunfordIntegral Γ h Tf) - (dunfordIntegral Γ h Tc).comp C =
178       (2 * (Real.pi : ℂ) * Complex.I)⁻¹ •
179         Γ.lineIntegral (fun z => h z •
180           ((resolvent Tc z).comp
181             ((continuousDefect C Tf Tc).comp (resolvent Tf z)))) := by
182   let post : (Ef →L[ℂ] Ef) →L[ℂ] (Ef →L[ℂ] Ec) :=
183     ContinuousLinearMap.compL ℂ Ef Ef Ec C
184   let pre : (Ec →L[ℂ] Ec) →L[ℂ] (Ef →L[ℂ] Ec) :=
185     (ContinuousLinearMap.compL ℂ Ef Ec Ec).flip C
186   have hff := hh.smul (continuousOn_resolvent_trace Γ Tf hf)
187   have hcc := hh.smul (continuousOn_resolvent_trace Γ Tc hc)
188   have hp := Γ.lineIntegral_map post hff
189   have hq := Γ.lineIntegral_map pre hcc
190   have hdiff := Γ.lineIntegral_sub (post.continuous.comp_continuousOn hff)
191     (pre.continuous.comp_continuousOn hcc)
192   have hpoint : Γ.lineIntegral (fun z => post (h z • resolvent Tf z) -
193       pre (h z • resolvent Tc z)) =
194       Γ.lineIntegral (fun z => h z • ((resolvent Tc z).comp
195         ((continuousDefect C Tf Tc).comp (resolvent Tf z)))) := by
196     unfold IntegralCycle.lineIntegral
197     apply Finset.sum_congr rfl
198     intro i hi
199     apply intervalIntegral.integral_congr
200     intro s hs
201     have hz : Γ.curve i s ∈ Γ.trace := ⟨i,s,hs,rfl⟩
202     apply congrArg (fun A : Ef →L[ℂ] Ec => Γ.velocity i s • A)
203     dsimp only
204     rw [map_smul, map_smul]
205     change h (Γ.curve i s) • (C.comp (resolvent Tf (Γ.curve i s))) -
206       h (Γ.curve i s) • ((resolvent Tc (Γ.curve i s)).comp C) = _
207     rw [← smul_sub, resolvent_defect_actual C Tf Tc _ (hf hz) (hc hz)]
208   change Γ.lineIntegral (fun z => post (h z • resolvent Tf z)) =
209     post (Γ.lineIntegral (fun z => h z • resolvent Tf z)) at hp
210   change Γ.lineIntegral (fun z => pre (h z • resolvent Tc z)) =
211     pre (Γ.lineIntegral (fun z => h z • resolvent Tc z)) at hq
212   change Γ.lineIntegral (fun z => post (h z • resolvent Tf z) -
213     pre (h z • resolvent Tc z)) =
214     Γ.lineIntegral (fun z => post (h z • resolvent Tf z)) -
215     Γ.lineIntegral (fun z => pre (h z • resolvent Tc z)) at hdiff
216   rw [← hpoint, hdiff, hp, hq]
217   ext x
218   simp [dunfordIntegral, post, pre, smul_sub]
219 /-- The Cauchy normalization has exactly the norm 1/(2*pi). -/
220 theorem norm_cauchy_prefactor :
221     ‖(2 * (Real.pi : ℂ) * Complex.I)⁻¹‖ = (2 * Real.pi)⁻¹ := by
222   simp [norm_inv, Complex.norm_real, abs_of_pos Real.pi_pos]
223 
224 /-- The chosen-cycle defect norm bound with separate uniform bounds for h
225 and the two actual resolvents. -/
226 theorem dunfordIntegral_norm_defect_le
227     (Γ : IntegralCycle) (h : ℂ → ℂ) (hh : ContinuousOn h Γ.trace)
228     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
229     (hf : Γ.trace ⊆ resolventSet ℂ Tf) (hc : Γ.trace ⊆ resolventSet ℂ Tc)
230     (Mh Mc Mf : ℝ) (hMh : 0 ≤ Mh) (hMc : 0 ≤ Mc) (_hMf : 0 ≤ Mf)
231     (hhb : ∀ z ∈ Γ.trace, ‖h z‖ ≤ Mh)
232     (hcb : ∀ z ∈ Γ.trace, ‖resolvent Tc z‖ ≤ Mc)
233     (hfb : ∀ z ∈ Γ.trace, ‖resolvent Tf z‖ ≤ Mf) :
234     ‖C.comp (dunfordIntegral Γ h Tf) - (dunfordIntegral Γ h Tc).comp C‖ ≤
235       Γ.length / (2 * Real.pi) * Mh * ‖continuousDefect C Tf Tc‖ * Mc * Mf := by
236   rw [dunfordIntegral_defect Γ h hh C Tf Tc hf hc, norm_smul]
237   calc
238     _ ≤ ‖(2 * (Real.pi : ℂ) * Complex.I)⁻¹‖ *
239         (Γ.length * (Mh * (Mc * (‖continuousDefect C Tf Tc‖ * Mf)))) := by
240       apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
241       apply Γ.norm_lineIntegral_le
242       intro z hz
243       rw [norm_smul]
244       calc
245         _ ≤ ‖h z‖ * (‖resolvent Tc z‖ *
246             ‖(continuousDefect C Tf Tc).comp (resolvent Tf z)‖) :=
247           mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le _ _) (norm_nonneg _)
248         _ ≤ ‖h z‖ * (‖resolvent Tc z‖ *
249             (‖continuousDefect C Tf Tc‖ * ‖resolvent Tf z‖)) := by
250           gcongr
251           exact ContinuousLinearMap.opNorm_comp_le _ _
252         _ ≤ Mh * (Mc * (‖continuousDefect C Tf Tc‖ * Mf)) := by
253           gcongr
254           · exact hhb z hz
255           · exact hcb z hz
256           · exact hfb z hz
257     _ = _ := by
258       rw [norm_cauchy_prefactor, div_eq_mul_inv]
259       ring
260 
261 /-- The zero-defect chosen-cycle consequence is obtained from the integral
262 identity, not assumed as a calculus naturality axiom. -/
263 theorem dunfordIntegral_compatible_of_defect_eq_zero
264     (Γ : IntegralCycle) (h : ℂ → ℂ) (hh : ContinuousOn h Γ.trace)
265     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
266     (hf : Γ.trace ⊆ resolventSet ℂ Tf) (hc : Γ.trace ⊆ resolventSet ℂ Tc)
267     (hdef : continuousDefect C Tf Tc = 0) :
268     C.comp (dunfordIntegral Γ h Tf) = (dunfordIntegral Γ h Tc).comp C := by
269   apply sub_eq_zero.mp
270   rw [dunfordIntegral_defect Γ h hh C Tf Tc hf hc]
271   simp [hdef, IntegralCycle.lineIntegral]
272 end Resolvent
273 end Komorebi.PaperII.ReleaseAnalyticContour

Back to source controls