ReleaseDefectCompatibility.lean

1 import KomorebiVerification.PaperII.ReleaseDefectTower
2 import KomorebiVerification.PaperII.ReleaseAnalyticExponential
3 import KomorebiVerification.PaperII.ReleaseAnalyticContour
4 
5 set_option autoImplicit false
6 noncomputable section
7 namespace Komorebi.PaperII.ReleaseDefectCompatibility
8 open TypedLinearDefects ReleaseDefectTower ReleaseAnalyticExponential ReleaseAnalyticContour
9 universe u v
10 
11 /-- Exact arbitrary-depth exponential compatibility on a genuinely typed
12 Banach-space tower, derived from its local zero defects and Duhamel. -/
13 theorem multilevel_exponential_compatible
14     {𝕜 : Type u} [RCLike 𝕜] {X : ℕ → Type v}
15     [∀ n, NormedAddCommGroup (X n)] [∀ n, NormedSpace 𝕜 (X n)]
16     [∀ n, NormedSpace ℝ (X n)] [∀ n, IsScalarTower ℝ 𝕜 (X n)]
17     [∀ n, CompleteSpace (X n)]
18     (C : ∀ n, X (n + 1) →L[𝕜] X n) (T : ∀ n, X n →L[𝕜] X n)
19     (L : ℕ) (h : ∀ k : Fin L,
20       continuousDefect (C k.val) (T (k.val + 1)) (T k.val) = 0) (t : 𝕜) :
21     (continuousSegment C (Nat.zero_le L)).comp (NormedSpace.exp (t • T L)) =
22       (NormedSpace.exp (t • T 0)).comp (continuousSegment C (Nat.zero_le L)) := by
23   apply exponential_compatible_of_defect_eq_zero
24   exact sub_eq_zero.mpr (continuous_multilevel_compatible C T L h)
25 
26 /-- Exact arbitrary-depth compatibility of actual chosen-cycle integrals.
27 Canonical holomorphic-calculus identification remains a separate bridge. -/
28 theorem multilevel_dunfordIntegral_compatible
29     {X : ℕ → Type v}
30     [∀ n, NormedAddCommGroup (X n)] [∀ n, NormedSpace ℂ (X n)]
31     [∀ n, NormedSpace ℝ (X n)] [∀ n, IsScalarTower ℝ ℂ (X n)]
32     [∀ n, CompleteSpace (X n)]
33     (C : ∀ n, X (n + 1) →L[ℂ] X n) (T : ∀ n, X n →L[ℂ] X n)
34     (L : ℕ) (hd : ∀ k : Fin L,
35       continuousDefect (C k.val) (T (k.val + 1)) (T k.val) = 0)
36     (Γ : IntegralCycle) (h : ℂ → ℂ) (hh : ContinuousOn h Γ.trace)
37     (hf : Γ.trace ⊆ resolventSet ℂ (T L)) (hc : Γ.trace ⊆ resolventSet ℂ (T 0)) :
38     (continuousSegment C (Nat.zero_le L)).comp (dunfordIntegral Γ h (T L)) =
39       (dunfordIntegral Γ h (T 0)).comp (continuousSegment C (Nat.zero_le L)) := by
40   apply dunfordIntegral_compatible_of_defect_eq_zero Γ h hh _ _ _ hf hc
41   exact sub_eq_zero.mpr (continuous_multilevel_compatible C T L hd)
42 end Komorebi.PaperII.ReleaseDefectCompatibility

Back to source controls