NonnormalMemory.lean

1 import KomorebiPaperVI.ComplexMemory
2 import KomorebiPaperVI.CanonicalJets
3 import KomorebiPaperVI.ScalarDecay
4 import Mathlib.Algebra.Algebra.Bilinear
5 
6 /-! Author: Komorebi P. Spectral half-plane Laplace inversion for arbitrary finite-dimensional
7 complex algebras. Generalized eigenspaces, including nilpotent Jordan parts, supply the decay. -/
8 namespace KomorebiPaperVI.NonnormalMemory
9 open Module Set Filter MeasureTheory NormedSpace
10 open scoped Topology
11 open KomorebiPaperVI.Semigroups KomorebiPaperVI.ComplexMemory
12 set_option backward.isDefEq.respectTransparency false
13 variable {R : Type*} [CStarAlgebra R] [FiniteDimensional ℂ R]
14 
15 omit [FiniteDimensional ℂ R] in
16 theorem left_shift_power (A : R) (μ : ℂ) (k : ℕ) (x : R) :
17     ((LinearMap.mulLeft ℂ A-μ • 1)^k) x=(A-μ • 1)^k*x := by
18   have he : LinearMap.mulLeft ℂ A-μ • 1=LinearMap.mulLeft ℂ (A-μ • 1) := by
19     ext y
20     simp [sub_mul,Algebra.smul_mul_assoc]
21   rw [he,LinearMap.pow_mulLeft,LinearMap.mulLeft_apply]
22 
23 omit [FiniteDimensional ℂ R] in
24 theorem component_spectrum (A : R) (μ : ℂ) (x : R)
25     (hx : x ∈ (Module.End.maxGenEigenspace (LinearMap.mulLeft ℂ A)) μ) (hne : x ≠ 0) :
26     μ ∈ spectrum ℂ A := by
27   have hv : (Module.End.HasUnifEigenvector (LinearMap.mulLeft ℂ A)) μ ⊤ x := ⟨hx,hne⟩
28   have he : (Module.End.HasEigenvalue (LinearMap.mulLeft ℂ A)) μ :=
29     (Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one (by simp : (0:ℕ∞)<⊤)).mp hv.hasUnifEigenvalue
30   obtain ⟨y,hy⟩ := he.exists_hasEigenvector
31   rw [spectrum.mem_iff]
32   rintro ⟨u,hu⟩
33   have hz : (u:R)*y=0 := by
34     rw [hu,sub_mul,Algebra.algebraMap_eq_smul_one,Algebra.smul_mul_assoc,one_mul]
35     exact sub_eq_zero.mpr hy.apply_eq_smul.symm
36   exact hy.2 ((Units.mul_right_eq_zero u).mp hz)
37 
38 theorem exp_mul_component (A : R) (μ : ℂ) (x : R)
39     (hx : x ∈ (Module.End.maxGenEigenspace (LinearMap.mulLeft ℂ A)) μ) (t : ℝ) :
40     transfer A t*x=Complex.exp (μ*t) •
41       ∑ k ∈ Finset.range (finrank ℂ R),((t:ℂ)^k/(k.factorial:ℂ)) • ((A-μ • 1)^k*x) := by
42   classical
43   let : NormedAlgebra ℚ R := NormedAlgebra.restrictScalars ℚ ℝ R
44   let D := A-μ • 1
45   have hkill (k : ℕ) (hk : finrank ℂ R ≤ k) : D^k*x=0 := by
46     rw [← left_shift_power]
47     exact CanonicalJets.power_kills _ μ x hx k hk
48   have hs := (exp_series_hasSum_exp' (𝕂 := ℂ) ((t:ℂ) • D)).mul_right x
49   have he : exp ((t:ℂ) • D)*x=
50       ∑ k ∈ Finset.range (finrank ℂ R),((t:ℂ)^k/(k.factorial:ℂ)) • (D^k*x) := by
51     have hs' : HasSum (fun k : ℕ => ((t:ℂ)^k/(k.factorial:ℂ)) • (D^k*x))
52         (exp ((t:ℂ) • D)*x) := by
53       simpa only [smul_pow,Algebra.smul_mul_assoc,smul_smul,div_eq_mul_inv,mul_comm] using hs
54     exact hs'.unique (hasSum_sum_of_ne_finset_zero (fun k hk => by
55       rw [hkill k (by simpa using hk),smul_zero]))
56   have ht : t • A=algebraMap ℂ R (μ*t)+(t:ℂ) • D := by
57     simp only [D,smul_sub,Algebra.algebraMap_eq_smul_one,smul_smul]
58     rw [RCLike.real_smul_eq_coe_smul (K := ℂ),mul_comm μ (t:ℂ)]
59     abel
60   rw [transfer,ht,exp_add_of_commute (Algebra.commutes _ _),
61     ← algebraMap_exp_comm,← Complex.exp_eq_exp_ℂ,Algebra.algebraMap_eq_smul_one,
62     Algebra.smul_mul_assoc,one_mul,Algebra.smul_mul_assoc,he]
63 
64 theorem damped_mul_component (A : R) (z μ : ℂ) (x : R)
65     (hx : x ∈ (Module.End.maxGenEigenspace (LinearMap.mulLeft ℂ A)) μ) (t : ℝ) :
66     damped A z t*x=∑ k ∈ Finset.range (finrank ℂ R),
67       (Complex.exp ((μ-z)*t)*(t:ℂ)^k) • ((k.factorial:ℂ)⁻¹ • ((A-μ • 1)^k*x)) := by
68   rw [damped,Algebra.smul_mul_assoc,exp_mul_component A μ x hx,
69     smul_smul,Finset.smul_sum]
70   apply Finset.sum_congr rfl
71   intro k _
72   have he : -z*(t:ℂ)+μ*t=(μ-z)*t := by ring
73   simp only [smul_smul,div_eq_mul_inv]
74   rw [← Complex.exp_add,he,mul_assoc]
75 
76 theorem component_decay (A : R) (z : ℂ)
77     (hz : ∀ μ∈spectrum ℂ A,μ.re < z.re) (μ : ℂ) (x : R)
78     (hx : x ∈ (Module.End.maxGenEigenspace (LinearMap.mulLeft ℂ A)) μ) :
79     IntegrableOn (fun t => damped A z t*x) (Ioi 0) ∧
80     Tendsto (fun t => damped A z t*x) atTop (𝓝 0) := by
81   classical
82   by_cases hne : x=0
83   · subst x
84     simp
85   have hμ : (μ-z).re < 0 := by
86     have hh := hz μ (component_spectrum A μ x hx hne)
87     simp only [Complex.sub_re]
88     linarith
89   have he : (fun t => damped A z t*x)=(fun t : ℝ => ∑ k ∈ Finset.range (finrank ℂ R),
90       (Complex.exp ((μ-z)*t)*(t:ℂ)^k) • ((k.factorial:ℂ)⁻¹ • ((A-μ • 1)^k*x))) :=
91     funext (damped_mul_component A z μ x hx)
92   rw [he]
93   constructor
94   · exact integrable_finsetSum _ (fun k _ => (ScalarDecay.exp_pow_integrable _ hμ k).smul_const _)
95   · simpa using tendsto_finsetSum (Finset.range (finrank ℂ R))
96       (fun k _ => (ScalarDecay.exp_pow_tendsto_zero _ hμ k).smul_const
97         ((k.factorial:ℂ)⁻¹ • ((A-μ • 1)^k*x)))
98 
99 theorem spectral_decay (A : R) (z : ℂ) (hz : ∀ μ∈spectrum ℂ A,μ.re < z.re) :
100     IntegrableOn (damped A z) (Ioi 0) ∧ Tendsto (damped A z) atTop (𝓝 0) := by
101   have h (x : R) : IntegrableOn (fun t => damped A z t*x) (Ioi 0) ∧
102       Tendsto (fun t => damped A z t*x) atTop (𝓝 0) := by
103     apply Submodule.iSup_induction (Module.End.maxGenEigenspace (LinearMap.mulLeft ℂ A))
104       (x := x) (motive := fun x => IntegrableOn (fun t : ℝ => damped A z t*x) (Ioi 0) volume ∧
105         Tendsto (fun t => damped A z t*x) atTop (𝓝 0))
106       (by rw [Module.End.iSup_maxGenEigenspace_eq_top]; trivial)
107     · exact component_decay A z hz
108     · simp
109     · intro x y hx hy
110       simpa only [Pi.add_def,mul_add,add_zero] using And.intro (hx.1.add hy.1) (hx.2.add hy.2)
111   simpa using h 1
112 
113 
114 theorem spectral_laplace_inverse (A : R) (z : ℂ)
115     (hz : ∀ μ∈spectrum ℂ A,μ.re < z.re) :
116     IntegrableOn (damped A z) (Ioi 0) ∧ IsUnit (algebraMap ℂ R z-A) ∧
117       (∫ t in Ioi 0,damped A z t)=Ring.inverse (algebraMap ℂ R z-A) := by
118   have hs := spectral_decay A z hz
119   let B := A-algebraMap ℂ R z
120   have he : damped A z=transfer B := funext (damped_eq_shifted A z)
121   rw [he] at hs ⊢
122   have hl := integral_Ioi_of_hasDerivAt_of_tendsto'
123     (fun t (_ : t∈Ici (0:ℝ)) => transfer_derivative_left B t)
124     ((ContinuousLinearMap.mul ℝ R B).integrable_comp hs.1) hs.2
125   have hr := integral_Ioi_of_hasDerivAt_of_tendsto'
126     (fun t (_ : t∈Ici (0:ℝ)) => transfer_derivative_right B t)
127     (((ContinuousLinearMap.mul ℝ R).flip B).integrable_comp hs.1) hs.2
128   rw [integral_const_mul_of_integrable hs.1,transfer_zero,zero_sub] at hl
129   rw [integral_mul_const_of_integrable hs.1,transfer_zero,zero_sub] at hr
130   have hn : algebraMap ℂ R z-A= -B := by dsimp [B]; abel
131   have hl' : (algebraMap ℂ R z-A)*(∫ t in Ioi 0,transfer B t)=1 := by
132     rw [hn,neg_mul,hl,neg_neg]
133   have hr' : (∫ t in Ioi 0,transfer B t)*(algebraMap ℂ R z-A)=1 := by
134     rw [hn,mul_neg,hr,neg_neg]
135   have hu : IsUnit (algebraMap ℂ R z-A) := ⟨⟨_,_,hl',hr'⟩,rfl⟩
136   refine ⟨hs.1,hu,?_⟩
137   calc
138     _ = Ring.inverse (algebraMap ℂ R z-A)*((algebraMap ℂ R z-A)*(∫ t in Ioi 0,transfer B t)) :=
139       (Ring.inverse_mul_cancel_left _ _ hu).symm
140     _ = _ := by rw [hl',mul_one]
141 
142 theorem nonnormal_self_energy (A U V : R) (z : ℂ)
143     (hz : ∀ μ∈spectrum ℂ A,μ.re < z.re) :
144     IntegrableOn (fun t : ℝ => Complex.exp (-z*t) • (U*transfer A t*V)) (Ioi 0) ∧
145     (∫ t : ℝ in Ioi 0,Complex.exp (-z*t) • (U*transfer A t*V))=
146       U*Ring.inverse (algebraMap ℂ R z-A)*V := by
147   have h := spectral_laplace_inverse A z hz
148   have he : (fun t : ℝ => Complex.exp (-z*t) • (U*transfer A t*V))=
149       (fun t => U*damped A z t*V) := by
150     ext t
151     simp [damped,Algebra.mul_smul_comm,Algebra.smul_mul_assoc]
152   rw [he]
153   have hu : IntegrableOn (fun t => U*damped A z t) (Ioi 0) :=
154     (ContinuousLinearMap.mul ℝ R U).integrable_comp h.1
155   refine ⟨((ContinuousLinearMap.mul ℝ R).flip V).integrable_comp hu,?_⟩
156   rw [integral_mul_const_of_integrable hu,integral_const_mul_of_integrable h.1,h.2.2]
157 
158 end KomorebiPaperVI.NonnormalMemory

Back to source controls