MemoryLaplace.lean

1 import KomorebiPaperVI.Semigroups
2 import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
3 import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
4 
5 /-! Author: Komorebi P. Laplace inversion from an explicit exponential-growth bound.
6 The spectral-abscissa-to-growth bridge for arbitrary finite matrices is not assumed proved. -/
7 namespace KomorebiPaperVI.MemoryLaplace
8 open Set Filter MeasureTheory
9 open scoped Topology
10 open KomorebiPaperVI.Semigroups
11 variable {R : Type*} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R]
12 
13 theorem decay_integrable (B : R) (M d : ℝ) (hd : 0 < d)
14     (hB : ∀ t,0 ≤ t → ‖transfer B t‖ ≤ M*Real.exp (-d*t)) :
15     IntegrableOn (transfer B) (Ioi 0) := by
16   apply ((integrableOn_exp_mul_Ioi (a := -d) (by linarith) 0).const_mul M).mono'
17     (transfer_continuous B).aestronglyMeasurable
18   filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
19   exact hB t ht.le
20 
21 omit [CompleteSpace R] in
22 theorem decay_tendsto_zero (B : R) (M d : ℝ) (hd : 0 < d)
23     (hB : ∀ t,0 ≤ t → ‖transfer B t‖ ≤ M*Real.exp (-d*t)) :
24     Tendsto (transfer B) atTop (𝓝 0) := by
25   apply tendsto_zero_iff_norm_tendsto_zero.mpr
26   have ht : Tendsto (fun t : ℝ => M*Real.exp (-d*t)) atTop (𝓝 0) := by
27     simpa using (Real.tendsto_exp_atBot.comp
28       (tendsto_id.const_mul_atTop_of_neg (by linarith : -d < 0))).const_mul M
29   apply squeeze_zero' (Eventually.of_forall (fun t => norm_nonneg (transfer B t))) ?_ ht
30   filter_upwards [eventually_ge_atTop (0:ℝ)] with t ht
31   exact hB t ht
32 
33 theorem integral_generator_transfer (B : R) (M d : ℝ) (hd : 0 < d)
34     (hB : ∀ t,0 ≤ t → ‖transfer B t‖ ≤ M*Real.exp (-d*t)) :
35     B*(∫ t in Ioi 0,transfer B t)=-1 := by
36   have hi := decay_integrable B M d hd hB
37   have hprod : IntegrableOn (fun t => B*transfer B t) (Ioi 0) :=
38     (ContinuousLinearMap.mul ℝ R B).integrable_comp hi
39   have hf := integral_Ioi_of_hasDerivAt_of_tendsto'
40     (fun t (_ : t∈Ici (0:ℝ)) => transfer_derivative_left B t)
41     hprod (decay_tendsto_zero B M d hd hB)
42   rw [integral_const_mul_of_integrable hi,transfer_zero,zero_sub] at hf
43   exact hf
44 
45 theorem shifted_laplace_right_inverse (A : R) (z M d : ℝ) (hd : 0 < d)
46     (hB : ∀ t,0 ≤ t → ‖transfer (A-z • 1) t‖ ≤ M*Real.exp (-d*t)) :
47     (z • 1-A)*(∫ t in Ioi 0,transfer (A-z • 1) t)=1 := by
48   have h := integral_generator_transfer (A-z • 1) M d hd hB
49   rw [show z • (1:R)-A=-(A-z • 1) by abel,neg_mul,h,neg_neg]
50 
51 theorem memory_integral (B U V : R) (M d : ℝ) (hd : 0 < d)
52     (hB : ∀ t,0 ≤ t → ‖transfer B t‖ ≤ M*Real.exp (-d*t)) :
53     (∫ t in Ioi 0,U*transfer B t*V)=U*(∫ t in Ioi 0,transfer B t)*V := by
54   have hi := decay_integrable B M d hd hB
55   have hu : IntegrableOn (fun t => U*transfer B t) (Ioi 0) :=
56     (ContinuousLinearMap.mul ℝ R U).integrable_comp hi
57   rw [integral_mul_const_of_integrable hu,integral_const_mul_of_integrable hi]
58 
59 end KomorebiPaperVI.MemoryLaplace

Back to source controls