exact integral_mono (l1.mono' hf (eventually_of_forall h)).norm l1 h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
hf : AEStronglyMeasurable f volume
h : ∀ (t : ℝ), ‖f t‖ ≤ A * (1 + t ^ 2)⁻¹
l1 : Integrable (fun x => A * (1 + x ^ 2)⁻¹) volume
⊢ ∫ (t : ℝ), ‖f t‖ ≤ ∫ (a : ℝ), A * (1 + a ^ 2)⁻¹
no goals