asyptotics

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