ScalarDecay.lean

1 import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
2 import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
3 import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
4 
5 /-! Author: Komorebi P. Complex exponential-polynomial decay and actual integrability. -/
6 namespace KomorebiPaperVI.ScalarDecay
7 open Set Filter MeasureTheory
8 open scoped Topology
9 set_option backward.isDefEq.respectTransparency false
10 
11 theorem norm_exp_pow (a : ℂ) (k : ℕ) (t : ℝ) (ht : 0 ≤ t) :
12     ‖Complex.exp (a*t)*(t:ℂ)^k‖=t^k*Real.exp (a.re*t) := by
13   simp [Complex.norm_exp,Complex.mul_re,Complex.norm_real,Real.norm_eq_abs,
14     abs_of_nonneg ht,mul_comm]
15 
16 theorem exp_pow_integrable (a : ℂ) (ha : a.re < 0) (k : ℕ) :
17     IntegrableOn (fun t : ℝ => Complex.exp (a*t)*(t:ℂ)^k) (Ioi 0) := by
18   have hi := integrableOn_rpow_mul_exp_neg_mul_rpow
19     (s := (k:ℝ)) (p := (1:ℝ)) (b := -a.re) (by linarith [Nat.cast_nonneg (α := ℝ) k]) zero_lt_one (by linarith)
20   simp only [Real.rpow_natCast,Real.rpow_one,neg_neg] at hi
21   apply hi.mono' (by fun_prop)
22   filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
23   rw [norm_exp_pow a k t ht.le]
24 
25 theorem exp_pow_tendsto_zero (a : ℂ) (ha : a.re < 0) (k : ℕ) :
26     Tendsto (fun t : ℝ => Complex.exp (a*t)*(t:ℂ)^k) atTop (𝓝 0) := by
27   apply tendsto_zero_iff_norm_tendsto_zero.mpr
28   have hh := tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (k:ℝ) (-a.re) (by linarith)
29   simp only [Real.rpow_natCast,neg_neg] at hh
30   apply hh.congr'
31   filter_upwards [eventually_ge_atTop (0:ℝ)] with t ht
32   exact (norm_exp_pow a k t ht).symm
33 
34 end KomorebiPaperVI.ScalarDecay

Back to source controls