Semigroups.lean

1 import KomorebiPaperVI.Algebra
2 import Mathlib.Analysis.SpecialFunctions.Exponential
3 import Mathlib.Analysis.Calculus.Deriv.Mul
4 import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
5 import Mathlib.Tactic
6 
7 /-! Author: Komorebi P. Banach-algebra exponentials and rectangular bounded-operator Duhamel. -/
8 namespace KomorebiPaperVI.Semigroups
9 open NormedSpace
10 open scoped Topology
11 
12 section BanachAlgebra
13 variable {R : Type*} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R]
14 
15 noncomputable def transfer (A : R) (t : ℝ) : R := exp (t • A)
16 
17 omit [CompleteSpace R] in
18 theorem transfer_zero (A : R) : transfer A 0 = 1 := by simp [transfer]
19 
20 theorem transfer_add (A : R) (s t : ℝ) : transfer A (s+t) = transfer A s*transfer A t := by
21   let : NormedAlgebra ℚ R := NormedAlgebra.restrictScalars ℚ ℝ R
22   dsimp [transfer]
23   rw [add_smul]
24   exact exp_add_of_commute (((Commute.refl A).smul_left s).smul_right t)
25 
26 theorem transfer_derivative_right (A : R) (t : ℝ) :
27     HasDerivAt (transfer A) (transfer A t*A) t := hasDerivAt_exp_smul_const A t
28 
29 theorem transfer_derivative_left (A : R) (t : ℝ) :
30     HasDerivAt (transfer A) (A*transfer A t) t := hasDerivAt_exp_smul_const' A t
31 
32 @[fun_prop]
33 theorem transfer_continuous (A : R) : Continuous (transfer A) := by
34   exact continuous_iff_continuousAt.mpr fun t => (transfer_derivative_right A t).continuousAt
35 
36 theorem transfer_intertwining (C A B : R) (h : C*A=B*C) (t : ℝ) :
37     C*transfer A t=transfer B t*C := by
38   let : NormedAlgebra ℚ R := NormedAlgebra.restrictScalars ℚ ℝ R
39   have hs : SemiconjBy C (t • A) (t • B) :=
40     (show SemiconjBy C A B from h).smul_right t
41   exact hs.exp_right
42 
43 
44 theorem exponential_packet_convolution {I : Type*} [Fintype I]
45     (P : I → R) (hP : ∑ i, P i=1) (hid : ∀ i, P i*P i=P i)
46     (A : R) (s t : ℝ) (b a : I) :
47     Algebra.block P (transfer A (s+t)) b a =
48       ∑ c, Algebra.block P (transfer A s) b c*Algebra.block P (transfer A t) c a :=
49   Algebra.packet_semigroup_convolution P hP hid (transfer A) (transfer_add A) s t b a
50 
51 end BanachAlgebra
52 
53 section Rectangular
54 variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
55     [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
56 
57 theorem duhamel_integrand_derivative (A : E →L[ℝ] E) (B : F →L[ℝ] F)
58     (C : E →L[ℝ] F) (t r : ℝ) :
59     HasDerivAt (fun u => (transfer B (t-u)).comp (C.comp (transfer A u)))
60       ((transfer B (t-r)).comp ((C.comp A-B.comp C).comp (transfer A r))) r := by
61   have hb : HasDerivAt (fun u => transfer B (t-u)) (-(transfer B (t-r)*B)) r := by
62     simpa [Function.comp_def] using (transfer_derivative_right B (t-r)).scomp r
63       ((hasDerivAt_const r t).sub (hasDerivAt_id r))
64   have hc := (hasDerivAt_const r C).clm_comp (transfer_derivative_left A r)
65   convert hb.clm_comp hc using 1
66   ext x
67   simp [mul_apply_eq_comp, ContinuousLinearMap.comp_apply]
68   abel
69 
70 theorem duhamel_rectangular (A : E →L[ℝ] E) (B : F →L[ℝ] F)
71     (C : E →L[ℝ] F) (t : ℝ) :
72     C.comp (transfer A t)-(transfer B t).comp C =
73       ∫ r in 0..t, (transfer B (t-r)).comp ((C.comp A-B.comp C).comp (transfer A r)) := by
74   have hc : Continuous (fun r => (transfer B (t-r)).comp
75       ((C.comp A-B.comp C).comp (transfer A r))) := by
76     fun_prop
77   have h := intervalIntegral.integral_eq_sub_of_hasDerivAt
78     (fun r _ => duhamel_integrand_derivative A B C t r) (hc.intervalIntegrable 0 t)
79   simpa [transfer_zero, ContinuousLinearMap.one_def] using h.symm
80 
81 theorem exact_rectangular_intertwining (A : E →L[ℝ] E) (B : F →L[ℝ] F)
82     (C : E →L[ℝ] F) (h : C.comp A=B.comp C) (t : ℝ) :
83     C.comp (transfer A t)=(transfer B t).comp C := by
84   have hd := duhamel_rectangular A B C t
85   simp only [h, sub_self, ContinuousLinearMap.zero_comp, ContinuousLinearMap.comp_zero,
86     intervalIntegral.integral_zero] at hd
87   exact sub_eq_zero.mp hd
88 
89 theorem contraction_duhamel_bound (A : E →L[ℝ] E) (B : F →L[ℝ] F)
90     (C : E →L[ℝ] F) (t : ℝ) (ht : 0 ≤ t)
91     (hA : ∀ u, 0 ≤ u → ‖transfer A u‖ ≤ 1)
92     (hB : ∀ u, 0 ≤ u → ‖transfer B u‖ ≤ 1) :
93     ‖C.comp (transfer A t)-(transfer B t).comp C‖ ≤ t*‖C.comp A-B.comp C‖ := by
94   rw [duhamel_rectangular]
95   have h := intervalIntegral.norm_integral_le_of_norm_le_const (a := 0) (b := t)
96     (C := ‖C.comp A-B.comp C‖)
97     (f := fun r => (transfer B (t-r)).comp ((C.comp A-B.comp C).comp (transfer A r)))
98     (fun r hr => ?_)
99   · simpa [abs_of_nonneg ht, mul_comm] using h
100   · have hr' : r ∈ Set.Ioc 0 t := by simpa [Set.uIoc_of_le ht] using hr
101     calc
102       _ ≤ ‖transfer B (t-r)‖ * ‖(C.comp A-B.comp C).comp (transfer A r)‖ :=
103         ContinuousLinearMap.opNorm_comp_le _ _
104       _ ≤ 1*(‖C.comp A-B.comp C‖*1) :=
105         mul_le_mul (hB _ (sub_nonneg.mpr hr'.2))
106           ((ContinuousLinearMap.opNorm_comp_le _ _).trans
107             (mul_le_mul_of_nonneg_left (hA _ hr'.1.le) (norm_nonneg _)))
108           (norm_nonneg _) (by norm_num)
109       _ = _ := by ring
110 
111 end Rectangular
112 end KomorebiPaperVI.Semigroups

Back to source controls