CH2.integrable_phi_fourier_ray

theorem integrable_phi_fourier_ray (ν ε σ x : ℝ) (hν : ν > 0) (hsigma : σ ∈ Set.Icc (-1 : ℝ) 1) (hx : x < 0)    (f : ℂ → ℂ)    (hf_formula : f = (fun z ↦ (Phi_circ ν ε z + Phi_star ν ε z) * E (-z * x)) ∨                  f = (fun z ↦ (Phi_circ ν ε z - Phi_star ν ε z) * E (-z * x))) :    IntegrableOn (fun (y : ℝ) ↦ f (σ + y * I)) (Set.Ici (0 : ℝ)) := by  have h_cont : ContinuousOn (fun (y : ℝ) ↦ f (σ + y * I)) (Set.Ici (0 : ℝ)) := fun y hy ↦ by    let z := ↑σ + ↑y * I    have hy_im : 0 ≤ z.im := by dsimp [z]; simpa using hy    have h_anal_at_z : AnalyticAt ℂ f z := by      have hE : AnalyticAt ℂ (fun z : ℂ ↦ E (-z * x)) z := by        simpa [E] using! analyticAt_cexp.comp          (by fun_prop : AnalyticAt ℂ (fun z : ℂ ↦ 2 * π * I * (-z * x)) z)      rcases hf_formula with h_eq | h_eq <;> rw [h_eq]      · exact ((Phi_circ.analyticAt_of_im_nonneg ν ε z hν hy_im).add (Phi_star.analyticAt_of_im_nonneg ν ε z hν hy_im)).mul hE      · exact ((Phi_circ.analyticAt_of_im_nonneg ν ε z hν hy_im).sub (Phi_star.analyticAt_of_im_nonneg ν ε z hν hy_im)).mul hE    have h_ray : ContinuousAt (fun (y' : ℝ) => ↑σ + ↑y' * I) y :=      continuousAt_const.add (Complex.continuous_ofReal.continuousAt.mul continuousAt_const)    exact ContinuousAt.comp_of_eq h_anal_at_z.continuousAt h_ray rfl |>.continuousWithinAt  obtain ⟨C, hC⟩ : ∃ C, ∀ y : ℝ, y ≥ 1 → ‖f (σ + y * I)‖ ≤ C * (y + 1) * rexp (2 * π * x * y) := by    apply phi_fourier_ray_bound ν ε σ x hν hsigma    intro z    rcases hf_formula with rfl | rfl <;> simp only [norm_mul]    · exact mul_le_mul_of_nonneg_right (norm_add_le _ _) (norm_nonneg _)    · exact mul_le_mul_of_nonneg_right (norm_sub_le _ _) (norm_nonneg _)  let g (y : ℝ) := if y < 1 then (if y < 0 then 0 else ‖f (σ + y * I)‖) else C * (y + 1) * rexp (2 * π * x * y)  have h_int_decay : IntegrableOn (fun y ↦ (y + 1) * rexp (2 * π * x * y)) (Set.Ici 1) := by    have htlam : 2 * π * x < 0 := by nlinarith [hx, Real.pi_pos]    have h1 : IntegrableOn (fun (y : ℝ) ↦ rexp (2 * π * x * y)) (Set.Ici 1) := by      rw [integrableOn_Ici_iff_integrableOn_Ioi]      exact integrableOn_exp_mul_Ioi htlam 1    have h2 : IntegrableOn (fun y ↦ y * rexp (2 * π * x * y)) (Set.Ici 1) := by      have hb : 0 < -(2 * π * x) := by nlinarith [hx, Real.pi_pos]      have h_int := integrableOn_rpow_mul_exp_neg_mul_rpow (s := 1) (p := 1) (by norm_num) (by norm_num) hb      refine IntegrableOn.congr_fun (f := fun (y : ℝ) ↦ y ^ (1 : ℝ) * rexp (- -(2 * π * x) * y ^ (1 : ℝ))) ?_ ?_ measurableSet_Ici      · apply h_int.mono_set        intro y hy; exact Set.mem_Ioi.mpr (by linarith [Set.mem_Ici.mp hy])      · intro y _; dsimp; simp only [Real.rpow_one, neg_neg]    simpa [add_mul] using! h2.add h1  have hg : IntegrableOn g (Set.Ici 0) := by    rw [show Set.Ici (0 : ℝ) = Set.Ico 0 1 ∪ Set.Ici 1 from      (Set.Ico_union_Ici_eq_Ici zero_le_one).symm]    refine IntegrableOn.union ?_ ?_    · have h_int_Icc : IntegrableOn (fun y : ℝ ↦ ‖f (↑σ + ↑y * I)‖) (Set.Icc 0 1) := by        apply ContinuousOn.integrableOn_compact isCompact_Icc        exact h_cont.norm.mono Set.Icc_subset_Ici_self      exact IntegrableOn.congr_fun (h_int_Icc.mono_set Set.Ico_subset_Icc_self)        (fun y hy ↦ by simp [g, hy.2, not_lt.mpr hy.1]) measurableSet_Ico    · exact IntegrableOn.congr_fun (h_int_decay.const_mul C)        (fun y hy ↦ by simp [g, not_lt.mpr (Set.mem_Ici.mp hy)]; ring)        measurableSet_Ici  refine hg.mono' (h_cont.aestronglyMeasurable measurableSet_Ici) <| (ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ (fun y hy ↦ ?_)  by_cases h : y < 1  · simp [g, h, not_lt.mpr (Set.mem_Ici.mp hy)]  · simpa [g, h] using hC y (not_lt.mp h)