HolomorphicContours.lean

1 import KomorebiPaperVI.ContourNaturality
2 import Mathlib.Topology.Instances.Matrix
3 import Mathlib.Analysis.Analytic.Basic
4 
5 /-! Author: Komorebi P. Holomorphic input supplies integrability on common resolvent circles.
6 The canonical finite-dimensional construction and its local Cauchy-circle independence
7 are supplied by HolomorphicFinite. -/
8 namespace KomorebiPaperVI.HolomorphicContours
9 open Set Complex
10 open KomorebiPaperVI.ContourNaturality
11 set_option backward.isDefEq.respectTransparency false
12 variable {I J K : Type*} [Fintype I] [Fintype J] [Fintype K] [DecidableEq I] [DecidableEq J]
13 
14 omit [Fintype J] [Fintype K] [DecidableEq J] in
15 theorem resolvent_continuousAt (A : Matrix I I ℂ) (z : ℂ) (hz : IsUnit (Matrix.scalar I z-A)) :
16     ContinuousAt (ContourNaturality.resolvent A) z := by
17   have hd : (Matrix.scalar I z-A).det ≠ 0 :=
18     (Matrix.isUnit_iff_isUnit_det _).mp hz |>.ne_zero
19   have hi : ContinuousAt Ring.inverse (Matrix.scalar I z-A).det := by
20     rw [Ring.inverse_eq_inv']
21     exact continuousAt_inv₀ hd
22   have hc : Continuous (fun w : ℂ => Matrix.scalar I w-A) := by
23     apply continuous_matrix
24     intro i j
25     simp only [Matrix.sub_apply,Matrix.scalar_apply,Matrix.diagonal_apply]
26     split_ifs <;> fun_prop
27   change ContinuousAt (fun w : ℂ => (Matrix.scalar I w-A)⁻¹) z
28   exact (continuousAt_matrix_inv _ hi).comp (x := z) hc.continuousAt
29 
30 omit [Fintype J] [Fintype K] [DecidableEq J] in
31 theorem holomorphic_circle_integrable (A : Matrix I I ℂ) (f : ℂ → ℂ) (U : Set ℂ)
32     (hf : AnalyticOnNhd ℂ f U) (c : ℂ) (r : ℝ) (hr : 0 ≤ r)
33     (hc : Metric.sphere c r ⊆ U)
34     (hA : ∀ z∈Metric.sphere c r,IsUnit (Matrix.scalar I z-A)) (i j : I) :
35     CircleIntegrable (fun z => f z*ContourNaturality.resolvent A z i j) c r := by
36   apply ContinuousOn.circleIntegrable hr
37   apply (hf.continuousOn.mono hc).mul
38   intro z hz
39   have ht := resolvent_continuousAt A z (hA z hz)
40   exact ((continuous_apply j).continuousAt.comp ((continuous_apply i).continuousAt.comp ht)).continuousWithinAt
41 
42 theorem holomorphic_common_contour_naturality (C : Matrix J I ℂ) (A : Matrix I I ℂ) (B : Matrix J J ℂ)
43     (h : C*A=B*C) (f : ℂ → ℂ) (U : Set ℂ) (hf : AnalyticOnNhd ℂ f U)
44     (c : K → ℂ) (r : K → ℝ) (hr : ∀ k,0 ≤ r k)
45     (hc : ∀ k,Metric.sphere (c k) (r k) ⊆ U)
46     (hA : ∀ k z,z∈Metric.sphere (c k) (r k) → IsUnit (Matrix.scalar I z-A))
47     (hB : ∀ k z,z∈Metric.sphere (c k) (r k) → IsUnit (Matrix.scalar J z-B)) :
48     C*calculus A f c r=calculus B f c r*C :=
49   common_contour_naturality C A B h f c r hr hA hB
50     (fun k i j => holomorphic_circle_integrable A f U hf (c k) (r k) (hr k) (hc k) (hA k) i j)
51     (fun k i j => holomorphic_circle_integrable B f U hf (c k) (r k) (hr k) (hc k) (hB k) i j)
52 
53 end KomorebiPaperVI.HolomorphicContours

Back to source controls