ReleaseRectifiableDefect.lean

1 import KomorebiVerification.PaperII.ReleaseRectifiableLength
2 import KomorebiVerification.PaperII.ReleaseRectifiableRSError
3 import KomorebiVerification.PaperII.ReleaseAnalyticContourSup
4 
5 /-! Defect identity and original geometric-length bound for classical tagged
6 Riemann–Stieltjes integrals on finite continuous rectifiable cycles.  The remaining
7 canonical holomorphic-calculus identification is a separate theorem. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace Komorebi.PaperII.ReleaseRectifiableDefect
11 open MeasureTheory Set
12 open scoped Topology BigOperators
13 open Komorebi.PaperII.ReleaseAnalyticContour
14 open Komorebi.PaperII.ReleaseRectifiableCycle
15 open Komorebi.PaperII.ReleaseRectifiableLength
16 open Komorebi.PaperII.ReleaseRectifiableRSError
17 open Komorebi.PaperII.ReleaseArcLength
18 open TypedLinearDefects
19 universe u v
20 
21 /-- Chosen-cycle Dunford integral using the original contours' tagged RS
22 integrals, not defined through a velocity integral. -/
23 def rectifiableDunford (n : ℕ) (f : Fin n → ℝ → ℂ) (h : ℂ → ℂ)
24     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
25     (T : E →L[ℂ] E) : E →L[ℂ] E :=
26   (2 * (Real.pi : ℂ) * Complex.I)⁻¹ •
27     ∑ i : Fin n, taggedContourIntegral (f i) (fun z ↦ h z • resolvent T z) 0 1
28 
29 section Operators
30 variable {Ef : Type u} {Ec : Type v}
31 variable [NormedAddCommGroup Ef] [NormedAddCommGroup Ec]
32 variable [NormedSpace ℂ Ef] [NormedSpace ℂ Ec]
33 variable [NormedSpace ℝ Ef] [NormedSpace ℝ Ec]
34 variable [IsScalarTower ℝ ℂ Ef] [IsScalarTower ℝ ℂ Ec]
35 variable [CompleteSpace Ef] [CompleteSpace Ec]
36 
37 /-- Every original component trace lies in the actual reconstructed cycle. -/
38 theorem component_subset_trace (n : ℕ) (f : Fin n → ℝ → ℂ)
39     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
40     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
41     (hclosed : ∀ i, f i 1 = f i 0) (i : Fin n) :
42     f i '' Icc (0:ℝ) 1 ⊆ (cycleOfRectifiable n f hv hc hclosed).trace := by
43   intro z hz
44   rw [trace_cycleOfRectifiable n f hv hc hclosed]
45   exact ⟨i,hz⟩
46 
47 /-- Proven RS/velocity representation for each original Dunford integral. -/
48 theorem rectifiableDunford_eq_dunfordIntegral (n : ℕ) (f : Fin n → ℝ → ℂ)
49     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
50     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
51     (hclosed : ∀ i, f i 1 = f i 0)
52     (h : ℂ → ℂ) (hh : ContinuousOn h (cycleOfRectifiable n f hv hc hclosed).trace)
53     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
54     [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E]
55     (T : E →L[ℂ] E)
56     (hT : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ T) :
57     rectifiableDunford n f h T = dunfordIntegral (cycleOfRectifiable n f hv hc hclosed) h T := by
58   unfold rectifiableDunford dunfordIntegral
59   apply congrArg (fun A ↦ (2 * (Real.pi : ℂ) * Complex.I)⁻¹ • A)
60   exact sum_taggedContourIntegral_eq_lineIntegral n f hv hc hclosed
61     (fun i ↦ (hh.smul (continuousOn_resolvent_trace _ T hT)).mono
62       (component_subset_trace n f hv hc hclosed i))
63 
64 /-- The actual classical finite-rectifiable-cycle defect identity. -/
65 theorem rectifiableDunford_defect (n : ℕ) (f : Fin n → ℝ → ℂ)
66     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
67     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
68     (hclosed : ∀ i, f i 1 = f i 0)
69     (h : ℂ → ℂ) (hh : ContinuousOn h (cycleOfRectifiable n f hv hc hclosed).trace)
70     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
71     (hf : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ Tf)
72     (hcc : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ Tc) :
73     C.comp (rectifiableDunford n f h Tf) - (rectifiableDunford n f h Tc).comp C =
74       (2 * (Real.pi : ℂ) * Complex.I)⁻¹ •
75         ∑ i : Fin n, taggedContourIntegral (f i) (fun z ↦ h z •
76           ((resolvent Tc z).comp ((continuousDefect C Tf Tc).comp (resolvent Tf z)))) 0 1 := by
77   have hfc := continuousOn_resolvent_trace (cycleOfRectifiable n f hv hc hclosed) Tf hf
78   have hccc := continuousOn_resolvent_trace (cycleOfRectifiable n f hv hc hclosed) Tc hcc
79   have hcont := hh.smul (hccc.clm_comp
80     ((continuousOn_const (c := continuousDefect C Tf Tc)).clm_comp hfc))
81   rw [rectifiableDunford_eq_dunfordIntegral n f hv hc hclosed h hh Tf hf,
82     rectifiableDunford_eq_dunfordIntegral n f hv hc hclosed h hh Tc hcc,
83     dunfordIntegral_defect _ h hh C Tf Tc hf hcc]
84   apply congrArg (fun A ↦ (2 * (Real.pi : ℂ) * Complex.I)⁻¹ • A)
85   exact (sum_taggedContourIntegral_eq_lineIntegral n f hv hc hclosed
86     (fun i ↦ hcont.mono (component_subset_trace n f hv hc hclosed i))).symm
87 
88 /-- The paper's separate supremum factors with the original geometric length,
89 proved using the sufficient velocity-length upper bound. -/
90 theorem rectifiableDunford_norm_defect_le_geometric_sup (n : ℕ) (f : Fin n → ℝ → ℂ)
91     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
92     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
93     (hclosed : ∀ i, f i 1 = f i 0)
94     (h : ℂ → ℂ) (hh : ContinuousOn h (cycleOfRectifiable n f hv hc hclosed).trace)
95     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
96     (hf : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ Tf)
97     (hcc : (cycleOfRectifiable n f hv hc hclosed).trace ⊆ resolventSet ℂ Tc) :
98     ‖C.comp (rectifiableDunford n f h Tf) - (rectifiableDunford n f h Tc).comp C‖ ≤
99       (∑ i : Fin n, geometricLength (f i)) / (2 * Real.pi) *
100         (cycleOfRectifiable n f hv hc hclosed).supNorm h * ‖continuousDefect C Tf Tc‖ *
101         (cycleOfRectifiable n f hv hc hclosed).supNorm (resolvent Tc) *
102         (cycleOfRectifiable n f hv hc hclosed).supNorm (resolvent Tf) := by
103   let Γ := cycleOfRectifiable n f hv hc hclosed
104   have hfc := continuousOn_resolvent_trace Γ Tf hf
105   have hccc := continuousOn_resolvent_trace Γ Tc hcc
106   have hh0 := Γ.supNorm_nonneg hh
107   have hfc0 := Γ.supNorm_nonneg hfc
108   have hcc0 := Γ.supNorm_nonneg hccc
109   rw [rectifiableDunford_eq_dunfordIntegral n f hv hc hclosed h hh Tf hf,
110     rectifiableDunford_eq_dunfordIntegral n f hv hc hclosed h hh Tc hcc]
111   apply (dunfordIntegral_norm_defect_le_sup Γ h hh C Tf Tc hf hcc).trans
112   gcongr
113   exact length_cycleOfRectifiable_le n f hv hc hclosed
114 
115 end Operators
116 end Komorebi.PaperII.ReleaseRectifiableDefect

Back to source controls