Kadiri.kadiriTestFn_decay

@[blueprint  "kadiri-test-fn-decay"  (title := "Decay condition (B) for the Kadiri test function")  (statement := /-- For $f$ satisfying $(H_1)$ of \ref{kadiri-prop-2-1} and  $s \in \mathbb{C}$ with $\Re s > 1$, the Kadiri test function  $\varphi$ satisfies  decay condition (B) of \ref{kadiri-thm-3-1-q1}: there exists $b > 0$  (any $0 < b < \Re s - 1$ works) such that both $\varphi(x;\, s) e^{x/2}$ and  $\varphi'(x;\, s) e^{x/2}$ are $O(e^{-(1/2 + b)|x|})$ as $|x| \to \infty$. -/)  (proof := /-- For $x < 0$ both $\varphi(x;\, s)$ and $\varphi'(x;\, s)$ are identically  $0$, so the bound holds trivially at $-\infty$. For $x > d$ (above the support of $f$),  $\varphi(x;\, s) = f(0)\, e^{-x s}$ and $\varphi'(x;\, s) = -s\, f(0)\, e^{-x s}$, so  $|\varphi(x;\, s) e^{x/2}| = |f(0)|\, e^{-x(\Re s - 1/2)}$ and similarly for the  derivative with an extra factor $|s|$; both are $O(e^{-(1/2 + b) x})$ as $x \to +\infty$  precisely when $\Re s - 1/2 \geq 1/2 + b$, i.e.\ $b \leq \Re s - 1$. Take any  $0 < b < \Re s - 1$. To be formalised. -/)  (latexEnv := "lemma")  (discussion := 1485)]theorem kadiriTestFn_decay {d : ℝ} {f : ℝ → ℝ} (hf_supp : tsupport f ⊆ .Ico 0 d)    {s : ℂ} (hs : 1 < s.re) :    ∃ b > 0,      ((fun x : ℝ ↦ kadiriTestFn f s x * exp ((x : ℂ) / 2))          =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) ∧      ((fun x : ℝ ↦ deriv (kadiriTestFn f s) x * exp ((x : ℂ) / 2))          =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) := by  have hb : (0 : ℝ) < (s.re - 1) / 2 := by linarith  have hre : ∀ x : ℝ, (-s * (x : ℂ)).re = -(s.re * x) := fun x => by    simp [Complex.mul_re]  have hre2 : ∀ x : ℝ, ((x : ℂ) / 2).re = x / 2 := fun x => by    have : (x : ℂ) / 2 = ((x / 2 : ℝ) : ℂ) := by push_cast; ring    rw [this, Complex.ofReal_re]  have hexp : ∀ x : ℝ, max d 0 < x →      -(s.re * x) + x / 2 ≤ -(1 / 2 + (s.re - 1) / 2) * |x| := by    intro x hx    have hx0 : (0 : ℝ) < x := (le_max_right d 0).trans_lt hx    rw [abs_of_pos hx0]    nlinarith [mul_nonneg hx0.le (sub_nonneg.2 hs.le)]  refine ⟨(s.re - 1) / 2, hb, ?_, ?_⟩  · rw [cocompact_eq_atBot_atTop, Asymptotics.isBigO_sup]    constructor    · have h0 : (fun x : ℝ ↦ kadiriTestFn f s x * exp ((x : ℂ) / 2))          =ᶠ[Filter.atBot] fun _ => (0 : ℂ) := by        filter_upwards [Filter.eventually_lt_atBot (0 : ℝ)] with x hx        simp [kadiriTestFn, not_le_of_gt hx]      exact h0.trans_isBigO (Asymptotics.isBigO_zero _ _)    · rw [Asymptotics.isBigO_iff]      refine ⟨‖(f 0 : ℂ)‖, ?_⟩      filter_upwards [Filter.eventually_gt_atTop (max d 0)] with x hx      have hx0 : (0 : ℝ) < x := (le_max_right d 0).trans_lt hx      have hfx : f x = 0 :=        eq_zero_of_tsupport_subset_Ico_right hf_supp ((le_max_left d 0).trans_lt hx).le      have hval : kadiriTestFn f s x = (f 0 : ℂ) * exp (-s * (x : ℂ)) := by        simp [kadiriTestFn, hx0.le, hfx]      rw [hval, mul_assoc, ← Complex.exp_add, norm_mul, Complex.norm_exp,        Real.norm_eq_abs, Real.abs_exp, Complex.add_re, hre, hre2]      exact mul_le_mul_of_nonneg_left (Real.exp_le_exp.2 (hexp x hx)) (norm_nonneg _)  · rw [cocompact_eq_atBot_atTop, Asymptotics.isBigO_sup]    constructor    · have h0 : (fun x : ℝ ↦ deriv (kadiriTestFn f s) x * exp ((x : ℂ) / 2))          =ᶠ[Filter.atBot] fun _ => (0 : ℂ) := by        filter_upwards [Filter.eventually_lt_atBot (0 : ℝ)] with x hx        simp [kadiriTestFn_H1_deriv_of_lt_zero s hx]      exact h0.trans_isBigO (Asymptotics.isBigO_zero _ _)    · rw [Asymptotics.isBigO_iff]      refine ⟨‖(f 0 : ℂ)‖ * ‖s‖, ?_⟩      filter_upwards [Filter.eventually_gt_atTop (max d 0)] with x hx      rw [kadiriTestFn_deriv_of_gt_max hf_supp s hx]      have hnorm : ‖(f 0 : ℂ) * (-s * exp (-s * (x : ℂ))) * exp ((x : ℂ) / 2)‖ =          ‖(f 0 : ℂ)‖ * ‖s‖ * Real.exp (-(s.re * x) + x / 2) := by        rw [mul_assoc, mul_assoc, ← Complex.exp_add, norm_mul, norm_mul, norm_neg,          Complex.norm_exp, Complex.add_re, hre, hre2]        ring      rw [hnorm, Real.norm_eq_abs, Real.abs_exp]      exact mul_le_mul_of_nonneg_left (Real.exp_le_exp.2 (hexp x hx)) (by positivity)