Kadiri.laplaceTransform_sub_pole_norm_decay

theorem laplaceTransform_sub_pole_norm_decay {d : ℝ} (hd : 0 < d) {f : ℝ → ℝ}    (hf_C2 : ContDiffOn ℝ 2 f (.Icc 0 d))    (hf_supp : tsupport f ⊆ .Ico 0 d)    (hf_d : f d = 0)    (hf_deriv_0 : derivWithin f (Set.Icc 0 d) 0 = 0)    (hf_deriv_d : derivWithin f (Set.Icc 0 d) d = 0)    (σ₀ : ℝ) :    ∃ C : ℝ, ∀ s : ℂ, σ₀ ≤ s.re → s.im ≠ 0 →      ‖(f 0 : ℂ) / s - laplaceTransform f s‖ ≤ C / s.im ^ 2 := by  have hdf_C1 : ContDiffOn ℝ 1 (fun y => derivWithin f (Set.Icc 0 d) y) (Set.Icc 0 d) :=    hf_C2.derivWithin (uniqueDiffOn_Icc hd) (by norm_num)  have hg_cont : ContinuousOn      (fun x => derivWithin (fun y => derivWithin f (Set.Icc 0 d) y) (Set.Icc 0 d) x)      (Set.Icc 0 d) :=    hdf_C1.continuousOn_derivWithin (uniqueDiffOn_Icc hd) le_rfl  obtain ⟨K0, hK0⟩ := isCompact_Icc.exists_bound_of_continuousOn hg_cont  have hK00 : 0 ≤ K0 := (norm_nonneg _).trans (hK0 0 (Set.left_mem_Icc.2 hd.le))  set B : ℝ := max 0 (-σ₀) with hB  set M : ℝ := Real.exp (B * d) * K0 * d with hMdef  have hM0 : 0 ≤ M := mul_nonneg (mul_nonneg (Real.exp_pos _).le hK00) hd.le  have hMbound : ∀ s : ℂ, σ₀ ≤ s.re →      ‖laplaceTransform (fun u => deriv (deriv f) u) s‖ ≤ M := by    intro s hs0    rw [laplaceTransform_deriv_deriv_eq_interval_of_tsupport_subset_Ico hd hf_supp s]    have hpt : ∀ t ∈ Set.uIoc (0 : ℝ) d,        ‖exp (-s * (t : ℂ)) * ((deriv (deriv f) t : ℝ) : ℂ)‖ ≤ Real.exp (B * d) * K0 := by      intro t ht      rw [Set.uIoc_of_le hd.le] at ht      rw [norm_mul, Complex.norm_exp]      have hre : (-s * (t : ℂ)).re = -(s.re * t) := by simp [Complex.mul_re]      have hexp_le : Real.exp ((-s * (t : ℂ)).re) ≤ Real.exp (B * d) := by        rw [hre]        apply Real.exp_le_exp.2        have hBge : -s.re ≤ B := le_trans (neg_le_neg hs0) (le_max_right 0 (-σ₀))        have hB0 : (0 : ℝ) ≤ B := le_max_left 0 (-σ₀)        calc -(s.re * t) = -s.re * t := (neg_mul _ _).symm          _ ≤ B * t := mul_le_mul_of_nonneg_right hBge ht.1.le          _ ≤ B * d := mul_le_mul_of_nonneg_left ht.2 hB0      have hfpp : ‖((deriv (deriv f) t : ℝ) : ℂ)‖ ≤ K0 := by        rw [Complex.norm_real]        by_cases htd : t = d        · rw [htd, deriv_deriv_eq_zero_of_tsupport_subset_Ico hf_supp le_rfl]          simpa using hK00        · have htlt : t < d := lt_of_le_of_ne ht.2 htd          rw [deriv_deriv_eq_derivWithin_derivWithin_of_mem_Ioo ⟨ht.1, htlt⟩]          simpa using hK0 t ⟨ht.1.le, ht.2⟩      exact mul_le_mul hexp_le hfpp (norm_nonneg _) (Real.exp_pos _).le    refine le_trans (intervalIntegral.norm_integral_le_of_norm_le_const hpt) ?_    rw [sub_zero, abs_of_pos hd]  refine ⟨M, ?_⟩  intro s hs0 him0  have hs : s ≠ 0 := fun h => him0 (by rw [h]; rfl)  have him2 : (0 : ℝ) < s.im ^ 2 := by positivity  have hns : s.im ^ 2 ≤ Complex.normSq s := by    rw [Complex.normSq_apply]    nlinarith [mul_self_nonneg s.re]  rw [laplaceTransform_ibp hd hf_C2 hf_supp hf_d hf_deriv_0 hf_deriv_d hs]  have hcancel : (f 0 : ℂ) / s -      ((f 0 : ℂ) / s + laplaceTransform (fun u => deriv (deriv f) u) s / s ^ 2) =      -(laplaceTransform (fun u => deriv (deriv f) u) s / s ^ 2) := by    ring  rw [hcancel, norm_neg, norm_div, norm_pow]  have hsq : s.im ^ 2 ≤ ‖s‖ ^ 2 := by    rw [← Complex.normSq_eq_norm_sq]    exact hns  have hnorm2 : (0 : ℝ) < ‖s‖ ^ 2 := by positivity  calc ‖laplaceTransform (fun u => deriv (deriv f) u) s‖ / ‖s‖ ^ 2      ≤ M / ‖s‖ ^ 2 := by        gcongr        exact hMbound s hs0    _ ≤ M / s.im ^ 2 := by gcongr