ReleaseCanonicalHFC.lean

1 import KomorebiVerification.PaperII.ReleaseCycleCauchy
2 import Mathlib.Analysis.Normed.Algebra.Spectrum
3 
4 set_option autoImplicit false
5 noncomputable section
6 namespace Komorebi.PaperII.ReleaseCanonicalHFC
7 open Set
8 open scoped Topology
9 open Komorebi.PaperII.ReleaseAnalyticContour
10 open Komorebi.PaperII.ReleaseCycleWinding
11 open Komorebi.PaperII.ReleaseCycleCauchy
12 
13 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
14 variable [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E]
15 
16 /-- The paper's admissibility data consist only of holomorphy, genuine
17 cycle traces, actual resolvents and actual winding integrals. No calculus
18 value, contour-independence equation or Cauchy conclusion is a field. -/
19 structure AdmissibleCycle (h : ℂ → ℂ) (T : E →L[ℂ] E) where
20   domain : Set ℂ
21   isOpen_domain : IsOpen domain
22   holomorphic : DifferentiableOn ℂ h domain
23   spectrum_subset : spectrum ℂ T ⊆ domain
24   cycle : IntegralCycle
25   trace_domain : cycle.trace ⊆ domain
26   trace_resolvent : cycle.trace ⊆ resolventSet ℂ T
27   winding_spectrum : ∀ z ∈ spectrum ℂ T, winding cycle z = 1
28   winding_complement : ∀ z ∉ domain, winding cycle z = 0
29 
30 /-- Actual normalized Dunford integrals are independent of every admissible
31 cycle and its open holomorphy domain, including on the zero operator space. -/
32 theorem dunfordIntegral_eq_of_admissible (h : ℂ → ℂ) (T : E →L[ℂ] E)
33     (A B : AdmissibleCycle h T) :
34     dunfordIntegral A.cycle h T = dunfordIntegral B.cycle h T := by
35   let V : Set ℂ := (A.domain ∪ B.domain) ∩ resolventSet ℂ T
36   have hV : IsOpen V :=
37     (A.isOpen_domain.union B.isOpen_domain).inter (spectrum.isOpen_resolventSet T)
38   have hhol : DifferentiableOn ℂ h (A.domain ∪ B.domain) := by
39     intro z hz
40     rcases hz with ha | hb
41     · exact ((A.holomorphic z ha).differentiableAt
42         (A.isOpen_domain.mem_nhds ha)).differentiableWithinAt
43     · exact ((B.holomorphic z hb).differentiableAt
44         (B.isOpen_domain.mem_nhds hb)).differentiableWithinAt
45   have hdensity : DifferentiableOn ℂ (fun z ↦ h z • resolvent T z) V := by
46     intro z hz
47     have hh := (hhol z hz.1).differentiableAt
48       ((A.isOpen_domain.union B.isOpen_domain).mem_nhds hz.1)
49     exact (hh.smul (spectrum.hasDerivAt_resolvent_const_left hz.2).differentiableAt).differentiableWithinAt
50   have htraceA : A.cycle.trace ⊆ V := fun z hz ↦
51     ⟨Or.inl (A.trace_domain hz),A.trace_resolvent hz⟩
52   have htraceB : B.cycle.trace ⊆ V := fun z hz ↦
53     ⟨Or.inr (B.trace_domain hz),B.trace_resolvent hz⟩
54   have hwind : ∀ w ∉ V, winding A.cycle w = winding B.cycle w := by
55     intro w hw
56     by_cases hr : w ∈ resolventSet ℂ T
57     · have ho : w ∉ A.domain ∪ B.domain := fun hu ↦ hw ⟨hu,hr⟩
58       rw [A.winding_complement w (fun ha ↦ ho (Or.inl ha)),
59         B.winding_complement w (fun hb ↦ ho (Or.inr hb))]
60     · have hs : w ∈ spectrum ℂ T := by simpa only [spectrum, mem_compl_iff] using hr
61       rw [A.winding_spectrum w hs,B.winding_spectrum w hs]
62   unfold dunfordIntegral
63   exact congrArg (fun q : E →L[ℂ] E ↦ (2 * (Real.pi : ℂ) * Complex.I)⁻¹ • q)
64     (lineIntegral_eq_of_winding A.cycle B.cycle hV hdensity htraceA htraceB hwind)
65 
66 /-- The canonical value is chosen only when admissible data exist. The
67 theorem below proves that the choice has no effect on the resulting value. -/
68 def canonicalValue (h : ℂ → ℂ) (T : E →L[ℂ] E)
69     (H : Nonempty (AdmissibleCycle h T)) : E →L[ℂ] E :=
70   dunfordIntegral (Classical.choice H).cycle h T
71 
72 theorem canonicalValue_eq_dunfordIntegral (h : ℂ → ℂ) (T : E →L[ℂ] E)
73     (H : Nonempty (AdmissibleCycle h T)) (A : AdmissibleCycle h T) :
74     canonicalValue h T H = dunfordIntegral A.cycle h T :=
75   dunfordIntegral_eq_of_admissible h T (Classical.choice H) A
76 
77 theorem canonicalValue_eq_of_witness (h : ℂ → ℂ) (T : E →L[ℂ] E)
78     (H K : Nonempty (AdmissibleCycle h T)) : canonicalValue h T H = canonicalValue h T K := by
79   exact dunfordIntegral_eq_of_admissible h T (Classical.choice H) (Classical.choice K)
80 
81 end Komorebi.PaperII.ReleaseCanonicalHFC

Back to source controls