MatrixMemory.lean

1 import KomorebiPaperVI.NonnormalMemory
2 import Mathlib.Analysis.CStarAlgebra.Matrix
3 
4 /-! Author: Komorebi P. The literal rectangular matrix memory/self-energy identity. -/
5 namespace KomorebiPaperVI.MatrixMemory
6 open Set MeasureTheory
7 open KomorebiPaperVI.Semigroups KomorebiPaperVI.ComplexMemory
8 open scoped Matrix.Norms.L2Operator
9 set_option backward.isDefEq.respectTransparency false
10 variable {I J : Type*} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
11 
12 noncomputable def sandwich (U : Matrix I J ℂ) (V : Matrix J I ℂ) :
13     Matrix J J ℂ →L[ℂ] Matrix I I ℂ :=
14   ( { toFun := fun B => U*B*V
15       map_add' := fun A B => by simp [Matrix.mul_add,Matrix.add_mul]
16       map_smul' := fun c A => by simp [Matrix.mul_smul,Matrix.smul_mul] } :
17     Matrix J J ℂ →ₗ[ℂ] Matrix I I ℂ).toContinuousLinearMap
18 
19 theorem rectangular_memory_self_energy (A : Matrix J J ℂ)
20     (U : Matrix I J ℂ) (V : Matrix J I ℂ) (z : ℂ)
21     (hz : ∀ μ∈spectrum ℂ A,μ.re < z.re) :
22     IntegrableOn (fun t : ℝ => Complex.exp (-z*t) • (U*transfer A t*V)) (Ioi 0) ∧
23     (∫ t : ℝ in Ioi 0,Complex.exp (-z*t) • (U*transfer A t*V))=
24       U*(Matrix.scalar J z-A)⁻¹*V := by
25   have h := NonnormalMemory.spectral_laplace_inverse A z hz
26   have he : (fun t : ℝ => Complex.exp (-z*t) • (U*transfer A t*V))=
27       (fun t => sandwich U V (damped A z t)) := by
28     ext t i j
29     simp [sandwich,damped]
30   rw [he]
31   refine ⟨(sandwich U V).integrable_comp h.1,?_⟩
32   rw [(sandwich U V).integral_comp_comm h.1,h.2.2]
33   change U*Ring.inverse (algebraMap ℂ (Matrix J J ℂ) z-A)*V=_
34   rw [Matrix.nonsing_inv_eq_ringInverse]
35   rfl
36 
37 end KomorebiPaperVI.MatrixMemory

Back to source controls