second_fourier_integrable_aux1

lemma second_fourier_integrable_aux1 (hcont : Measurable ψ) (hsupp : Integrable ψ) (hσ : 1 < σ') :    let ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-Real.log x))).prod volume    Integrable (Function.uncurry fun (u : ℝ) (a : ℝ) ↦ ((rexp (-u * (σ' - 1))) : ℂ) •    (𝐞 (Multiplicative.ofAdd (-(a * (u / (2 * π))))) : ℂ) • ψ a) ν := by  intro ν  constructor  · apply Measurable.aestronglyMeasurable    -- TODO: find out why fun_prop does not play well with Multiplicative.ofAdd    simp only [neg_mul, ofReal_exp, ofReal_neg, ofReal_mul, ofReal_sub, ofReal_one,      Multiplicative.ofAdd, Equiv.coe_fn_mk, smul_eq_mul]    fun_prop  · let f1 : ℝ → ENNReal := fun a1 ↦ ‖cexp (-(↑a1 * (↑σ' - 1)))‖ₑ    let f2 : ℝ → ENNReal := fun a2 ↦ ‖ψ a2‖ₑ    suffices ∫⁻ (a : ℝ × ℝ), f1 a.1 * f2 a.2 ∂ν < ⊤ by      simpa [hasFiniteIntegral_iff_enorm, enorm_eq_nnnorm, Function.uncurry]    refine (lintegral_prod_mul ?_ ?_).trans_lt ?_ <;> try fun_prop    exact ENNReal.mul_lt_top (second_fourier_integrable_aux1a hσ).2 hsupp.2