ComplexMemory.lean

1 import KomorebiPaperVI.MemoryLaplace
2 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
3 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
4 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
5 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
6 
7 /-! Author: Komorebi P. Literal complex Laplace inversion and memory/self-energy.
8 The general nonnormal spectral-abscissa-to-growth implication is not asserted here. -/
9 namespace KomorebiPaperVI.ComplexMemory
10 open Set Filter MeasureTheory NormedSpace
11 open KomorebiPaperVI.Semigroups
12 set_option backward.isDefEq.respectTransparency false
13 attribute [local instance] IsStarNormal.instContinuousFunctionalCalculus
14 variable {R : Type*} [CStarAlgebra R]
15 
16 noncomputable def damped (A : R) (z : ℂ) (t : ℝ) : R := Complex.exp (-z*t) • transfer A t
17 
18 theorem damped_eq_shifted (A : R) (z : ℂ) (t : ℝ) :
19     damped A z t=transfer (A-algebraMap ℂ R z) t := by
20   let : NormedAlgebra ℚ R := NormedAlgebra.restrictScalars ℚ ℝ R
21   have he : t • (A-algebraMap ℂ R z)=algebraMap ℂ R (-z*t)+t • A := by
22     simp only [smul_sub,Algebra.algebraMap_eq_smul_one,neg_mul,neg_smul]
23     rw [← smul_assoc,Complex.real_smul,mul_comm (t:ℂ) z]
24     abel
25   simp only [damped,transfer]
26   rw [he,exp_add_of_commute (Algebra.commutes _ _),← algebraMap_exp_comm,
27     ← Complex.exp_eq_exp_ℂ,Algebra.algebraMap_eq_smul_one,smul_mul_assoc,one_mul]
28 
29 theorem shifted_decay (A : R) (z : ℂ) (M w : ℝ) (_hz : w < z.re)
30     (hA : ∀ t,0 ≤ t → ‖transfer A t‖ ≤ M*Real.exp (w*t)) :
31     ∀ t,0 ≤ t → ‖transfer (A-algebraMap ℂ R z) t‖ ≤ M*Real.exp (-(z.re-w)*t) := by
32   intro t ht
33   rw [← damped_eq_shifted,damped,norm_smul,Complex.norm_exp]
34   have hre : (-z*(t:ℂ)).re= -z.re*t := by simp
35   rw [hre]
36   calc
37     _ ≤ Real.exp (-z.re*t)*(M*Real.exp (w*t)) := mul_le_mul_of_nonneg_left (hA t ht) (Real.exp_pos _).le
38     _ = _ := by
39       rw [mul_left_comm,← Real.exp_add]
40       congr 2
41       ring
42 
43 theorem integral_transfer_right (B : R) (M d : ℝ) (hd : 0 < d)
44     (hB : ∀ t,0 ≤ t → ‖transfer B t‖ ≤ M*Real.exp (-d*t)) :
45     (∫ t in Ioi 0,transfer B t)*B= -1 := by
46   have hi := MemoryLaplace.decay_integrable B M d hd hB
47   have hprod : IntegrableOn (fun t => transfer B t*B) (Ioi 0) :=
48     ((ContinuousLinearMap.mul ℝ R).flip B).integrable_comp hi
49   have hf := integral_Ioi_of_hasDerivAt_of_tendsto'
50     (fun t (_ : t∈Ici (0:ℝ)) => transfer_derivative_right B t)
51     hprod (MemoryLaplace.decay_tendsto_zero B M d hd hB)
52   rw [integral_mul_const_of_integrable hi,transfer_zero,zero_sub] at hf
53   exact hf
54 
55 theorem laplace_inverse (A : R) (z : ℂ) (M w : ℝ) (hz : w < z.re)
56     (hA : ∀ t,0 ≤ t → ‖transfer A t‖ ≤ M*Real.exp (w*t)) :
57     IntegrableOn (damped A z) (Ioi 0) ∧
58     IsUnit (algebraMap ℂ R z-A) ∧
59     (∫ t in Ioi 0,damped A z t)=Ring.inverse (algebraMap ℂ R z-A) := by
60   have hd : 0 < z.re-w := sub_pos.mpr hz
61   have hB := shifted_decay A z M w hz hA
62   have hi := MemoryLaplace.decay_integrable (A-algebraMap ℂ R z) M (z.re-w) hd hB
63   have he : damped A z=transfer (A-algebraMap ℂ R z) := funext (damped_eq_shifted A z)
64   rw [he]
65   have hl := MemoryLaplace.integral_generator_transfer (A-algebraMap ℂ R z) M (z.re-w) hd hB
66   have hr := integral_transfer_right (A-algebraMap ℂ R z) M (z.re-w) hd hB
67   have hn : algebraMap ℂ R z-A= -(A-algebraMap ℂ R z) := by abel
68   have hl' : (algebraMap ℂ R z-A)*(∫ t in Ioi 0,transfer (A-algebraMap ℂ R z) t)=1 := by rw [hn,neg_mul,hl,neg_neg]
69   have hr' : (∫ t in Ioi 0,transfer (A-algebraMap ℂ R z) t)*(algebraMap ℂ R z-A)=1 := by rw [hn,mul_neg,hr,neg_neg]
70   have hu : IsUnit (algebraMap ℂ R z-A) := ⟨⟨_,_,hl',hr'⟩,rfl⟩
71   refine ⟨hi,hu,?_⟩
72   calc
73     _ = Ring.inverse (algebraMap ℂ R z-A)*((algebraMap ℂ R z-A)*(∫ t in Ioi 0,transfer (A-algebraMap ℂ R z) t)) :=
74       (Ring.inverse_mul_cancel_left _ _ hu).symm
75     _ = _ := by rw [hl',mul_one]
76 
77 theorem memory_self_energy (A U V : R) (z : ℂ) (M w : ℝ) (hz : w < z.re)
78     (hA : ∀ t,0 ≤ t → ‖transfer A t‖ ≤ M*Real.exp (w*t)) :
79     IntegrableOn (fun t : ℝ => Complex.exp (-z*t) • (U*transfer A t*V)) (Ioi 0) ∧
80     (∫ t : ℝ in Ioi 0,Complex.exp (-z*t) • (U*transfer A t*V))=U*Ring.inverse (algebraMap ℂ R z-A)*V := by
81   have h := laplace_inverse A z M w hz hA
82   have he : (fun t : ℝ => Complex.exp (-z*t) • (U*transfer A t*V))=(fun t => U*damped A z t*V) := by
83     ext t
84     simp [damped,Algebra.mul_smul_comm,Algebra.smul_mul_assoc]
85   rw [he]
86   have hu : IntegrableOn (fun t => U*damped A z t) (Ioi 0) := (ContinuousLinearMap.mul ℝ R U).integrable_comp h.1
87   refine ⟨((ContinuousLinearMap.mul ℝ R).flip V).integrable_comp hu,?_⟩
88   rw [integral_mul_const_of_integrable hu,integral_const_mul_of_integrable h.1,h.2.2]
89 
90 
91 theorem normal_growth (A : R) [IsStarNormal A] (w : ℝ)
92     (hw : ∀ z∈spectrum ℂ A,z.re ≤ w) (t : ℝ) (ht : 0 ≤ t) :
93     ‖transfer A t‖ ≤ Real.exp (w*t) := by
94   rw [transfer,← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ) (a := t • A),
95     ← cfc_comp_smul t (NormedSpace.exp : ℂ → ℂ) A]
96   apply norm_cfc_le (Real.exp_pos _).le
97   intro z hz
98   rw [← Complex.exp_eq_exp_ℂ,Complex.norm_exp,Real.exp_le_exp]
99   simpa only [Complex.smul_re,smul_eq_mul,mul_comm] using mul_le_mul_of_nonneg_left (hw z hz) ht
100 
101 theorem normal_memory_self_energy (A U V : R) [IsStarNormal A] (z : ℂ) (w : ℝ)
102     (hw : ∀ v∈spectrum ℂ A,v.re ≤ w) (hz : w < z.re) :
103     IntegrableOn (fun t : ℝ => Complex.exp (-z*t) • (U*transfer A t*V)) (Ioi 0) ∧
104     (∫ t : ℝ in Ioi 0,Complex.exp (-z*t) • (U*transfer A t*V))=U*Ring.inverse (algebraMap ℂ R z-A)*V :=
105   memory_self_energy A U V z 1 w hz (fun t ht => by simpa using normal_growth A w hw t ht)
106 
107 end KomorebiPaperVI.ComplexMemory

Back to source controls