ComplexSemigroups.lean

1 import KomorebiPaperVI.Semigroups
2 import KomorebiPaperVI.FractionalSemigroup
3 import KomorebiPaperVI.RectangularFractional
4 
5 /-! Author: Komorebi P. Real-time Duhamel for bounded complex linear maps. -/
6 set_option backward.isDefEq.respectTransparency false
7 namespace KomorebiPaperVI.ComplexSemigroups
8 open KomorebiPaperVI.Semigroups
9 
10 variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
11     [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
12 
13 theorem duhamel_integrand_derivative (A : E →L[ℂ] E) (B : F →L[ℂ] F)
14     (C : E →L[ℂ] F) (t r : ℝ) :
15     HasDerivAt (fun u => (transfer B (t-u)).comp (C.comp (transfer A u)))
16       ((transfer B (t-r)).comp ((C.comp A-B.comp C).comp (transfer A r))) r := by
17   have hb : HasDerivAt (fun u => transfer B (t-u)) (-(transfer B (t-r)*B)) r := by
18     simpa [Function.comp_def] using (transfer_derivative_right B (t-r)).scomp r
19       ((hasDerivAt_const r t).sub (hasDerivAt_id r))
20   have hc := ((ContinuousLinearMap.compL ℂ E E F).bilinearRestrictScalars ℝ).hasDerivAt_of_bilinear
21     (fun _ => hasDerivAt_const r C) (fun _ => transfer_derivative_left A r)
22   have hh := ((ContinuousLinearMap.compL ℂ E F F).bilinearRestrictScalars ℝ).hasDerivAt_of_bilinear
23     (fun _ => hb) (fun _ => hc)
24   convert! hh using 1
25   ext x
26   simp [mul_apply_eq_comp, ContinuousLinearMap.comp_apply]
27   abel
28 
29 theorem duhamel_rectangular (A : E →L[ℂ] E) (B : F →L[ℂ] F)
30     (C : E →L[ℂ] F) (t : ℝ) :
31     C.comp (transfer A t)-(transfer B t).comp C =
32       ∫ r in 0..t, (transfer B (t-r)).comp ((C.comp A-B.comp C).comp (transfer A r)) := by
33   have hc : Continuous (fun r => (transfer B (t-r)).comp
34       ((C.comp A-B.comp C).comp (transfer A r))) := by
35     fun_prop
36   have h := intervalIntegral.integral_eq_sub_of_hasDerivAt
37     (fun r _ => duhamel_integrand_derivative A B C t r) (hc.intervalIntegrable 0 t)
38   simpa [transfer_zero, ContinuousLinearMap.one_def] using h.symm
39 
40 theorem exact_rectangular_intertwining (A : E →L[ℂ] E) (B : F →L[ℂ] F)
41     (C : E →L[ℂ] F) (h : C.comp A=B.comp C) (t : ℝ) :
42     C.comp (transfer A t)=(transfer B t).comp C := by
43   have hd := duhamel_rectangular A B C t
44   simp only [h, sub_self, ContinuousLinearMap.zero_comp, ContinuousLinearMap.comp_zero,
45     intervalIntegral.integral_zero] at hd
46   exact sub_eq_zero.mp hd
47 
48 theorem contraction_duhamel_bound (A : E →L[ℂ] E) (B : F →L[ℂ] F)
49     (C : E →L[ℂ] F) (t : ℝ) (ht : 0 ≤ t)
50     (hA : ∀ u, 0 ≤ u → ‖transfer A u‖ ≤ 1)
51     (hB : ∀ u, 0 ≤ u → ‖transfer B u‖ ≤ 1) :
52     ‖C.comp (transfer A t)-(transfer B t).comp C‖ ≤ t*‖C.comp A-B.comp C‖ := by
53   rw [duhamel_rectangular]
54   have h := intervalIntegral.norm_integral_le_of_norm_le_const (a := 0) (b := t)
55     (C := ‖C.comp A-B.comp C‖)
56     (f := fun r => (transfer B (t-r)).comp ((C.comp A-B.comp C).comp (transfer A r)))
57     (fun r hr => ?_)
58   · simpa [abs_of_nonneg ht, mul_comm] using h
59   · have hr' : r ∈ Set.Ioc 0 t := by simpa [Set.uIoc_of_le ht] using hr
60     calc
61       _ ≤ ‖transfer B (t-r)‖ * ‖(C.comp A-B.comp C).comp (transfer A r)‖ :=
62         ContinuousLinearMap.opNorm_comp_le _ _
63       _ ≤ 1*(‖C.comp A-B.comp C‖*1) :=
64         mul_le_mul (hB _ (sub_nonneg.mpr hr'.2))
65           ((ContinuousLinearMap.opNorm_comp_le _ _).trans
66             (mul_le_mul_of_nonneg_left (hA _ hr'.1.le) (norm_nonneg _)))
67           (norm_nonneg _) (by norm_num)
68       _ = _ := by ring
69 
70 end KomorebiPaperVI.ComplexSemigroups

Back to source controls