BanachDefects.lean

1 import KomorebiPaperVI.Semigroups
2 
3 /-! Author: Komorebi P. Duhamel defects in a real Banach algebra. -/
4 namespace KomorebiPaperVI.BanachDefects
5 open KomorebiPaperVI.Semigroups
6 variable {R : Type*} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R]
7 
8 theorem duhamel_derivative (A B C : R) (t r : ℝ) :
9     HasDerivAt (fun u => transfer B (t-u)*C*transfer A u)
10       (transfer B (t-r)*(C*A-B*C)*transfer A r) r := by
11   have hsub : HasDerivAt (fun u : ℝ => t-u) (-1) r := by
12     convert! (hasDerivAt_const r t).sub (hasDerivAt_id r) using 1
13     simp
14   have hB : HasDerivAt (fun u : ℝ => transfer B (t-u))
15       ((-1:ℝ) • (transfer B (t-r)*B)) r := (transfer_derivative_right B (t-r)).scomp r
16     hsub
17   convert! (hB.mul_const C).mul (transfer_derivative_left A r) using 1
18   simp only [neg_smul,one_smul]
19   noncomm_ring
20 
21 theorem duhamel (A B C : R) (t : ℝ) :
22     C*transfer A t-transfer B t*C=
23       ∫ r in 0..t,transfer B (t-r)*(C*A-B*C)*transfer A r := by
24   have hc : Continuous (fun r => transfer B (t-r)*(C*A-B*C)*transfer A r) := by fun_prop
25   have h := intervalIntegral.integral_eq_sub_of_hasDerivAt
26     (fun r _ => duhamel_derivative A B C t r) (hc.intervalIntegrable 0 t)
27   simpa only [sub_self,transfer_zero,zero_sub,sub_zero,one_mul,mul_one] using h.symm
28 
29 theorem contraction_bound (A B C : R) (t : ℝ) (ht : 0 ≤ t)
30     (hA : ∀ r,0 ≤ r → ‖transfer A r‖ ≤ 1)
31     (hB : ∀ r,0 ≤ r → ‖transfer B r‖ ≤ 1) :
32     ‖C*transfer A t-transfer B t*C‖ ≤ t*‖C*A-B*C‖ := by
33   rw [duhamel]
34   have hc : Continuous (fun r => transfer B (t-r)*(C*A-B*C)*transfer A r) := by fun_prop
35   calc
36     _ ≤ ∫ r in 0..t,‖transfer B (t-r)*(C*A-B*C)*transfer A r‖ :=
37       intervalIntegral.norm_integral_le_integral_norm ht
38     _ ≤ ∫ _ in 0..t,‖C*A-B*C‖ := by
39       apply intervalIntegral.integral_mono_on ht (hc.norm.intervalIntegrable 0 t) intervalIntegrable_const
40       intro r hr
41       calc
42         _ ≤ ‖transfer B (t-r)‖*‖C*A-B*C‖*‖transfer A r‖ := norm_mul_le_of_le (norm_mul_le _ _) le_rfl
43         _ ≤ 1*‖C*A-B*C‖*1 := by gcongr; exact hB (t-r) (by linarith [hr.2]); exact hA r hr.1
44         _ = _ := by ring
45     _ = _ := by simp [smul_eq_mul]
46 
47 end KomorebiPaperVI.BanachDefects

Back to source controls