Kadiri.kadiri_laplace_exp_hasDerivAt_of_full_strip

theorem kadiri_laplace_exp_hasDerivAt_of_full_strip {φ : ℝ → ℂ}    (hφ : ContDiff ℝ 1 φ) {b : ℝ} {s0 : ℂ}    (hs0lo : -b < s0.re) (hs0hi : s0.re < 1 + b)    (hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) :    HasDerivAt      (fun s : ℂ => ∫ y : ℝ, φ y * exp (s * (y : ℂ)) ∂volume)      (∫ y : ℝ, φ y * ((y : ℂ) * exp (s0 * (y : ℂ))) ∂volume) s0 := by  let lo : ℝ := (-b + s0.re) / 2  let hi : ℝ := (s0.re + (1 + b)) / 2  let ε : ℝ := min (s0.re - lo) (hi - s0.re) / 2  have hlo_lt_s0 : lo < s0.re := by    dsimp [lo]    linarith  have hs0_lt_hi : s0.re < hi := by    dsimp [hi]    linarith  have hεpos : 0 < ε := by    dsimp [ε]    exact half_pos (lt_min (sub_pos.mpr hlo_lt_s0) (sub_pos.mpr hs0_lt_hi))  have hlo_bound : -b < lo := by    dsimp [lo]    linarith  have hhi_bound : hi < 1 + b := by    dsimp [hi]    linarith  have hlohi : lo ≤ hi := by    linarith [hlo_lt_s0.le, hs0_lt_hi.le]  let F : ℂ → ℝ → ℂ := fun s y => φ y * exp (s * (y : ℂ))  let F' : ℂ → ℝ → ℂ := fun s y => φ y * ((y : ℂ) * exp (s * (y : ℂ)))  let bound : ℝ → ℝ := fun y =>    ‖(y : ℂ)‖ * ‖φ y‖ * (Real.exp (lo * y) + Real.exp (hi * y))  have hball_re_bounds :      ∀ s ∈ Metric.ball s0 ε, lo ≤ s.re ∧ s.re ≤ hi := by    intro s hs    have hre_diff : |s.re - s0.re| ≤ ‖s - s0‖ := by      simpa [sub_re] using Complex.abs_re_le_norm (s - s0)    have hnorm_lt : ‖s - s0‖ < ε := by      simpa [dist_eq_norm] using Metric.mem_ball.mp hs    have hε_le_left : ε ≤ s0.re - lo := by      dsimp [ε]      exact (half_le_self (by positivity)).trans (min_le_left _ _)    have hε_le_right : ε ≤ hi - s0.re := by      dsimp [ε]      exact (half_le_self (by positivity)).trans (min_le_right _ _)    have hdiff_le : |s.re - s0.re| ≤ ε := le_trans hre_diff (le_of_lt hnorm_lt)    constructor    · have hleft := (abs_le.mp hdiff_le).1      linarith    · have hright := (abs_le.mp hdiff_le).2      linarith  have hF_meas : ∀ᶠ s in 𝓝 s0, AEStronglyMeasurable (F s) volume := by    exact Eventually.of_forall fun s => by      dsimp [F]      exact (hφ.continuous.mul (continuous_exp.comp (by fun_prop))).aestronglyMeasurable  have hF_int : Integrable (F s0) volume := by    have hbase : Integrable (fun y : ℝ => exp (((s0.re : ℝ) : ℂ) * (y : ℂ)) * φ y) :=      kadiri_laplace_full_strip_weight_integrable_of_continuous        (ψ := φ) hφ.continuous hs0lo hs0hi hφ_decay    refine hbase.congr' ?_ ?_    · dsimp [F]      exact (hφ.continuous.mul (continuous_exp.comp (by fun_prop))).aestronglyMeasurable    · filter_upwards with y      dsimp [F]      rw [norm_mul, norm_mul, Complex.norm_exp, Complex.norm_exp]      have h1 : (s0 * (y : ℂ)).re = s0.re * y := by norm_num [Complex.mul_re]      have h2 : ((((s0.re : ℝ) : ℂ) * (y : ℂ)) : ℂ).re = s0.re * y := by norm_num      rw [h1, h2]      ring  have hF'_meas : AEStronglyMeasurable (F' s0) volume := by    dsimp [F']    exact (hφ.continuous.mul ((continuous_ofReal.mul (continuous_exp.comp (by fun_prop))))).aestronglyMeasurable  have h_bound : ∀ᵐ y ∂volume, ∀ s ∈ Metric.ball s0 ε, ‖F' s y‖ ≤ bound y := by    filter_upwards with y s hs    obtain ⟨hslo, hshi⟩ := hball_re_bounds s hs    dsimp [F', bound]    rw [norm_mul, norm_mul, Complex.norm_exp]    have hre : (s * (y : ℂ)).re = s.re * y := by norm_num [Complex.mul_re]    rw [hre]    have hexp_le : Real.exp (s.re * y) ≤ Real.exp (lo * y) + Real.exp (hi * y) := by      by_cases hy : 0 ≤ y      · have hmul : s.re * y ≤ hi * y := mul_le_mul_of_nonneg_right hshi hy        exact (Real.exp_le_exp.mpr hmul).trans          (le_add_of_nonneg_left (Real.exp_nonneg _))      · have hy' : y ≤ 0 := le_of_not_ge hy        have hmul : s.re * y ≤ lo * y := mul_le_mul_of_nonpos_right hslo hy'        exact (Real.exp_le_exp.mpr hmul).trans          (le_add_of_nonneg_right (Real.exp_nonneg _))    calc      ‖φ y‖ * (‖(y : ℂ)‖ * Real.exp (s.re * y))          ≤ ‖φ y‖ * (‖(y : ℂ)‖ *              (Real.exp (lo * y) + Real.exp (hi * y))) := by            gcongr      _ = ‖(y : ℂ)‖ * ‖φ y‖ *          (Real.exp (lo * y) + Real.exp (hi * y)) := by ring  have hbound_int : Integrable bound volume :=    kadiri_laplace_full_strip_exp_interval_moment_integrable_of_continuous      hφ.continuous hlo_bound hhi_bound hlohi hφ_decay  have h_diff : ∀ᵐ y ∂volume, ∀ s ∈ Metric.ball s0 ε,      HasDerivAt (fun w : ℂ => F w y) (F' s y) s := by    filter_upwards with y s _hs    dsimp [F, F']    simpa [mul_assoc, mul_comm, mul_left_comm] using      (((hasDerivAt_id s).mul_const (y : ℂ)).cexp.const_mul (φ y))  have hderiv :=    (hasDerivAt_integral_of_dominated_loc_of_deriv_le      (F := F) (F' := F') (x₀ := s0) (s := Metric.ball s0 ε)      (bound := bound) (μ := volume) (Metric.ball_mem_nhds s0 hεpos)      hF_meas hF_int hF'_meas h_bound hbound_int h_diff).2  simpa [F, F'] using hderiv