Phi_differentiableAt

theorem Phi_differentiableAt {φ : ℝ → ℂ} {b : ℝ} (hφc : Continuous φ)    (hφ_decay : (fun x : ℝ ↦ φ x * Complex.exp ((x:ℂ)/2)) =O[cocompact ℝ]      fun x ↦ Real.exp (-(1/2+b)*|x|))    {x₀ : ℂ} (h_top : -(1+b) < x₀.re) (h_bot : x₀.re < b) :    DifferentiableAt ℂ (fun s ↦ ∫ y, φ y * Complex.exp (-s*(y:ℂ))) x₀ := by  set σ₀ := x₀.re with hσ₀  set m : ℝ := min (b - σ₀) (σ₀ + 1 + b) with hm_def  have hm : 0 < m := lt_min (by linarith) (by linarith)  set ε : ℝ := m/4 with hε_def  have hε : 0 < ε := by positivity  have hmle1 : m ≤ b - σ₀ := min_le_left _ _  have hmle2 : m ≤ σ₀ + 1 + b := min_le_right _ _  have hlo_top : -(1+b) < σ₀ - ε := by simp only [hε_def, hm_def]; linarith  have hlo_bot : σ₀ - ε < b := by linarith  have hhi_top : -(1+b) < σ₀ + ε := by linarith  have hhi_bot : σ₀ + ε < b := by simp only [hε_def, hm_def]; linarith  set bound : ℝ → ℝ := fun y ↦ ‖(-(y:ℂ)*φ y) * Complex.exp (-((σ₀-ε:ℝ):ℂ)*y)‖      + ‖(-(y:ℂ)*φ y) * Complex.exp (-((σ₀+ε:ℝ):ℂ)*y)‖ with hbound_def  have hbound_int : Integrable bound :=    (laplace_deriv_integrand_integrable hφc hφ_decay hlo_top hlo_bot).norm.add      (laplace_deriv_integrand_integrable hφc hφ_decay hhi_top hhi_bot).norm  have hnorm : ∀ (σ' : ℝ) (y : ℝ), ‖(-(y:ℂ)*φ y) * Complex.exp (-(σ':ℂ)*y)‖      = ‖(-(y:ℂ)*φ y)‖ * Real.exp (-(σ'*y)) := by    intro σ' y; rw [norm_mul, Complex.norm_exp]; congr 2; simp [Complex.mul_re]  have hF_int : Integrable (fun y : ℝ ↦ φ y * Complex.exp (-x₀*(y:ℂ))) := by    rw [← integrable_norm_iff (by fun_prop)]    refine (laplace_integrand_integrable hφc hφ_decay h_top h_bot |>.norm).congr      (Filter.Eventually.of_forall (fun y ↦ ?_))    simp only [norm_mul, Complex.norm_exp]    congr 2    simp [Complex.mul_re, hσ₀]  have key := hasDerivAt_integral_of_dominated_loc_of_deriv_le (μ := volume)    (bound := bound) (F := fun s y ↦ φ y * Complex.exp (-s*(y:ℂ)))    (F' := fun s y ↦ -(y:ℂ) * φ y * Complex.exp (-s*(y:ℂ)))    (s := Metric.ball x₀ ε) (x₀ := x₀)    (Metric.ball_mem_nhds x₀ hε)    (Filter.Eventually.of_forall (fun s ↦ by fun_prop)) hF_int (by fun_prop)    ?_ hbound_int ?_  · exact (key.2).differentiableAt  · refine Filter.Eventually.of_forall (fun y s hs ↦ ?_)    have hsre : σ₀ - ε < s.re ∧ s.re < σ₀ + ε := by      have h2 : ‖s - x₀‖ < ε := by rw [← dist_eq_norm]; exact Metric.mem_ball.mp hs      have h1 : |s.re - x₀.re| ≤ ‖s - x₀‖ := by rw [← Complex.sub_re]; exact Complex.abs_re_le_norm _      rw [← hσ₀] at h1      have hd : |s.re - σ₀| < ε := lt_of_le_of_lt h1 h2      rw [abs_lt] at hd; exact ⟨by linarith [hd.1], by linarith [hd.2]⟩    have hgoalL : ‖-(y:ℂ) * φ y * Complex.exp (-s*(y:ℂ))‖        = ‖(-(y:ℂ)*φ y)‖ * Real.exp (-(s.re*y)) := by      rw [show -(y:ℂ) * φ y * Complex.exp (-s*(y:ℂ)) = (-(y:ℂ)*φ y) * Complex.exp (-s*(y:ℂ)) by ring,        norm_mul, Complex.norm_exp]; congr 2; simp [Complex.mul_re]    rw [hgoalL]; simp only [hbound_def]; rw [hnorm, hnorm]    have hN : (0:ℝ) ≤ ‖(-(y:ℂ)*φ y)‖ := norm_nonneg _    have hexp_le : Real.exp (-(s.re*y)) ≤ Real.exp (-((σ₀-ε)*y)) + Real.exp (-((σ₀+ε)*y)) := by      rcases le_total 0 y with hy | hy      · have : Real.exp (-(s.re*y)) ≤ Real.exp (-((σ₀-ε)*y)) :=          Real.exp_le_exp.mpr (by nlinarith [hsre.1, hy])        linarith [Real.exp_pos (-((σ₀+ε)*y))]      · have : Real.exp (-(s.re*y)) ≤ Real.exp (-((σ₀+ε)*y)) :=          Real.exp_le_exp.mpr (by nlinarith [hsre.2, hy])        linarith [Real.exp_pos (-((σ₀-ε)*y))]    calc ‖(-(y:ℂ)*φ y)‖ * Real.exp (-(s.re*y))        ≤ ‖(-(y:ℂ)*φ y)‖ * (Real.exp (-((σ₀-ε)*y)) + Real.exp (-((σ₀+ε)*y))) :=          mul_le_mul_of_nonneg_left hexp_le hN      _ = _ := by ring  · refine Filter.Eventually.of_forall (fun y s _ ↦ ?_)    have h1 : HasDerivAt (fun s : ℂ ↦ -s * (y:ℂ)) (-1 * (y:ℂ)) s :=      ((hasDerivAt_id s).neg).mul_const (y:ℂ)    have h2 := (h1.cexp).const_mul (φ y)    convert! h2 using 1; ring