From d71659575c7946c1b3fd7b0b4350593d5136e24d Mon Sep 17 00:00:00 2001
From: L Lllvvuu <git@llllvvuu.dev>
Date: Sun, 4 Feb 2024 14:13:39 -0800
Subject: [PATCH] asyptotics

---
 Mathlib/MeasureTheory/Integral/Asymptotics.lean | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/Asymptotics.lean b/Mathlib/MeasureTheory/Integral/Asymptotics.lean
index 7498b294abe90e..3ce95e25702bd0 100644
--- a/Mathlib/MeasureTheory/Integral/Asymptotics.lean
+++ b/Mathlib/MeasureTheory/Integral/Asymptotics.lean
@@ -15,12 +15,12 @@ noncomputable section
 
 open Asymptotics MeasureTheory Set Filter
 
-variable {α E : Type*} [MeasurableSpace α] {f g : α → E} {a b : α} {μ : Measure α} {l : Filter α}
+variable {α E : Type*} [MeasurableSpace α] [NormedDivisionRing E] [NormedSpace ℝ E]
+ [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E]
+ {f g : α → E} {a b : α} {μ : Measure α} {l : Filter α}
 
-theorem _root_.Asymptotics.IsBigO.integrableAtFilter [NormedDivisionRing E] [NormedSpace ℝ E]
-    [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E]
-    (hfm : Measurable f) (hgm : Measurable g) (hf : f =O[l] g) (hg : IntegrableAtFilter g l μ) :
-    IntegrableAtFilter f l μ := by
+theorem _root_.Asymptotics.IsBigO.integrableAtFilter (hfm : Measurable f) (hgm : Measurable g)
+    (hf : f =O[l] g) (hg : IntegrableAtFilter g l μ) : IntegrableAtFilter f l μ := by
   obtain ⟨C, hC⟩ := hf.bound
   obtain ⟨C', hC'⟩ := exists_norm_eq E <| le_max_right C 0
   obtain ⟨s, hsl, hs⟩ := hC.exists_mem
@@ -35,4 +35,10 @@ theorem _root_.Asymptotics.IsBigO.integrableAtFilter [NormedDivisionRing E] [Nor
     gcongr
     apply le_max_left
 
+theorem _root_.Asymptotics.IsBigO.integrable
+    (hfm : Measurable f) (hgm : Measurable g)
+    (hf : f =O[⊤] g) (hg : Integrable g μ) : Integrable f μ := by
+  rewrite [← IntegrableAtFilter.top] at *
+  exact hf.integrableAtFilter hfm hgm hg
+
 end