ReleaseAnalyticExponential.lean

1 import KomorebiVerification.PaperII.TypedLinearDefects
2 import Mathlib.Analysis.SpecialFunctions.Exponential
3 import Mathlib.Analysis.Calculus.Deriv.Mul
4 import Mathlib.Analysis.Calculus.Deriv.Linear
5 import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
6 
7 set_option autoImplicit false
8 noncomputable section
9 namespace Komorebi.PaperII.ReleaseAnalyticExponential
10 open scoped Topology
11 open MeasureTheory
12 open TypedLinearDefects
13 universe u v w
14 variable {𝕜 : Type u} [RCLike 𝕜]
15 variable {Ef : Type v} {Ec : Type w}
16 variable [NormedAddCommGroup Ef] [NormedAddCommGroup Ec]
17 variable [NormedSpace 𝕜 Ef] [NormedSpace 𝕜 Ec]
18 variable [CompleteSpace Ef] [CompleteSpace Ec]
19 
20 /-- The genuinely rectangular operator path whose endpoint difference is the
21 exponential defect. -/
22 def exponentialPath (C : Ef →L[𝕜] Ec)
23     (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) (t s : 𝕜) : Ef →L[𝕜] Ec :=
24   (NormedSpace.exp ((t - s) • Tc)).comp
25     (C.comp (NormedSpace.exp (s • Tf)))
26 
27 /-- The Duhamel integrand, retaining coarse/fine multiplication order. -/
28 def exponentialKernel (C : Ef →L[𝕜] Ec)
29     (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) (t s : 𝕜) : Ef →L[𝕜] Ec :=
30   (NormedSpace.exp ((t - s) • Tc)).comp
31     ((continuousDefect C Tf Tc).comp (NormedSpace.exp (s • Tf)))
32 
33 /-- Actual Banach-algebra exponential differentiation and the typed bilinear
34 composition product rule produce the Duhamel kernel. -/
35 theorem hasDerivAt_exponentialPath
36     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) (t s : 𝕜) :
37     HasDerivAt (exponentialPath C Tf Tc t) (exponentialKernel C Tf Tc t s) s := by
38   have hc := (hasDerivAt_exp_smul_const Tc (t - s)).scomp s
39     ((hasDerivAt_id s).const_sub t)
40   have hf := hasDerivAt_exp_smul_const' Tf s
41   have h := hc.clm_comp ((hasDerivAt_const s C).clm_comp hf)
42   convert h using 1
43   · rfl
44   · ext x
45     simp [exponentialKernel, continuousDefect, sub_eq_add_neg, add_comm]
46 
47 /-- Continuity is derived from the actual exponential maps, not supplied as
48 an integration certificate. -/
49 theorem continuous_exponentialKernel
50     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) (t : 𝕜) :
51     Continuous (exponentialKernel C Tf Tc t) := by
52   have hf := (differentiable_exp_smul_const 𝕜 Tf).continuous
53   have hc : Continuous (fun s : 𝕜 => NormedSpace.exp ((t - s) • Tc)) :=
54     (differentiable_exp_smul_const 𝕜 Tc).continuous.comp
55       (continuous_const.sub continuous_id)
56   exact hc.clm_comp (continuous_const.clm_comp hf)
57 
58 omit [CompleteSpace Ef] [CompleteSpace Ec] in
59 @[simp] theorem exponentialPath_zero
60     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) (t : 𝕜) :
61     exponentialPath C Tf Tc t 0 = (NormedSpace.exp (t • Tc)).comp C := by
62   simp [exponentialPath, NormedSpace.exp_zero, ContinuousLinearMap.one_def]
63 
64 omit [CompleteSpace Ef] [CompleteSpace Ec] in
65 @[simp] theorem exponentialPath_self
66     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) (t : 𝕜) :
67     exponentialPath C Tf Tc t t = C.comp (NormedSpace.exp (t • Tf)) := by
68   simp [exponentialPath, NormedSpace.exp_zero, ContinuousLinearMap.one_def]
69 
70 omit [CompleteSpace Ef] [CompleteSpace Ec] in
71 /-- The pointwise estimate used inside the integral, requiring no relation
72 between the fine and coarse operator norms. -/
73 theorem norm_exponentialKernel_le
74     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) (t s : 𝕜) :
75     ‖exponentialKernel C Tf Tc t s‖ ≤
76       ‖continuousDefect C Tf Tc‖ *
77         (‖NormedSpace.exp ((t-s) • Tc)‖ * ‖NormedSpace.exp (s • Tf)‖) := by
78   unfold exponentialKernel
79   calc
80     _ ≤ ‖NormedSpace.exp ((t-s) • Tc)‖ *
81         ‖(continuousDefect C Tf Tc).comp (NormedSpace.exp (s • Tf))‖ :=
82       ContinuousLinearMap.opNorm_comp_le _ _
83     _ ≤ ‖NormedSpace.exp ((t-s) • Tc)‖ *
84         (‖continuousDefect C Tf Tc‖ * ‖NormedSpace.exp (s • Tf)‖) :=
85       mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le _ _) (norm_nonneg _)
86     _ = _ := by ac_rfl
87 
88 section RealParameter
89 variable [NormedSpace ℝ Ec]
90 variable [IsScalarTower ℝ 𝕜 Ec]
91 
92 /-- Duhamel's identity for every real time, including negative time, on real
93 or complex Banach spaces with their compatible real scalar structures. -/
94 theorem exponential_defect_real
95     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) (t : ℝ) :
96     C.comp (NormedSpace.exp ((t : 𝕜) • Tf)) -
97         (NormedSpace.exp ((t : 𝕜) • Tc)).comp C =
98       ∫ s : ℝ in 0..t, exponentialKernel C Tf Tc (t : 𝕜) (s : 𝕜) := by
99   have hd (s : ℝ) :
100       HasDerivAt (fun r : ℝ => exponentialPath C Tf Tc (t : 𝕜) (r : 𝕜))
101         (exponentialKernel C Tf Tc (t : 𝕜) (s : 𝕜)) s := by
102     convert! (hasDerivAt_exponentialPath C Tf Tc (t : 𝕜) (s : 𝕜)).scomp s
103       (RCLike.ofRealCLM (K := 𝕜)).hasDerivAt using 1
104     simp
105   have hi : IntervalIntegrable
106       (fun s : ℝ => exponentialKernel C Tf Tc (t : 𝕜) (s : 𝕜)) volume 0 t :=
107     ((continuous_exponentialKernel C Tf Tc (t : 𝕜)).comp RCLike.continuous_ofReal).intervalIntegrable _ _
108   simpa using (intervalIntegral.integral_eq_sub_of_hasDerivAt (fun s hs => hd s) hi).symm
109 
110 /-- The complex-time statement uses the actual straight-segment
111 parameterization s=u*t, so the integral includes the tangent factor t. -/
112 theorem exponential_defect_segment
113     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) (t : 𝕜) :
114     C.comp (NormedSpace.exp (t • Tf)) - (NormedSpace.exp (t • Tc)).comp C =
115       ∫ s : ℝ in (0:ℝ)..1, t • exponentialKernel C Tf Tc t (s • t) := by
116   have hd (s : ℝ) :
117       HasDerivAt (fun r : ℝ => exponentialPath C Tf Tc t (r • t))
118         (t • exponentialKernel C Tf Tc t (s • t)) s := by
119     convert! (hasDerivAt_exponentialPath C Tf Tc t (s • t)).scomp s
120       ((hasDerivAt_id s).smul_const t) using 1
121     simp
122   have hi : IntervalIntegrable
123       (fun s : ℝ => t • exponentialKernel C Tf Tc t (s • t)) volume 0 1 :=
124     by
125       have hk : Continuous (fun s : ℝ => exponentialKernel C Tf Tc t (s • t)) :=
126         (continuous_exponentialKernel C Tf Tc t).comp
127           (continuous_id.smul continuous_const)
128       exact (hk.const_smul t).intervalIntegrable _ _
129   simpa using (intervalIntegral.integral_eq_sub_of_hasDerivAt (fun s hs => hd s) hi).symm
130 
131 /-- The exact manuscript norm estimate for real nonnegative time. -/
132 theorem norm_exponential_defect_real_le
133     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec)
134     (t : ℝ) (ht : 0 ≤ t) :
135     ‖C.comp (NormedSpace.exp ((t : 𝕜) • Tf)) -
136         (NormedSpace.exp ((t : 𝕜) • Tc)).comp C‖ ≤
137       ‖continuousDefect C Tf Tc‖ *
138         ∫ s : ℝ in 0..t,
139           ‖NormedSpace.exp (((t : 𝕜) - (s : 𝕜)) • Tc)‖ *
140           ‖NormedSpace.exp ((s : 𝕜) • Tf)‖ := by
141   rw [exponential_defect_real]
142   have hf : Continuous (fun s : ℝ => NormedSpace.exp ((s : 𝕜) • Tf)) :=
143     (differentiable_exp_smul_const 𝕜 Tf).continuous.comp RCLike.continuous_ofReal
144   have hc : Continuous (fun s : ℝ => NormedSpace.exp (((t : 𝕜) - (s : 𝕜)) • Tc)) :=
145     (differentiable_exp_smul_const 𝕜 Tc).continuous.comp
146       (continuous_const.sub RCLike.continuous_ofReal)
147   calc
148     _ ≤ ∫ s : ℝ in 0..t, ‖continuousDefect C Tf Tc‖ *
149           (‖NormedSpace.exp (((t : 𝕜) - (s : 𝕜)) • Tc)‖ *
150            ‖NormedSpace.exp ((s : 𝕜) • Tf)‖) := by
151       apply intervalIntegral.norm_integral_le_of_norm_le ht
152       · exact Filter.Eventually.of_forall (fun s hs => norm_exponentialKernel_le C Tf Tc _ _)
153       · exact (continuous_const.mul (hc.norm.mul hf.norm)).intervalIntegrable _ _
154     _ = _ := intervalIntegral.integral_const_mul _ _
155 
156 /-- A zero one-step defect gives the exact complex/real exponential
157 compatibility, using the segment formula just proved. -/
158 theorem exponential_compatible_of_defect_eq_zero
159     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec)
160     (h : continuousDefect C Tf Tc = 0) (t : 𝕜) :
161     C.comp (NormedSpace.exp (t • Tf)) = (NormedSpace.exp (t • Tc)).comp C := by
162   apply sub_eq_zero.mp
163   rw [exponential_defect_segment]
164   simp [exponentialKernel, h]
165 end RealParameter
166 end Komorebi.PaperII.ReleaseAnalyticExponential

Back to source controls