ReleaseCanonicalDefect.lean

1 import KomorebiVerification.PaperII.ReleaseCanonicalHFC
2 import KomorebiVerification.PaperII.ReleaseCanonicalNaturality
3 import KomorebiVerification.PaperII.ReleaseRectifiableDefect
4 import KomorebiVerification.PaperII.ReleaseDefectTower
5 
6 /-! Canonical holomorphic-calculus defect and arbitrary-depth compatibility,
7 with the original finite rectifiable tagged RS contours and geometric length. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace Komorebi.PaperII.ReleaseCanonicalDefect
11 open Set
12 open scoped Topology BigOperators
13 open Komorebi.PaperII.ReleaseAnalyticContour
14 open Komorebi.PaperII.ReleaseRectifiableCycle
15 open Komorebi.PaperII.ReleaseRectifiableDefect
16 open Komorebi.PaperII.ReleaseRectifiableRSError
17 open Komorebi.PaperII.ReleaseArcLength
18 open Komorebi.PaperII.ReleaseCycleWinding
19 open Komorebi.PaperII.ReleaseCanonicalHFC
20 open Komorebi.PaperII.ReleaseDefectTower
21 open TypedLinearDefects
22 universe u v
23 
24 /-- Original rectifiable winding, defined from the genuine tagged RS
25 contour integrals on the original parameterized paths. -/
26 def rectifiableWinding (n : ℕ) (f : Fin n → ℝ → ℂ) (w : ℂ) : ℂ :=
27   (2 * (Real.pi : ℂ) * Complex.I)⁻¹ *
28     ∑ i : Fin n, taggedContourIntegral (f i) (fun z ↦ (z-w)⁻¹) 0 1
29 
30 /-- The original classical winding equals the actual represented cycle's
31 winding, as a theorem of the tagged RS/velocity comparison. -/
32 theorem rectifiableWinding_eq_winding (n : ℕ) (f : Fin n → ℝ → ℂ)
33     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
34     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
35     (hclosed : ∀ i, f i 1 = f i 0) {w : ℂ}
36     (hw : w ∉ (cycleOfRectifiable n f hv hc hclosed).trace) :
37     rectifiableWinding n f w = winding (cycleOfRectifiable n f hv hc hclosed) w := by
38   have hcont : ContinuousOn (fun z : ℂ ↦ (z-w)⁻¹) (cycleOfRectifiable n f hv hc hclosed).trace :=
39     (continuousOn_id.sub continuousOn_const).inv₀
40       (fun z hz ↦ sub_ne_zero.mpr (ne_of_mem_of_not_mem hz hw))
41   unfold rectifiableWinding winding
42   apply congrArg (fun a : ℂ ↦ (2 * (Real.pi : ℂ) * Complex.I)⁻¹ * a)
43   exact sum_taggedContourIntegral_eq_lineIntegral n f hv hc hclosed
44     (fun i ↦ hcont.mono (component_subset_trace n f hv hc hclosed i))
45 
46 /-- The manuscript's actual rectifiable Cauchy hypotheses construct an
47 admissible canonical-calculus cycle. No representation equation is a field. -/
48 def admissibleRectifiable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
49     (n : ℕ) (f : Fin n → ℝ → ℂ)
50     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
51     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
52     (hclosed : ∀ i, f i 1 = f i 0)
53     (h : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U) (hh : DifferentiableOn ℂ h U)
54     (T : E →L[ℂ] E) (hσ : spectrum ℂ T ⊆ U)
55     (htrace : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ U)
56     (hR : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ T)
57     (hwindσ : ∀ z ∈ spectrum ℂ T, winding (cycleOfRectifiable n f hv hc hclosed) z = 1)
58     (hwindU : ∀ z ∉ U, winding (cycleOfRectifiable n f hv hc hclosed) z = 0) :
59     AdmissibleCycle h T where
60   domain := U
61   isOpen_domain := hU
62   holomorphic := hh
63   spectrum_subset := hσ
64   cycle := cycleOfRectifiable n f hv hc hclosed
65   trace_domain := htrace
66   trace_resolvent := hR
67   winding_spectrum := hwindσ
68   winding_complement := hwindU
69 
70 /-- Admission from the original contours' own classical winding numbers.
71 The off-trace hypotheses needed for winding comparison follow from the actual
72 resolvent and open-domain assumptions. -/
73 def admissibleRectifiable_original {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
74     (n : ℕ) (f : Fin n → ℝ → ℂ)
75     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
76     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
77     (hclosed : ∀ i, f i 1 = f i 0)
78     (h : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U) (hh : DifferentiableOn ℂ h U)
79     (T : E →L[ℂ] E) (hσ : spectrum ℂ T ⊆ U)
80     (htrace : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ U)
81     (hR : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ T)
82     (hwindσ : ∀ z ∈ spectrum ℂ T, rectifiableWinding n f z = 1)
83     (hwindU : ∀ z ∉ U, rectifiableWinding n f z = 0) : AdmissibleCycle h T := by
84   refine admissibleRectifiable n f hv hc hclosed h U hU hh T hσ htrace hR ?_ ?_
85   · intro z hz
86     have hzR : z ∉ resolventSet ℂ T := by simpa only [spectrum,mem_compl_iff] using hz
87     rw [← rectifiableWinding_eq_winding n f hv hc hclosed (fun ht ↦ hzR (hR ht))]
88     exact hwindσ z hz
89   · intro z hz
90     rw [← rectifiableWinding_eq_winding n f hv hc hclosed (fun ht ↦ hz (htrace ht))]
91     exact hwindU z hz
92 
93 /-- Canonical calculus is represented by the original tagged rectifiable
94 contour integral under precisely the geometric Cauchy hypotheses. -/
95 theorem canonicalValue_eq_rectifiableDunford
96     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
97     [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E]
98     (n : ℕ) (f : Fin n → ℝ → ℂ)
99     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
100     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
101     (hclosed : ∀ i, f i 1 = f i 0)
102     (h : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U) (hh : DifferentiableOn ℂ h U)
103     (T : E →L[ℂ] E) (hσ : spectrum ℂ T ⊆ U)
104     (htrace : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ U)
105     (hR : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ T)
106     (hwindσ : ∀ z ∈ spectrum ℂ T, winding (cycleOfRectifiable n f hv hc hclosed) z = 1)
107     (hwindU : ∀ z ∉ U, winding (cycleOfRectifiable n f hv hc hclosed) z = 0)
108     (H : Nonempty (AdmissibleCycle h T)) :
109     canonicalValue h T H = rectifiableDunford n f h T := by
110   let A := admissibleRectifiable n f hv hc hclosed h U hU hh T hσ htrace hR hwindσ hwindU
111   exact (canonicalValue_eq_dunfordIntegral h T H A).trans
112     (rectifiableDunford_eq_dunfordIntegral n f hv hc hclosed h
113       (hh.continuousOn.mono htrace) T hR).symm
114 
115 /-- Original-winding form of the canonical RS representation theorem. -/
116 theorem canonicalValue_eq_rectifiableDunford_original
117     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
118     [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E]
119     (n : ℕ) (f : Fin n → ℝ → ℂ)
120     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
121     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
122     (hclosed : ∀ i, f i 1 = f i 0)
123     (h : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U) (hh : DifferentiableOn ℂ h U)
124     (T : E →L[ℂ] E) (hσ : spectrum ℂ T ⊆ U)
125     (htrace : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ U)
126     (hR : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ T)
127     (hwindσ : ∀ z ∈ spectrum ℂ T, rectifiableWinding n f z = 1)
128     (hwindU : ∀ z ∉ U, rectifiableWinding n f z = 0)
129     (H : Nonempty (AdmissibleCycle h T)) :
130     canonicalValue h T H = rectifiableDunford n f h T := by
131   let A := admissibleRectifiable_original n f hv hc hclosed h U hU hh T hσ htrace hR hwindσ hwindU
132   exact (canonicalValue_eq_dunfordIntegral h T H A).trans
133     (rectifiableDunford_eq_dunfordIntegral n f hv hc hclosed h
134       (hh.continuousOn.mono htrace) T hR).symm
135 
136 section TwoSpaces
137 variable {Ef : Type u} {Ec : Type v}
138 variable [NormedAddCommGroup Ef] [NormedAddCommGroup Ec]
139 variable [NormedSpace ℂ Ef] [NormedSpace ℂ Ec]
140 variable [NormedSpace ℝ Ef] [NormedSpace ℝ Ec]
141 variable [IsScalarTower ℝ ℂ Ef] [IsScalarTower ℝ ℂ Ec]
142 variable [CompleteSpace Ef] [CompleteSpace Ec]
143 
144 /-- Theorem 11.6: the canonical holomorphic-calculus defect, with the original
145 classical tagged rectifiable contour integrals on its right-hand side. -/
146 theorem canonical_holomorphic_defect (n : ℕ) (f : Fin n → ℝ → ℂ)
147     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
148     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
149     (hclosed : ∀ i, f i 1 = f i 0)
150     (h : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U) (hh : DifferentiableOn ℂ h U)
151     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
152     (hσf : spectrum ℂ Tf ⊆ U) (hσc : spectrum ℂ Tc ⊆ U)
153     (htrace : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ U)
154     (hRf : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ Tf)
155     (hRc : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ Tc)
156     (hwindσ : ∀ z ∈ spectrum ℂ Tf ∪ spectrum ℂ Tc,
157       rectifiableWinding n f z = 1)
158     (hwindU : ∀ z ∉ U, rectifiableWinding n f z = 0)
159     (Hf : Nonempty (AdmissibleCycle h Tf)) (Hc : Nonempty (AdmissibleCycle h Tc)) :
160     C.comp (canonicalValue h Tf Hf) - (canonicalValue h Tc Hc).comp C =
161       (2 * (Real.pi : ℂ) * Complex.I)⁻¹ •
162         ∑ i : Fin n, taggedContourIntegral (f i) (fun z ↦ h z •
163           ((resolvent Tc z).comp ((continuousDefect C Tf Tc).comp (resolvent Tf z)))) 0 1 := by
164   rw [canonicalValue_eq_rectifiableDunford_original n f hv hc hclosed h U hU hh Tf hσf htrace hRf
165       (fun z hz ↦ hwindσ z (Or.inl hz)) hwindU Hf,
166     canonicalValue_eq_rectifiableDunford_original n f hv hc hclosed h U hU hh Tc hσc htrace hRc
167       (fun z hz ↦ hwindσ z (Or.inr hz)) hwindU Hc]
168   exact rectifiableDunford_defect n f hv hc hclosed h (hh.continuousOn.mono htrace) C Tf Tc hRf hRc
169 
170 /-- Theorem 11.6 norm bound: original geometric length, actual canonical
171 values, and the three separate trace suprema occurring in the manuscript. -/
172 theorem canonical_holomorphic_norm_defect_le (n : ℕ) (f : Fin n → ℝ → ℂ)
173     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
174     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
175     (hclosed : ∀ i, f i 1 = f i 0)
176     (h : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U) (hh : DifferentiableOn ℂ h U)
177     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
178     (hσf : spectrum ℂ Tf ⊆ U) (hσc : spectrum ℂ Tc ⊆ U)
179     (htrace : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ U)
180     (hRf : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ Tf)
181     (hRc : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ Tc)
182     (hwindσ : ∀ z ∈ spectrum ℂ Tf ∪ spectrum ℂ Tc,
183       rectifiableWinding n f z = 1)
184     (hwindU : ∀ z ∉ U, rectifiableWinding n f z = 0)
185     (Hf : Nonempty (AdmissibleCycle h Tf)) (Hc : Nonempty (AdmissibleCycle h Tc)) :
186     ‖C.comp (canonicalValue h Tf Hf) - (canonicalValue h Tc Hc).comp C‖ ≤
187       (∑ i : Fin n, geometricLength (f i)) / (2 * Real.pi) *
188         (cycleOfRectifiable n f hv hc hclosed).supNorm h * ‖continuousDefect C Tf Tc‖ *
189         (cycleOfRectifiable n f hv hc hclosed).supNorm (resolvent Tc) *
190         (cycleOfRectifiable n f hv hc hclosed).supNorm (resolvent Tf) := by
191   rw [canonicalValue_eq_rectifiableDunford_original n f hv hc hclosed h U hU hh Tf hσf htrace hRf
192       (fun z hz ↦ hwindσ z (Or.inl hz)) hwindU Hf,
193     canonicalValue_eq_rectifiableDunford_original n f hv hc hclosed h U hU hh Tc hσc htrace hRc
194       (fun z hz ↦ hwindσ z (Or.inr hz)) hwindU Hc]
195   exact rectifiableDunford_norm_defect_le_geometric_sup n f hv hc hclosed h
196     (hh.continuousOn.mono htrace) C Tf Tc hRf hRc
197 
198 /-- The zero-defect consequence concerns genuine canonical holomorphic
199 values, independently of the witnesses used to define them. -/
200 theorem canonicalValue_compatible_of_defect_eq_zero (h : ℂ → ℂ)
201     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
202     (Hf : Nonempty (AdmissibleCycle h Tf)) (Hc : Nonempty (AdmissibleCycle h Tc))
203     (Af : AdmissibleCycle h Tf) (Ac : AdmissibleCycle h Tc)
204     (hcycle : Ac.cycle = Af.cycle) (hdef : continuousDefect C Tf Tc = 0) :
205     C.comp (canonicalValue h Tf Hf) = (canonicalValue h Tc Hc).comp C := by
206   have hh : ContinuousOn h Af.cycle.trace := Af.holomorphic.continuousOn.mono Af.trace_domain
207   have hRc : Af.cycle.trace ⊆ resolventSet ℂ Tc := by rw [← hcycle]; exact Ac.trace_resolvent
208   rw [canonicalValue_eq_dunfordIntegral h Tf Hf Af, canonicalValue_eq_dunfordIntegral h Tc Hc Ac,
209     hcycle]
210   exact dunfordIntegral_compatible_of_defect_eq_zero Af.cycle h hh C Tf Tc Af.trace_resolvent hRc hdef
211 end TwoSpaces
212 
213 /-- Corollary 11.10, holomorphic branch, at every actual tower depth including
214 zero: vanishing local defects imply canonical holomorphic compatibility. -/
215 theorem multilevel_canonical_holomorphic_compatible
216     {X : ℕ → Type v}
217     [∀ n, NormedAddCommGroup (X n)] [∀ n, NormedSpace ℂ (X n)]
218     [∀ n, NormedSpace ℝ (X n)] [∀ n, IsScalarTower ℝ ℂ (X n)]
219     [∀ n, CompleteSpace (X n)]
220     (C : ∀ n, X (n+1) →L[ℂ] X n) (T : ∀ n, X n →L[ℂ] X n) (L : ℕ)
221     (hd : ∀ k : Fin L, continuousDefect (C k.val) (T (k.val+1)) (T k.val) = 0)
222     (h : ℂ → ℂ)
223     (Hf : Nonempty (AdmissibleCycle h (T L))) (Hc : Nonempty (AdmissibleCycle h (T 0))) :
224     (continuousSegment C (Nat.zero_le L)).comp (canonicalValue h (T L) Hf) =
225       (canonicalValue h (T 0) Hc).comp (continuousSegment C (Nat.zero_le L)) := by
226   apply Komorebi.PaperII.ReleaseCanonicalNaturality.canonicalValue_compatible_of_defect_eq_zero
227     h _ _ _ Hf Hc
228   exact sub_eq_zero.mpr (continuous_multilevel_compatible C T L hd)
229 
230 end Komorebi.PaperII.ReleaseCanonicalDefect

Back to source controls